Uniqueness for continuous decaying weakly harmonic functions #
Continuity and decay at infinity imply a globally bounded range.
A continuous weakly harmonic function decaying at infinity vanishes.
theorem
LiebThirring.eq_zero_of_weak_laplacian_of_tendsto
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
[Nontrivial E]
[MeasurableSpace E]
[BorelSpace E]
{μ : MeasureTheory.Measure E}
[μ.IsAddHaarMeasure]
{w : E → ℝ}
(hw : Continuous w)
(hweak : ∀ (f : E → ℝ), ContDiff ℝ (↑⊤) f → HasCompactSupport f → ∫ (x : E), w x * Laplacian.laplacian f x ∂μ = 0)
(hd : Filter.Tendsto w (Filter.cocompact E) (nhds 0))
:
A continuous weakly harmonic function decaying at infinity vanishes.
theorem
LiebThirring.weak_harmonic_eq_zero
{w : Position → ℝ}
(hw : Continuous w)
(hweak :
∀ (f : Position → ℝ), ContDiff ℝ (↑⊤) f → HasCompactSupport f → ∫ (x : Position), w x * Laplacian.laplacian f x = 0)
(hd : Filter.Tendsto w (Filter.cocompact Position) (nhds 0))
:
harmonic uniqueness on the three-dimensional carrier.