From a Morrey majorant to the A-slot estimate for the correction #
The actual Riesz fields of the centred source correction, not merely a measurable selection of them, satisfy the clipped-cell affine estimate as soon as the carrier-restricted sources carry a common Morrey majorant. The carrier restriction is invisible on the collar time window because the correction vanishes off the source ball.
theorem
CKN.Core.Step4.originASlot_correction_zero_outside
{R₀ : ℝ}
{η : Foundation.Parabolic.Vec3 → ℝ}
{dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
(hη : ∀ x ∉ Foundation.Parabolic.vec3Ball 0 R₀, η x = 0)
(hdη : ∀ (k : Fin 3), ∀ x ∉ Foundation.Parabolic.vec3Ball 0 R₀, dη k x = 0)
(u f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3)
(c : Foundation.Parabolic.Vec3)
(j : Fin 3)
{x : Foundation.Parabolic.Vec3}
(hx : x ∉ Foundation.Parabolic.vec3Ball 0 R₀)
:
Outside the source ball the centred correction vanishes.
theorem
CKN.Core.Step4.originASlot_correction_slice_eq
{R₀ ρ : ℝ}
{η : Foundation.Parabolic.Vec3 → ℝ}
{dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
(hη : ∀ x ∉ Foundation.Parabolic.vec3Ball 0 R₀, η x = 0)
(hdη : ∀ (k : Fin 3), ∀ x ∉ Foundation.Parabolic.vec3Ball 0 R₀, dη k x = 0)
{c : ℝ → Foundation.Parabolic.Vec3}
(u' f' : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du' : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(z : Foundation.Parabolic.ParabolicPoint)
(j : Fin 3)
{s : ℝ}
(hs : s ∈ Set.Ioc (z.2 - ρ ^ 2) z.2)
:
(fun (x : Foundation.Parabolic.Vec3) =>
(Foundation.Parabolic.vec3Ball 0 R₀ ×ˢ Set.Ioc (z.2 - ρ ^ 2) z.2).indicator
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) η dη
(fun (y : Foundation.Parabolic.Vec3) => u' (y, w.2)) (fun (y : Foundation.Parabolic.Vec3) => f' (y, w.2))
(fun (y : Foundation.Parabolic.Vec3) => Du' (y, w.2)) (c w.2) j w.1)
(x, s)) = fun (x : Foundation.Parabolic.Vec3) =>
centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) η dη
(fun (y : Foundation.Parabolic.Vec3) => u' (y, s)) (fun (y : Foundation.Parabolic.Vec3) => f' (y, s))
(fun (y : Foundation.Parabolic.Vec3) => Du' (y, s)) (c s) j x
On the collar time window the carrier restriction does not change the centred correction slices.
theorem
CKN.Core.Step4.originASlot_literal_riesz_sum_clipped_le_slot
(q τ C_CZ ε : ℝ)
(KU KD Cbig : ENNReal)
(hq : 5 / 2 < q)
(hτ : 25 / 3 ≤ τ)
(hτhi : τ ≤ 25)
(hcoef : pressureRieszMorreyConstant (25 / 9) * Cbig ≤ ENNReal.ofReal (|C_CZ| + 1))
(i : Fin 3)
{F : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ}
(hF : ∀ (j : Fin 3), AEMeasurable (F j) MeasureTheory.volume)
(hFs :
∀ (j : Fin 3),
∀ᵐ (s : ℝ), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => F j (y, s)) (ENNReal.ofReal (6 / 5))
MeasureTheory.volume)
{K : Set Foundation.Parabolic.Vec3}
(hK : IsCompact K)
(hsupport : ∀ (j : Fin 3) (y : Foundation.Parabolic.Vec3) (s : ℝ), y ∉ K → F j (y, s) = 0)
(hN :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) (F j) ≤ Cbig * (3 * KU * KD + Endgame.forceSourceMorreyBound q ε))
(B : Set Foundation.Parabolic.Vec3)
(J : Set ℝ)
(z : Foundation.Parabolic.ParabolicPoint)
{r : ℝ}
(hr : 0 < r)
:
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ J, MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) =>
∑ j : Fin 3,
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯
(fun (x : Foundation.Parabolic.Vec3) => F j (x, s)) y)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ B)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))
The actual Riesz fields of three sources with a common Morrey majorant satisfy the affine clipped-cell estimate above the matching threshold.
theorem
CKN.Core.Step4.originASlot_correction_mass_of_morrey_bound
(q τ C_CZ R₀ R₁ ε : ℝ)
(KU KD Cbig : ENNReal)
(hq : 5 / 2 < q)
(hτ : 25 / 3 ≤ τ)
(hτhi : τ ≤ 25)
(hcoef : pressureRieszMorreyConstant (25 / 9) * Cbig ≤ ENNReal.ofReal (|C_CZ| + 1))
(hR₁ : 0 < R₁)
(hgap : R₁ < R₀)
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(z : Foundation.Parabolic.ParabolicPoint)
(hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁))
(i : Fin 3)
(r : ℝ)
(hr : 0 < r)
(hcell : r ≤ (R₀ - R₁) / 4)
(hρ : 0 < (R₀ - R₁) / 2)
(G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ)
(hG :
∀ (j : Fin 3),
G j = (Foundation.Parabolic.vec3Ball 0 R₀ ×ˢ Set.Ioc (z.2 - ((R₀ - R₁) / 2) ^ 2) z.2).indicator
fun (w : Foundation.Parabolic.ParabolicPoint) =>
centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) (mollifiedBallCutoff z.1 hρ)
(spatialDeriv (mollifiedBallCutoff z.1 hρ)) (fun (y : Foundation.Parabolic.Vec3) => u (y, w.2))
(fun (y : Foundation.Parabolic.Vec3) => f (y, w.2)) (fun (y : Foundation.Parabolic.Vec3) => Du (y, w.2))
(sourceSliceCentredMean z.1 ((R₀ - R₁) / 2) u w.2) j w.1)
(hF : ∀ (j : Fin 3), AEMeasurable (G j) MeasureTheory.volume)
(hFs :
∀ (j : Fin 3),
∀ᵐ (s : ℝ), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => G j (y, s)) (ENNReal.ofReal (6 / 5))
MeasureTheory.volume)
(hN :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) (G j) ≤ Cbig * (3 * KU * KD + Endgame.forceSourceMorreyBound q ε))
:
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm
(fun (x : Foundation.Parabolic.Vec3) =>
∑ j : Fin 3,
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯
(centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) (mollifiedBallCutoff z.1 hρ)
(spatialDeriv (mollifiedBallCutoff z.1 hρ)) (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (y : Foundation.Parabolic.Vec3) => f (y, s)) (fun (y : Foundation.Parabolic.Vec3) => Du (y, s))
(sourceSliceCentredMean z.1 ((R₀ - R₁) / 2) u s) j)
x)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))
Given the Morrey majorant for the carrier-restricted correction sources, the clipped-cell time mass of the actual correction Riesz fields satisfies the affine A-slot estimate.