Locally uniform limits of harmonic functions #
Let E be a finite-dimensional real inner product space. This file proves that a locally uniform
limit of harmonic functions E → ℝ on an open set U is harmonic. The limit is continuous and
inherits the mean-value property on small balls, so it is harmonic by the converse of the
mean-value property (TauCeti.harmonicOnNhd_of_setAverage_ball_eq).
Main declarations #
TauCeti.harmonicOnNhd_of_tendstoLocallyUniformlyOn: a locally uniform limit of harmonic functions is harmonic.
References #
- D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 2.8.
- L. C. Evans, Partial Differential Equations, Section 2.2.3.
theorem
TauCeti.harmonicOnNhd_of_tendstoLocallyUniformlyOn
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{ι : Type u_2}
{F : ι → E → ℝ}
{f : E → ℝ}
{U : Set E}
{p : Filter ι}
[p.NeBot]
(hU : IsOpen U)
(hF : ∀ᶠ (i : ι) in p, InnerProductSpace.HarmonicOnNhd (F i) U)
(hlim : TendstoLocallyUniformlyOn F f p U)
:
Locally uniform limits of harmonic functions are harmonic. If eventually along a nontrivial
filter p the functions F i are harmonic on the open set U, and F i tends to f locally
uniformly on U, then f is harmonic on U.