Corrected pressure-gradient slices from suitable-solution data #
The force-free centred source and its tested identity are extracted from suitable-solution data. The resulting quantitative slice estimate is in the form used to transfer a doubled-scale bound to cell data.
theorem
CKN.Core.Step4.slice_selected_gradient_corrected_ae_of_sws_data
(C₁₇ C_P1 C₈ : ℝ)
(hC₁₇ : 1000 * Foundation.Heat.harmonicInteriorDisplayConstant ≤ C₁₇)
(hCZ_p1 : Foundation.Euclidean.czP1OperatorConstant ≤ C_P1)
(hC₈ : sliceForceGradientConstant ≤ C₈)
{Ω : 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}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3),
(∀ (k : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => D x k) (euclideanBall z.1 (ρ / 2))
MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ∧ (∀ (k : Fin 3),
HasWeakPartialDerivOn (euclideanBall z.1 (ρ / 2)) 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) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ ENNReal.ofReal Foundation.Euclidean.czGradientOperatorConstant * ∑ _i : Fin 3, centredSWSCentredMajorant z.1 ρ q u Du f s + ENNReal.ofReal
(C₁₇ * (MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (euclideanBall z.1 ρ)) + 9 * C_P1 * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, utensorNorm u z.1 ρ s y ^ (3 / 2)) ^ (2 / 3) + harmonicRemainderForceBound z hρ f s) * ρ ^ (-1 / 2)) + ENNReal.ofReal (sliceForceGradientBound Foundation.Euclidean.czGradientOperatorConstant C₈ z.1 hρ f s)
The corrected force-free centred-source slice estimate, with the
quantitative bound consumed by the doubled-slice cell transfer. Its only
analytic hypothesis beyond suitability and cylinder containment is the
operator bound hCZ_p1.