Actual dilation identities for L² fields and weak harmonic scalar functions.

theorem EulerMeanHarmonic.memLp_dilation {V : Type u_1} [NormedAddCommGroup V] (f : EulerSmoothLimit.Space → V) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (a : ℝ) (ha : a ≠ 0) : MeasureTheory.MemLp (fun (x : EulerSmoothLimit.Space) => f (a • x)) 2 MeasureTheory.volume

theorem EulerMeanHarmonic.lpNorm_dilation_sq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (a : ℝ) (ha : 0 < a) : MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => f (a • x)) 2 MeasureTheory.volume ^ 2 = (a ^ 3)⁻¹ * MeasureTheory.lpNorm f 2 MeasureTheory.volume ^ 2

theorem EulerMeanHarmonic.scalarWeakHarmonicOn_dilation (f : EulerSmoothLimit.Space → ℝ) (R : ℝ) (hR : 0 < R) (hf : ScalarWeakHarmonicOn (Metric.ball 0 R) f) : ScalarWeakHarmonicOn (Metric.ball 0 1) fun (x : EulerSmoothLimit.Space) => f (R • x)

The distributional harmonic test identity is preserved by spatial dilation.