Fixed-radius pressure slices on the full solution interval #
The unit time interval supplies enough room to cover the whole open solution
interval by interior backward windows of any fixed length less than one.
The slice bound of eq:pressure-gradient-morrey therefore holds almost
everywhere on the full interval, with its source radius unchanged.
Identification of cell-selected pressure gradients #
On each cell, a locally selected weak pressure gradient and the fixed glued gradient are weak derivatives of the same pressure. Uniqueness identifies them almost everywhere, preserving the cell's own quantitative bound.
theorem
CKN.Core.Step4.ae_glued_gradient_cell_selected_slice_identification
{B : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x : Foundation.Parabolic.Vec3}
{t r : ℝ}
(hr : 0 < r)
{M : ℝ → ENNReal}
(hball : Foundation.Parabolic.vec3Ball x r ⊆ B)
(htime : Set.Ioc (t - r ^ 2) t ⊆ I)
(hfield :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (k : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) k) B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) k)
(hslice :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - (2 * r) ^ 2) t), ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3),
(∀ (k : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => D y k) (euclideanBall x (2 * r / 2))
MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x (2 * r / 2))) ∧ (∀ (k : Fin 3),
HasWeakPartialDerivOn (euclideanBall x (2 * r / 2)) k (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) =>
D y k) ∧ ∀ (k : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => D y k) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (euclideanBall x (2 * r / 2))) ≤ M s)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t), ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3),
(∀ (k : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => D y k) (euclideanBall x (2 * r / 2))
MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x (2 * r / 2))) ∧ (∀ (k : Fin 3),
HasWeakPartialDerivOn (euclideanBall x (2 * r / 2)) k (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) =>
D y k) ∧ (∀ (k : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => D y k) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (euclideanBall x (2 * r / 2))) ≤ M s) ∧ (∀ (k : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) k) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (euclideanBall x (2 * r / 2))) ≤ M s) ∧ ∀ (k : Fin 3),
(fun (y : Foundation.Parabolic.Vec3) =>
Dp (y, s) k) =ᵐ[MeasureTheory.volume.restrict (euclideanBall x (2 * r / 2))]
fun (y : Vec 3) => D y k
The selected weak-gradient witness on a doubled cell agrees locally with the fixed glued field. Its norm bound retains the majorant belonging to that cell.
theorem
CKN.Core.Step4.ae_on_interval_of_fixed_windows
{I : Set ℝ}
(hIo : IsOpen I)
(hIc : I.OrdConnected)
(hunit : Set.Icc (-1) 0 ⊆ I)
{d : ℝ}
(hd : 0 < d)
(hd1 : d < 1)
{P : ℝ → Prop}
(hwindow : ∀ (t : ℝ), Set.Icc (t - d) t ⊆ I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - d) t), P s)
:
A statement holding almost everywhere on every interior backward window of a fixed length less than one holds almost everywhere on the full interval.
theorem
CKN.Core.Step4.origin_slice_bound_on_full_interval
{ρ : ℝ}
(hρ : 0 < ρ)
(hρone : ρ < 1)
{Ω : 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}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hball : closure (Foundation.Parabolic.vec3Ball 0 ρ) ⊆ Ω)
(htime : Set.Icc (-1) 0 ⊆ I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 ρ)) ∧ ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3),
(∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => D y i)
(Foundation.Parabolic.vec3Ball 0 (ρ / 2)) MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 (ρ / 2))) ∧ (∀ (i : Fin 3),
HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 (ρ / 2)) i (fun (y : Vec 3) => p (y, s))
fun (y : Vec 3) => D y i) ∧ ∀ (i : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => D y i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 (ρ / 2))) ≤ originSliceGradientMajorant u Du p f (0, 0) hρ s
The complete fixed-origin slice estimate holds on almost every time of the entire solution interval; unit-time containment and compact spatial source containment suffice.
theorem
CKN.Core.Step4.translated_slice_bound_on_full_interval
(x : Foundation.Parabolic.Vec3)
{ρ : ℝ}
(hρ : 0 < ρ)
(hρone : ρ < 1)
{Ω : 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}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hball : closure (Foundation.Parabolic.vec3Ball x ρ) ⊆ Ω)
(htime : Set.Icc (-1) 0 ⊆ I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
∃ (g : Foundation.Parabolic.Vec3 → ℝ),
MeasureTheory.LocallyIntegrableOn g (Foundation.Parabolic.vec3Ball x (ρ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball x (ρ / 2)) i (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x (ρ / 2))) ≤ Endgame.theoremATranslatedSliceMajorant u Du p f x hρ s
Translating a fixed source ball gives the complete local slice bound on almost every time in the full solution interval, with the exact translated majorant used by the carrier time estimate.
theorem
CKN.Core.Step4.origin_carrier_finite_translated_slice_estimate
(R : ℝ)
(hR : 0 < R)
(hR34 : R < 3 / 4)
:
∃ (n : ℕ) (x : Fin n → Foundation.Parabolic.Vec3) (ρ : ℝ) (hρ : 0 < ρ),
(∀ (j : Fin n), closure (Foundation.Parabolic.vec3Ball (x j) ρ) ⊆ Foundation.Parabolic.vec3Ball 0 1) ∧ ∀ {Ω : 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 →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
∀ (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),
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R)) ≤ ∑ j : Fin n, Endgame.theoremATranslatedSliceMajorant u Du p f (x j) hρ s
The exact finite spatial estimate used by the full-interval carrier
time theorem. All centres and the source radius are chosen before the
suitable solution, and the bound holds on almost every time in all of I.
theorem
CKN.Core.Step4.origin_carrier_slice_time_obligations_of_sws
{R : ℝ}
(hR : 0 < R)
(hR34 : R < 3 / 4)
{Ω : 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}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(hDp : Measurable Dp)
(hfield :
∀ᵐ (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),
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R)) ≠ ⊤) ∧ ∀ (i : Fin 3) (T : Set ℝ),
IsCompact (closure T) →
closure T ⊆ I →
MeasureTheory.Integrable
(fun (s : ℝ) =>
(MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R))).toReal)
(MeasureTheory.volume.restrict T)
The selected gradient on the whole spatial carrier has finite slice
norm almost everywhere on I, and its slice norm is integrable on every
compactly interior time set, with no additional slice estimate hypothesis.