Blowup Riesz Decomposition #
Pressure reconstruction and convergence bounds for the rescaled sequence.
theorem
ESS.blowup_tensor_time_near_far
(F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(L : ℝ)
(J : Set ℝ)
:
A time-restricted tensor is the sum of its near and exterior spatial parts, pointwise.
theorem
ESS.blowup_rieszPressureSpaceTime_congr
{F G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
(hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
(hFG : F = G)
:
The chosen pressure representative does not depend on the proof that its
tensor components belong to L^(3/2).
theorem
ESS.blowup_rieszPressure_time_near_far_ae
(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 : ℝ)
(J : Set ℝ)
(hJ : MeasurableSet J)
:
let S := Set.univ ×ˢ J;
let A := CKN.euclideanBall 0 L ×ˢ J;
let B := (CKN.euclideanBall 0 L)ᶜ ×ˢ J;
let Ftime := fun (i j : Fin 3) => S.indicator (F i 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 hTime := ⋯;
have hNear := ⋯;
have hFar := ⋯;
CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_congr._proof_1 Ftime
hTime =ᵐ[MeasureTheory.volume]
fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_congr._proof_1 Fnear hNear z + CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_congr._proof_1 Ffar hFar z
The Riesz pressure of a time-restricted tensor splits almost everywhere into near and far pressures for every spatial radius.
theorem
ESS.blowup_rieszPressure_full_near_far_on_time_ae
(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 : ℝ)
(J : Set ℝ)
(hJ : MeasurableSet J)
:
have S := Set.univ ×ˢ 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 := ⋯;
S.indicator
(CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_congr._proof_1 F
hF) =ᵐ[MeasureTheory.volume]
S.indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_congr._proof_1 Fnear hNear z + CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_congr._proof_1 Ffar hFar z
On a fixed time set, the full Riesz pressure equals the sum of the near and exterior pressures.
theorem
ESS.blowup_rieszPressure_full_near_far_local_ae
(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)
:
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 := ⋯;
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_congr._proof_1 F hF
z) =ᵐ[MeasureTheory.volume.restrict (CKN.euclideanBall 0 R ×ˢ J)]
fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_congr._proof_1 Fnear hNear z + CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_congr._proof_1 Ffar hFar z
On every spatial ball over the selected time set, the full pressure is the sum of the near and exterior pressures almost everywhere.