Finite sums of harmonic functions #
Mathlib's InnerProductSpace.HarmonicAt.add and InnerProductSpace.HarmonicOnNhd.add show that
harmonic functions are closed under addition. This file extends this to finite sums.
Main declarations #
InnerProductSpace.HarmonicAt.sum,InnerProductSpace.HarmonicOnNhd.sum: a finite sum of harmonic functions is harmonic.
theorem
InnerProductSpace.HarmonicAt.sum
{E : Type u_1}
{F : Type u_2}
{ι : Type u_3}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : ι → E → F}
{u : Finset ι}
{x : E}
(h : ∀ i ∈ u, HarmonicAt (f i) x)
:
HarmonicAt (fun (y : E) => ∑ i ∈ u, f i y) x
A finite sum of functions harmonic at x is harmonic at x.
theorem
InnerProductSpace.HarmonicOnNhd.sum
{E : Type u_1}
{F : Type u_2}
{ι : Type u_3}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : ι → E → F}
{u : Finset ι}
{s : Set E}
(h : ∀ i ∈ u, HarmonicOnNhd (f i) s)
:
HarmonicOnNhd (fun (y : E) => ∑ i ∈ u, f i y) s
A finite sum of functions harmonic on a neighborhood of s is harmonic there.