Cellwise bounds for one measurable pressure gradient #
The slice bounds in paper/ckn.tex, Section sec:pressure, are
transported from the derivative selected at a cell's scale to a fixed field.
Spatial a.e. uniqueness preserves the complete quantitative majorant. Time
windows are restricted only along an explicit subset inclusion.
theorem
CKN.Core.Step4.ae_glued_gradient_bound_of_vector_slice_bound
{B W : Set Foundation.Parabolic.Vec3}
{I J : Set ℝ}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{q : ENNReal}
{M : ℝ → ENNReal}
(hW : IsOpen W)
(hWB : W ⊆ B)
(hJI : J ⊆ I)
(hfield :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (k : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => Dp (x, s) k) B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) => Dp (x, s) k)
(hslice :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3),
(∀ (k : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => D x k) W MeasureTheory.volume) ∧ MeasureTheory.MemLp D q (MeasureTheory.volume.restrict W) ∧ (∀ (k : Fin 3), HasWeakPartialDerivOn W k (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) => D x k) ∧ ∀ (k : Fin 3),
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => D x k) q (MeasureTheory.volume.restrict W) ≤ M s)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (k : Fin 3),
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Dp (x, s) k) q (MeasureTheory.volume.restrict W) ≤ M s
A vector slice bound on an open cell transfers, coordinate by coordinate, to a fixed weak gradient on a larger spatial carrier and time set.
theorem
CKN.Core.Step4.ae_glued_gradient_cell_bound_of_doubled_slice_bound
{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), ∀ (k : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) k) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)) ≤ M s
The cell bound on a doubled cylinder supplies the bound on its half-radius spatial ball throughout the cell's shorter backward time window.
theorem
CKN.Core.Step4.ae_glued_gradient_cell_data_of_doubled_slice_bound
{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)
(k : Fin 3)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t), ∃ (g : Foundation.Parabolic.Vec3 → ℝ),
MeasureTheory.LocallyIntegrableOn g (Foundation.Parabolic.vec3Ball x r) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball x r) k (fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)) ≤ M s
The same field supplies the existential cell datum required by the cell-transfer theorem; the witness is its own restricted spatial slice.