Spatial scaling of the harmonic pressure supremum

Positive spatial dilations preserve essential suprema up to the pressure amplitude, on any measurable region whose image stays in the interior ball.

theorem ESS.pressureSplit_scaledSpatial_sup_le {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩ : MeasurableSet Ω) {x₀ : CKN.Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (himage : ∀ x ∈ Ω, CKN.scalingSpace r x₀ x ∈ CKN.euclideanBall 0 (3 / 4)) (p : CKN.Foundation.Parabolic.Vec3 → ℝ) (hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.euclideanBall 0 1))) : MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => r ^ 2 * p (CKN.scalingSpace r x₀ x)) ⊤ (MeasureTheory.volume.restrict Ω) ≤ ENNReal.ofReal (r ^ 2) * MeasureTheory.eLpNorm p ⊤ (MeasureTheory.volume.restrict (CKN.euclideanBall 0 (3 / 4)))

The spatial pressure scaling is bounded by the source interior supremum on every measurable region whose image lies in the three-quarter ball.