Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Weyl's lemma

Let E be a finite-dimensional real inner product space with an additive Haar measure μ. A function u : E → ℝ that is continuous on an open set U and weakly harmonic there (∫ Δχ · u dμ = 0 for all smooth χ with compact support in U, WeaklyHarmonicOn) is C^∞ in U and satisfies Δu = 0 pointwise in U (weyl_of_weaklyHarmonicOn).

Proof

1. Reproduction by a radial kernel: for a smooth radial kernel ρ with ∫ ρ = 1 supported in closedBall 0 r (exists_radial_kernel), the mean value property (integral_radial_smul_eq_of_weaklyHarmonic) gives u = (B.indicator u) ⋆ ρ on ball x₀ r, where B = closedBall x₀ (2 r) ⊆ U. The right side is C^∞.
2. Harmonicity: Δ (f ⋆ ρ) = f ⋆ Δρ (laplacian_convolution), and (f ⋆ Δρ)(x₀) = ∫ Δψ · u for the test function ψ = ρ(· - x₀), which vanishes by weak harmonicity.
3. In dimension zero every function is constant.

This file imports only Mathlib and the TauCeti ports Weyl/{LaplacianInvariance, DuBoisReymond, PolarCoord, MeanValue}.lean, so that it can be reused elsewhere. The mean value property is the TauCeti port in Weyl/MeanValue.lean; the code in this file is new.

theorem ViscositySolns.Analysis.laplacian_eq_sum_fderiv_fderiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ E) {f : E → ℝ} (hf : ContDiff ℝ 2 f) (x : E) : Laplacian.laplacian f x = ∑ i : ι, (fderiv ℝ (fun (y : E) => (fderiv ℝ f y) (b i)) x) (b i)

The Laplacian as a sum of iterated directional derivatives along an orthonormal basis.

theorem ViscositySolns.Analysis.fderiv_convolution_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {f g : E → ℝ} (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (x v : E) : (fderiv ℝ (MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ) x) v = MeasureTheory.convolution f (fun (y : E) => (fderiv ℝ g y) v) (ContinuousLinearMap.lsmul ℝ ℝ) μ x

Directional derivative of a convolution with a C¹ compactly supported kernel.

theorem ViscositySolns.Analysis.laplacian_convolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {f g : E → ℝ} (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (x : E) : Laplacian.laplacian (MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ) x = MeasureTheory.convolution f (Laplacian.laplacian g) (ContinuousLinearMap.lsmul ℝ ℝ) μ x

Δ (f ⋆ g) = f ⋆ Δg for a smooth compactly supported kernel g.

theorem ViscositySolns.Analysis.exists_radial_kernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {r : ℝ} (hr : 0 < r) : ∃ (g : ℝ → ℝ), ContDiff ℝ (↑⊤) g ∧ (∀ (t : ℝ), r ^ 2 ≤ t → g t = 0) ∧ ∫ (y : E), g (‖y‖ ^ 2) ∂μ = 1

A smooth radial kernel of integral one: g is smooth, vanishes on [r², ∞), and ∫ g (‖y‖²) dμ = 1.

theorem ViscositySolns.Analysis.exists_contDiff_eventuallyEq_laplacian_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [Nontrivial E] {U : Set E} {u : E → ℝ} (hU : IsOpen U) (hcont : ContinuousOn u U) (hu : WeaklyHarmonicOn μ u U) {x₀ : E} (hx₀ : x₀ ∈ U) : ∃ (w : E → ℝ), ContDiff ℝ (↑⊤) w ∧ u =ᶠ[nhds x₀] w ∧ Laplacian.laplacian w x₀ = 0

Local Weyl lemma. A continuous weakly harmonic function agrees near each point of U with a smooth function whose Laplacian vanishes at that point.

theorem ViscositySolns.Analysis.weyl_of_weaklyHarmonicOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {U : Set E} {u : E → ℝ} (hU : IsOpen U) (hcont : ContinuousOn u U) (hu : WeaklyHarmonicOn μ u U) : ContDiffOn ℝ (↑⊤) u U ∧ ∀ x ∈ U, Laplacian.laplacian u x = 0

Weyl's lemma. A continuous weakly harmonic function on an open set U is C^∞ in U and classically harmonic there.