The proved harmonic interior bound for the actual weak L² solution.

Differentiating an actual compact mollifier transfers the distributional Laplacian to the kernel.

theorem EulerMeanHarmonic.partialDerivative_convolution_right (f g : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (i : Fin 3) : EulerVectorCalculus.partialDerivative (MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) i = MeasureTheory.convolution f (EulerVectorCalculus.partialDerivative g i) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

theorem EulerMeanHarmonic.laplacian_convolution_right (f g : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : Laplacian.laplacian (MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) = MeasureTheory.convolution f (Laplacian.laplacian g) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

Two genuine differentiations under the compact-kernel convolution integral.

theorem EulerMeanHarmonic.laplacian_comp_add_left (g : EulerSmoothLimit.Space → ℝ) (a x : EulerSmoothLimit.Space) : Laplacian.laplacian (fun (y : EulerSmoothLimit.Space) => g (a + y)) x = Laplacian.laplacian g (a + x)

theorem EulerMeanHarmonic.laplacian_comp_const_sub (g : EulerSmoothLimit.Space → ℝ) (hg : ContDiff ℝ (↑⊤) g) (a x : EulerSmoothLimit.Space) : Laplacian.laplacian (fun (y : EulerSmoothLimit.Space) => g (a - y)) x = Laplacian.laplacian g (a - x)

Reflection contributes two minus signs to the scalar Laplacian.

theorem EulerMeanHarmonic.convolution_harmonic_at (U : Set EulerSmoothLimit.Space) (f g : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (hh : ScalarWeakHarmonicOn U f) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (x : EulerSmoothLimit.Space) (hsupport : (tsupport fun (y : EulerSmoothLimit.Space) => g (x - y)) ⊆ U) : Laplacian.laplacian (MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) x = 0

A compact kernel contained in the weak-harmonic region produces a classical harmonic value.

theorem EulerMeanHarmonic.normed_reflected_support (φ : ContDiffBump 0) (x : EulerSmoothLimit.Space) : (tsupport fun (y : EulerSmoothLimit.Space) => φ.normed MeasureTheory.volume (x - y)) ⊆ Metric.closedBall x φ.rOut

theorem EulerMeanHarmonic.scalarMollification_harmonic (φ : ContDiffBump 0) (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hh : ScalarWeakHarmonicOn (Metric.ball 0 1) f) (hr : φ.rOut ≤ 1 / 4) (x : EulerSmoothLimit.Space) : x ∈ Metric.ball 0 (1 / 2) → Laplacian.laplacian (scalarMollification φ f) x = 0

Actual compact mollification turns weak harmonicity into classical harmonicity in the interior.

theorem EulerMeanHarmonic.interiorMollifier_harmonic (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hh : ScalarWeakHarmonicOn (Metric.ball 0 1) f) (n : ℕ) (x : EulerSmoothLimit.Space) : x ∈ Metric.ball 0 (1 / 2) → Laplacian.laplacian (scalarMollification (interiorMollifier n) f) x = 0

theorem EulerMeanHarmonic.weakScalarHarmonic_pointwise (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hh : ScalarWeakHarmonicOn (Metric.ball 0 1) f) : ∀ᵐ (x : EulerSmoothLimit.Space), x ∈ Metric.closedBall 0 (1 / 4) → f x ^ 2 ≤ harmonicQuarterBallConstant * MeasureTheory.lpNorm f 2 MeasureTheory.volume ^ 2

A scalar distributionally harmonic L² field has a uniform a.e. interior bound.

theorem EulerMeanHarmonic.weakHarmonic_pointwise (u : ↥EulerMeanSolenoidal.L2) (hu : WeakHarmonicOn (Metric.ball 0 1) u) : ∀ᵐ (x : EulerSmoothLimit.Space), x ∈ Metric.closedBall 0 (1 / 4) → ‖↑↑u x‖ ^ 2 ≤ harmonicQuarterBallConstant * ‖u‖ ^ 2

The same bound for an actual vector L² field, without assuming a smooth representative.

noncomputable def EulerMeanHarmonic.weakHarmonicSmallBallConstant : ℝ

Weak harmonic small ball constant, given by (Real.pi * 4 / 3) * harmonicQuarterBallConstant.

Equations

• EulerMeanHarmonic.weakHarmonicSmallBallConstant = Real.pi * 4 / 3 * EulerMeanHarmonic.harmonicQuarterBallConstant

theorem EulerMeanHarmonic.weakHarmonicSmallBallConstant_nonneg : 0 ≤ weakHarmonicSmallBallConstant

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

Source localization for weakly harmonic fields: the radius enters with the genuine power 3.