Blowup Riesz Far Harmonic

Pressure reconstruction and convergence bounds for the rescaled sequence.

theorem ESS.blowup_harmonic_far_local_bound : ∃ C < ⊤, ∀ (h : CKN.Foundation.Parabolic.Vec3 → ℝ) (L R : ℝ), 0 < L → 0 < R → R ≤ 3 * L / 4 → MeasureTheory.MemLp h (3 / 2) MeasureTheory.volume → CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 L) h → MeasureTheory.eLpNorm h ⊤ (MeasureTheory.volume.restrict (CKN.euclideanBall 0 R)) ≤ C * ENNReal.ofReal (L ^ 2)⁻¹ * MeasureTheory.eLpNorm h (3 / 2) MeasureTheory.volume

A globally bounded L^(3/2) function that is harmonic on a large ball is small on a fixed inner ball. This is the interior estimate for the far pressure in prop:blowup-limit.