Origin growth from the common temporal remainder input #
A majorant on each contained cylinder's time window extends by zero to the whole time axis. The backward origin cover then applies with the same half ball and the same cylinder scale. No symmetric enlargement of the time window or additional pressure estimate is needed.
theorem
CKN.Core.Step4.originClause_global_remainder_of_temporal_majorant
(hRemainderMajorant :
∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ},
5 / 2 < q →
∀ {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ),
closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I →
∃ (M : ℝ → ENNReal),
AEMeasurable M (MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2)) ∧ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, M s ^ (3 / 2) < ⊤ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3),
∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2),
‖classicalGradient
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p
s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
x i‖ₑ ≤ M s)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
:
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ),
closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I →
∃ (M : ℝ → ENNReal),
AEMeasurable M MeasureTheory.volume ∧ ∫⁻ (s : ℝ), M s ^ (3 / 2) < ⊤ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3),
∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2),
‖classicalGradient
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
x i‖ₑ ≤ M s
Extending each temporal majorant by zero gives the global-time remainder input used by the origin derivative construction.
theorem
CKN.Core.Step4.originClause_derivative_morrey_of_temporal_majorant
(hRemainderMajorant :
∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ},
5 / 2 < q →
∀ {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ),
closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I →
∃ (M : ℝ → ENNReal),
AEMeasurable M (MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2)) ∧ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, M s ^ (3 / 2) < ⊤ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3),
∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2),
‖classicalGradient
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p
s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
x i‖ₑ ≤ M s)
{q τ R₀ R₁ : ℝ}
{KU KD : ENNReal}
(hq : 5 / 2 < q)
(hτ : 25 / 3 ≤ τ)
(hτhi : τ ≤ 25)
(hR₁ : 0 < R₁)
(hgap : R₁ < R₀)
(hR₀ : R₀ < 1)
(hKU : KU < ⊤)
(hKD : KD < ⊤)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hU :
∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
u w i) ≤ KU)
(hDu :
∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
Du w i j) ≤ KD)
:
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s))
fun (y : Vec 3) => Dp (y, s) i) ∧ ∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q)
((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
Dp w i) < ⊤
The common temporal remainder input yields one measurable weak pressure gradient with finite Morrey norms on the backward origin carrier.
theorem
CKN.Core.Step4.originClause_clipped_growth_of_temporal_majorant
(hRemainderMajorant :
∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ},
5 / 2 < q →
∀ {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ),
closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I →
∃ (M : ℝ → ENNReal),
AEMeasurable M (MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2)) ∧ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, M s ^ (3 / 2) < ⊤ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3),
∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2),
‖classicalGradient
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p
s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
x i‖ₑ ≤ M s)
{q τ R₀ R₁ : ℝ}
{KU KD : ENNReal}
(hq : 5 / 2 < q)
(hτ : 25 / 3 ≤ τ)
(hτhi : τ ≤ 25)
(hR₁ : 0 < R₁)
(hgap : R₁ < R₀)
(hR₀ : R₀ < 1)
(hKU : KU < ⊤)
(hKD : KD < ⊤)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hU :
∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
u w i) ≤ KU)
(hDu :
∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
Du w i j) ≤ KD)
:
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s))
fun (y : Vec 3) => Dp (y, s) i) ∧ ∃ A < ⊤,
∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ),
0 < r →
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))
The common temporal remainder input yields the clipped growth bound for the same selected gradient, uniformly over all centres and positive radii.