Reg Tails Assembly

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.regTails_compact_weight_interval_increment (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (J : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hLE : ∀ ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), spatialGradientSq u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) z * ψ z = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + ∑ i : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * J z i + 2 * p z * u z i) * spatialPartial ψ i z) (hUcont : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (z.1, z.2) i) (Set.univ ×ˢ Set.Ioi 0)) (hDcont : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (Set.univ ×ˢ Set.Ioi 0)) (hPcont : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => p (z.1, z.2)) (Set.univ ×ˢ Set.Ioi 0)) (hJcont : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => J (z.1, z.2) i) (Set.univ ×ˢ Set.Ioi 0)) (hUdiff : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (z.1, z.2) i) (Set.univ ×ˢ Set.Ioi 0)) (q : Foundation.Parabolic.Vec3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hqc : HasCompactSupport q) {s t : ℝ} (hs : 0 < s) (hst : s < t) : regTailsEnergyWeight u q t - regTailsEnergyWeight u q s = ∫ (τ : ℝ) in s..t, ∫ (x : Foundation.Parabolic.Vec3), regTailsLocalizedSource u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) p J q (x, τ)

A compact spatial weight has the integrated localized energy identity on every positive-time interval, as in lem:reg-tails.

theorem CKN.Leray.regTails_localized_source_integral_le_flux (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (J : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (q : Foundation.Parabolic.Vec3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hqc : HasCompactSupport q) (hq0 : ∀ (x : Foundation.Parabolic.Vec3), 0 ≤ q x) (t : ℝ) (hUcont : ∀ (i : Fin 3), Continuous fun (x : Foundation.Parabolic.Vec3) => u (x, t) i) (hDcont : ∀ (i j : Fin 3), Continuous fun (x : Foundation.Parabolic.Vec3) => D (x, t) i j) (hPcont : Continuous fun (x : Foundation.Parabolic.Vec3) => p (x, t)) (hJcont : ∀ (j : Fin 3), Continuous fun (x : Foundation.Parabolic.Vec3) => J (x, t) j) : ∫ (x : Foundation.Parabolic.Vec3), regTailsLocalizedSource u D p J q (x, t) ≤ ∫ (x : Foundation.Parabolic.Vec3), 2 * ∑ i : Fin 3, ∑ j : Fin 3, |u (x, t) i| * |D (x, t) i j| * |spatialDeriv q j x| + ∑ j : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ^ 2 * |J (x, t) j| + 2 * |p (x, t)| * |u (x, t) j|) * |spatialDeriv q j x|

The localized source integral is bounded by the absolute flux density.

theorem CKN.Leray.regTails_open_interval_flux_bound {s t B M Q : ℝ} (hs : 0 < s) (hst : s < t) (hB : 0 ≤ B) (hM : 0 ≤ M) (hQ : 0 ≤ Q) (G A : ℝ → ℝ) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (Set.Ioo 0 t))) (hG0 : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), 0 ≤ G τ) (hGenergy : ∫ (τ : ℝ) in Set.Ioo 0 t, G τ ^ 2 ≤ B ^ 2 / 2) (hAcont : ContinuousOn A (Set.Ioi 0)) (hAprofile : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), A τ ≤ 18 * M * B * G τ + Q * M * B ^ (3 / 2) * G τ ^ (3 / 2)) : ∫ (τ : ℝ) in s..t, A τ ≤ 18 * M * B ^ 2 * t ^ (1 / 2) + Q * M * B ^ 3 * t ^ (1 / 4)

A positive-time source increment is bounded by the global flux profile.