Display (3.5) with the explicit Calderón–Zygmund endpoint constant #
The preceding slice theorem takes the weak-gradient construction as an explicit
hP1 input. The concrete extension theorem supplies exactly that input at
czGradientOperatorConstant, so this module exposes the resulting
solution-level statement without an analytic Calderón–Zygmund premise.
theorem
CKN.Core.Step4.slice_selected_gradient_ae_of_sws_of_source_data_unconditional
(C₁₇ C₁₁ C₈ : ℝ)
(hC₁₇ : 1000 * Foundation.Heat.harmonicInteriorDisplayConstant ≤ C₁₇)
(hC₈ : sliceForceGradientConstant ≤ C₈)
{E F : ℝ → ℝ}
{Ω : 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 V : 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)
(hC₁₁ : 0 ≤ C₁₁)
(hE : ∀ (s : ℝ), 0 ≤ E s)
(hF : ∀ (s : ℝ), 0 ≤ F s)
(hCZ_p1 :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp
(pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm
(pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C₁₁ * E s ^ (2 / 3))
(hP78 :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ∧ MeasureTheory.lpNorm (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ≤ F s)
(hV :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), (∀ (i : Fin 3),
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => V (x, s) i) (ENNReal.ofReal (6 / 5))
MeasureTheory.volume) ∧ ∀ (i : Fin 3), HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => V (x, s) i)
(hVpair :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), V (x, s) i * spatialDeriv ψ i x = pressureSecondPairing
(fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) =>
mollifiedBallCutoff z.1 hρ x * pressureUTensor u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
(x, s) i j)
ψ)
:
∀ᵐ (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,
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => V (x, s) i) (ENNReal.ofReal (6 / 5))
MeasureTheory.volume + ENNReal.ofReal
(C₁₇ * (MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (euclideanBall z.1 ρ)) + C₁₁ * E s ^ (2 / 3) + F s) * ρ ^ (-1 / 2)) + ENNReal.ofReal (sliceForceGradientBound Foundation.Euclidean.czGradientOperatorConstant C₈ z.1 hρ f s)
Display (3.5) on a slice of a suitable weak solution with the explicit
czGradientOperatorConstant in the first-potential gradient bound.