Blowup Riesz Far Time

Pressure reconstruction and convergence bounds for the rescaled sequence.

theorem ESS.blowup_harmonic_far_spaceTime_mass_bound : ∃ C < ⊤, ∀ (h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (L R : ℝ) (J : Set ℝ) (M : ENNReal), 0 < L → 0 < R → R ≤ 3 * L / 4 → MeasureTheory.AEStronglyMeasurable h ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 R)).prod (MeasureTheory.volume.restrict J)) → (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) (3 / 2) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) (3 / 2) MeasureTheory.volume ≤ M ∧ CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 L) fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) → ∫⁻ (z : CKN.Vec 3 × ℝ), ENNReal.ofReal |h z| ^ (3 / 2) ∂(MeasureTheory.volume.restrict (CKN.euclideanBall 0 R)).prod (MeasureTheory.volume.restrict J) ≤ MeasureTheory.volume J * (C * ENNReal.ofReal (L ^ 2)⁻¹ * M * MeasureTheory.volume (CKN.euclideanBall 0 R) ^ (2 / 3)) ^ (3 / 2)

Slice harmonicity and a uniform global pressure bound give the L^(3/2) far-field estimate on a bounded past cylinder.

theorem ESS.blowup_far_pressure_mass_bound_tendsto_zero (C M V T : ENNReal) (hC : C < ⊤) (hM : M < ⊤) (hV : V < ⊤) (hT : T < ⊤) : Filter.Tendsto (fun (n : ℕ) => T * (C * ENNReal.ofReal ((↑n + 1) ^ 2)⁻¹ * M * V ^ (2 / 3)) ^ (3 / 2)) Filter.atTop (nhds 0)

The quantitative far-field mass bound vanishes as the outer radius increases through integer radii.