Regularization of weakly harmonic functions

Reflection about a fixed point negates the Fréchet derivative.

The Laplacian is unchanged by reflection about a fixed point.

theorem LiebThirring.fderiv_reflect {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {b : E → F} (hb : Differentiable ℝ b) (x y : E) : fderiv ℝ (fun (z : E) => b (x - z)) y = -fderiv ℝ b (x - y)

Reflection about a fixed point negates the Fréchet derivative.

theorem LiebThirring.laplacian_reflect {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {b : E → ℝ} (hb : ContDiff ℝ 2 b) (x y : E) : Laplacian.laplacian (fun (z : E) => b (x - z)) y = Laplacian.laplacian b (x - y)

The Laplacian is unchanged by reflection about a fixed point.

theorem LiebThirring.laplacian_convolution_eq_zero_of_weak {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] {w b : E → ℝ} (hw : Continuous w) (hweak : ∀ (f : E → ℝ), ContDiff ℝ (↑⊤) f → HasCompactSupport f → ∫ (z : E), w z * Laplacian.laplacian f z ∂μ = 0) (hb : ContDiff ℝ (↑⊤) b) (hbc : HasCompactSupport b) (x : E) : Laplacian.laplacian (MeasureTheory.convolution w b (ContinuousLinearMap.lsmul ℝ ℝ) μ) x = 0

The weak test equation makes every smooth compact-kernel convolution harmonic.