Scale-independent local L² control of weak harmonic fields on ordinary R³.

theorem EulerMeanHarmonic.weakScalarHarmonic_pointwise_scaled (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (R : ℝ) (hR : 0 < R) (hh : ScalarWeakHarmonicOn (Metric.ball 0 R) f) : ∀ᵐ (x : EulerSmoothLimit.Space), x ∈ Metric.closedBall 0 (R / 4) → f x ^ 2 ≤ harmonicQuarterBallConstant * (R ^ 3)⁻¹ * MeasureTheory.lpNorm f 2 MeasureTheory.volume ^ 2

theorem EulerMeanHarmonic.weakHarmonic_pointwise_scaled (u : ↥EulerMeanSolenoidal.L2) (R : ℝ) (hR : 0 < R) (hu : WeakHarmonicOn (Metric.ball 0 R) u) : ∀ᵐ (x : EulerSmoothLimit.Space), x ∈ Metric.closedBall 0 (R / 4) → ‖↑↑u x‖ ^ 2 ≤ harmonicQuarterBallConstant * (R ^ 3)⁻¹ * ‖u‖ ^ 2

theorem EulerMeanHarmonic.weakHarmonic_scaled_smallBall_energy (u : ↥EulerMeanSolenoidal.L2) (R : ℝ) (hR : 0 < R) (hu : WeakHarmonicOn (Metric.ball 0 R) u) (r : ℝ) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) : localL2Energy (Metric.ball 0 (R * r)) u ≤ weakHarmonicSmallBallConstant * r ^ 3 * ‖u‖ ^ 2

The radius R of the ambient harmonic ball cancels exactly from the local-energy estimate.