Blowup Riesz Local Split Lp #
Pressure reconstruction and convergence bounds for the rescaled sequence.
theorem
ESS.blowup_rieszPressure_full_near_far_local_Lp
(F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
(L R : ℝ)
(J : Set ℝ)
(hJ : MeasurableSet J)
:
have C := CKN.euclideanBall 0 R ×ˢ J;
let A := CKN.euclideanBall 0 L ×ˢ J;
let B := (CKN.euclideanBall 0 L)ᶜ ×ˢ J;
let Fnear := fun (i j : Fin 3) => A.indicator (F i j);
let Ffar := fun (i j : Fin 3) => B.indicator (F i j);
have hNear := ⋯;
have hFar := ⋯;
let p := CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressure_full_near_far_local_Lp._proof_1 F hF;
let pn := CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressure_full_near_far_local_Lp._proof_1 Fnear hNear;
let pf := CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressure_full_near_far_local_Lp._proof_1 Ffar hFar;
have hp := ⋯;
have hn := ⋯;
have hf := ⋯;
MeasureTheory.MemLp.toLp p hp = MeasureTheory.MemLp.toLp pn hn + MeasureTheory.MemLp.toLp pf hf
The near and exterior pressure decomposition holds as an equality in
local L^(3/2) on a bounded cylinder.