Harmonic Functions

This file defines harmonic functions on real, finite-dimensional, inner product spaces E.

Definition

def InnerProductSpace.HarmonicAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (x : E) : Prop

Let E be a real, finite-dimensional, inner product space and x be a point of E. A function f on E is harmonic at x if it is two times continuously ℝ-differentiable and if its Laplacian vanishes in a neighborhood of x.

def InnerProductSpace.HarmonicOnNhd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (s : Set E) : Prop

Let E be a real, finite-dimensional, inner product space and s be a subset of E. A function f on E is harmonic in a neighborhood of s if it is harmonic at every point of s.

theorem InnerProductSpace.HarmonicOnNhd.contDiffOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} (hf : HarmonicOnNhd f s) : ContDiffOn ℝ 2 f s

Harmonic functions are two times continuously differentiable.

Elementary Properties

theorem InnerProductSpace.harmonicAt_congr_nhds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f₂) : HarmonicAt f₁ x ↔ HarmonicAt f₂ x

If two functions agree in a neighborhood of x, then one is harmonic at x iff so is the other.

theorem InnerProductSpace.HarmonicAt.eventually {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} (h : HarmonicAt f x) : ∀ᶠ (y : E) in nhds x, HarmonicAt f y

If f is harmonic at x, then it is harmonic at all points in a neighborhood of x.

@[simp]

theorem InnerProductSpace.harmonicAt_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {x : E} (c : F) : HarmonicAt (fun (x : E) => c) x

Constant functions are harmonic

@[simp]

theorem InnerProductSpace.harmonicOnNhd_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} (c : F) : HarmonicOnNhd (fun (x : E) => c) s

Constant functions are harmonic

theorem InnerProductSpace.isOpen_setOf_harmonicAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) : IsOpen {x : E | HarmonicAt f x}

Harmonicity is an open property.

theorem InnerProductSpace.HarmonicOnNhd.mono {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s t : Set E} (h : HarmonicOnNhd f s) (hst : t ⊆ s) : HarmonicOnNhd f t

If f is harmonic in a neighborhood of s, it is harmonic in a neighborhood of every subset.

theorem InnerProductSpace.HarmonicOnNhd.continuousOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} (h : HarmonicOnNhd f s) : ContinuousOn f s

Harmonic functions are continuous.

Vector Space Structure

theorem InnerProductSpace.HarmonicAt.add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E} (h₁ : HarmonicAt f₁ x) (h₂ : HarmonicAt f₂ x) : HarmonicAt (f₁ + f₂) x

Sums of harmonic functions are harmonic.

theorem InnerProductSpace.HarmonicAt.sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E} (h₁ : HarmonicAt f₁ x) (h₂ : HarmonicAt f₂ x) : HarmonicAt (f₁ - f₂) x

Differences of harmonic functions are harmonic.

theorem InnerProductSpace.HarmonicOnNhd.add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f₁ f₂ : E → F} {s : Set E} (h₁ : HarmonicOnNhd f₁ s) (h₂ : HarmonicOnNhd f₂ s) : HarmonicOnNhd (f₁ + f₂) s

Sums of harmonic functions are harmonic.

theorem InnerProductSpace.HarmonicOnNhd.sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f₁ f₂ : E → F} {s : Set E} (h₁ : HarmonicOnNhd f₁ s) (h₂ : HarmonicOnNhd f₂ s) : HarmonicOnNhd (f₁ - f₂) s

Differences of harmonic functions are harmonic.

theorem InnerProductSpace.HarmonicAt.neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} (h : HarmonicAt f x) : HarmonicAt (-f) x

The negative of a harmonic function is harmonic.

theorem InnerProductSpace.HarmonicOnNhd.neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} (h : HarmonicOnNhd f s) : HarmonicOnNhd (-f) s

The negative of a harmonic function is harmonic.

theorem InnerProductSpace.HarmonicAt.const_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} {c : ℝ} (h : HarmonicAt f x) : HarmonicAt (c • f) x

Scalar multiples of harmonic functions are harmonic.

theorem InnerProductSpace.HarmonicOnNhd.const_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {c : ℝ} (h : HarmonicOnNhd f s) : HarmonicOnNhd (c • f) s

Scalar multiples of harmonic functions are harmonic.

Compatibility with Linear Maps

theorem InnerProductSpace.HarmonicAt.comp_CLM {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {x : E} (h : HarmonicAt f x) (l : F →L[ℝ] G) : HarmonicAt (⇑l ∘ f) x

Compositions of continuous ℝ-linear maps with harmonic functions are harmonic.

theorem InnerProductSpace.HarmonicOnNhd.comp_CLM {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {s : Set E} (h : HarmonicOnNhd f s) (l : F →L[ℝ] G) : HarmonicOnNhd (⇑l ∘ f) s

Compositions of continuous linear maps with harmonic functions are harmonic.

theorem InnerProductSpace.harmonicAt_comp_CLE_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {x : E} (l : F ≃L[ℝ] G) : HarmonicAt (⇑l ∘ f) x ↔ HarmonicAt f x

Functions are harmonic iff their compositions with continuous linear equivalences are harmonic.

theorem InnerProductSpace.harmonicOnNhd_comp_CLE_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {s : Set E} (l : F ≃L[ℝ] G) : HarmonicOnNhd (⇑l ∘ f) s ↔ HarmonicOnNhd f s

Functions are harmonic iff their compositions with continuous linear equivalences are harmonic.