The local pressure-gradient estimate on origin margin cells #
At the scale (1 - R₁) / 4, cells meeting the origin carrier lie in a fixed
larger interior ball. The doubled source cylinder is admissible, and the
slice estimate in eq:pressure-gradient-morrey bounds the power integral of
one fixed measurable gradient, as used in prop:bootstrap.
theorem
CKN.Core.Step4.origin_margin_cell_subset_intermediate_ball
{R₁ r : ℝ}
{x : Foundation.Parabolic.Vec3}
(hmargin : r ≤ (1 - R₁) / 4)
(hmeet : (Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball 0 R₁).Nonempty)
:
Foundation.Parabolic.vec3Ball x r ⊆ Foundation.Parabolic.vec3Ball 0 ((1 + R₁) / 2)
A cell meeting the carrier at the origin margin scale lies in the
intermediate ball of radius (1 + R₁) / 2.
theorem
CKN.Core.Step4.origin_margin_cell_integral_le_of_sws
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q R₁ : ℝ}
{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)
(hR₁ : 0 < R₁)
(hR₁unit : R₁ < 1)
{Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hmeas : Measurable Dp)
(hfield :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (k : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) k)
(Foundation.Parabolic.vec3Ball 0 ((1 + R₁) / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 ((1 + R₁) / 2)) k (fun (y : Vec 3) => p (y, s))
fun (y : Vec 3) => Dp (y, s) k)
{x : Foundation.Parabolic.Vec3}
{t r : ℝ}
(hr : 0 < r)
(hmargin : r ≤ (1 - R₁) / 4)
(hmeet : (Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball 0 R₁).Nonempty)
(ht : t ∈ Set.Ioc (-(9 / 16)) 0)
(i : Fin 3)
:
Suitability and the actual slice estimate bound each margin-cell power integral of a fixed measurable weak gradient by the explicit time majorant.
theorem
CKN.Core.Step4.origin_measurable_gradient_margin_bounds_of_sws
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q R₁ : ℝ}
{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)
(hR₁ : 0 < R₁)
(hR₁unit : R₁ < 1)
:
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (k : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) k)
(Foundation.Parabolic.vec3Ball 0 ((1 + R₁) / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 ((1 + R₁) / 2)) k (fun (y : Vec 3) => p (y, s))
fun (y : Vec 3) => Dp (y, s) k) ∧ ∀ (x : Foundation.Parabolic.Vec3) (t r : ℝ) (hr : 0 < r),
r ≤ (1 - R₁) / 4 →
(Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball 0 R₁).Nonempty →
t ∈ Set.Ioc (-(9 / 16)) 0 →
∀ (i : Fin 3),
Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5)
(fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) (x, t) r ≤ ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, originSliceGradientMajorant u Du p f (x, t) ⋯ s ^ (6 / 5)
One measurable field supplied from suitability obeys the explicit slice-majorant bound on every origin margin cell meeting the carrier.