Documentation

LeanPool.ViscositySolutionTheory.ViscositySolns.Applications.Laplace.Weyl.MeanValue

The mean-value property of continuous weakly harmonic functions #

Let E be a nontrivial finite-dimensional real inner product space with an additive Haar measure μ, U ⊆ E open, and u : E → F continuous on U and weakly harmonic in U: ∫ Δχ • u ∂μ = 0 for every smooth χ with compact support in U. If closedBall x₀ R ⊆ U, then u x₀ is the average of u over the sphere of radius R about x₀:

∫ θ ∈ S, u (x₀ + R • θ) ∂μ.toSphere = μ.toSphere(S) • u x₀ (integral_toSphere_eq_of_weaklyHarmonic).

As a consequence, integrating against a radial kernel k (‖y‖) supported in closedBall 0 R reproduces u x₀ (integral_radial_smul_eq_of_weaklyHarmonic): ∫ k ‖y‖ • u (x₀ + y) ∂μ = (∫ k ‖y‖ ∂μ) • u x₀.

The argument (TauCeti) #

Write Φ s = ∫ θ ∈ S, u (s • θ) ∂μ.toSphere. For a test function ψ on (0, R), the radial test function χ x = ρ (‖x‖²), with ρ the primitive of t ↦ ψ (√t) / (√t) ^ n, has Δχ x = 4 ‖x‖² ρ'' (‖x‖²) + 2 n ρ' (‖x‖²). In polar coordinates the weak harmonicity ∫ Δχ • u = 0 becomes ∫ 2 ψ' • Φ = 0, so Φ is constant on (0, R) by the du Bois-Reymond lemma, and Φ R = Φ 0 = μ.toSphere(S) • u 0 by continuity. No divergence theorem is needed.

Provenance #

Pool port: imports relocated under LeanPool.ViscositySolutionTheory; original mathematical namespaces and copyright retained; checked with Lean/Mathlib v4.34.0.

source
def ViscositySolns.Analysis.WeaklyHarmonicOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure E) (u : E → F) (U : Set E) :
Prop

u is weakly harmonic in U (for the measure μ): ∫ Δχ • u ∂μ = 0 for every smooth χ : E → ℝ with compact support in U.

Equations
Instances For
    source
    theorem ViscositySolns.Analysis.weaklyHarmonic_comp_add_right {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] {u : E → F} {U : Set E} (hu : WeaklyHarmonicOn μ u U) (x₀ : E) :
    WeaklyHarmonicOn μ (fun (y : E) => u (y + x₀)) ((fun (x : E) => x + x₀) ⁻¹' U)

    Weak harmonicity is translation invariant.

    source
    theorem ViscositySolns.Analysis.integral_deriv_smul_integral_toSphere_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] {u : E → F} {R : ℝ} {U : Set E} [Nontrivial E] (hU : IsOpen U) (hcont : ContinuousOn u U) (hu : WeaklyHarmonicOn μ u U) (hΩ : Metric.closedBall 0 R ⊆ U) (hR : 0 < R) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψs : tsupport ψ ⊆ Set.Ioo 0 R) :
    ∫ (s : ℝ), deriv ψ s • ∫ (θ : ↑(Metric.sphere 0 1)), u (s • ↑θ) ∂μ.toSphere = 0

    The distributional derivative of the sphere integrals s ↦ ∫ θ, u (s • θ) ∂μ.toSphere of a continuous weakly harmonic function vanishes on (0, R): ∫ ψ' • Φ = 0 for every test function ψ on (0, R).

    source
    theorem ViscositySolns.Analysis.integral_toSphere_eq_of_weaklyHarmonic_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {u : E → F} {R : ℝ} {U : Set E} [Nontrivial E] (hU : IsOpen U) (hcont : ContinuousOn u U) (hu : WeaklyHarmonicOn μ u U) (hΩ : Metric.closedBall 0 R ⊆ U) (hR : 0 ≤ R) :
    ∫ (θ : ↑(Metric.sphere 0 1)), u (R • ↑θ) ∂μ.toSphere = μ.toSphere.real Set.univ • u 0

    The mean-value property on spheres about the origin.

    source
    theorem ViscositySolns.Analysis.integral_toSphere_eq_of_weaklyHarmonic {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {u : E → F} {R : ℝ} {U : Set E} [Nontrivial E] (hU : IsOpen U) (hcont : ContinuousOn u U) (hu : WeaklyHarmonicOn μ u U) {x₀ : E} (hΩ : Metric.closedBall x₀ R ⊆ U) (hR : 0 ≤ R) :
    ∫ (θ : ↑(Metric.sphere 0 1)), u (x₀ + R • ↑θ) ∂μ.toSphere = μ.toSphere.real Set.univ • u x₀

    The mean-value property on spheres for a continuous weakly harmonic function: if closedBall x₀ R ⊆ U and 0 ≤ R, the integral of u over the sphere of radius R about x₀, parametrized by the unit sphere with the surface measure μ.toSphere, is the total surface measure times u x₀.

    source
    theorem ViscositySolns.Analysis.integral_radial_smul_eq_of_weaklyHarmonic {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {u : E → F} {R : ℝ} {U : Set E} [Nontrivial E] (hU : IsOpen U) (hcont : ContinuousOn u U) (hu : WeaklyHarmonicOn μ u U) {x₀ : E} (hΩ : Metric.closedBall x₀ R ⊆ U) {k : ℝ → ℝ} (hk : Continuous k) (hkR : ∀ (r : ℝ), R < r → k r = 0) :
    ∫ (y : E), k ‖y‖ • u (x₀ + y) ∂μ = (∫ (y : E), k ‖y‖ ∂μ) • u x₀

    Reproduction by radial kernels. If u is continuous and weakly harmonic in U, closedBall x₀ R ⊆ U, and k : ℝ → ℝ is continuous and vanishes on (R, ∞), then ∫ k ‖y‖ • u (x₀ + y) ∂μ = (∫ k ‖y‖ ∂μ) • u x₀.