One measurable pressure gradient on the inner symmetric carrier #
Suitability on the doubled parabolic ball supplies spatial slice derivatives on a larger ball. Measurable selection fixes one field on the inner ball before any smaller cells or quantitative estimates are considered.
theorem
CKN.Core.Step4.closure_gradient_selection_cylinder_subset_doubled_ball
(z₀ : Foundation.Parabolic.ParabolicPoint)
{R : ℝ}
(hR : 0 < R)
:
closure (Foundation.Parabolic.parabolicCylinder z₀.1 (z₀.2 + R ^ 2 / 4) (3 * R / 2)) ⊆ Metric.ball z₀ (2 * R)
The larger auxiliary cylinder lies in the doubled parabolic ball.
theorem
CKN.Core.Step4.exists_measurable_inner_pressure_gradient_of_sws
{Ω : 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)
(z₀ : Foundation.Parabolic.ParabolicPoint)
{R : ℝ}
(hR : 0 < R)
(hdom : Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I)
:
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (z₀.2 - R ^ 2 / 4) (z₀.2 + R ^ 2 / 4)), ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball z₀.1 (R / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball z₀.1 (R / 2)) i (fun (y : Vec 3) => p (y, s))
fun (y : Vec 3) => Dp (y, s) i
Suitability fixes a single jointly measurable spatial weak pressure gradient over the entire time interval of the inner symmetric ball.