Geometric invariance of harmonic functions

TauCeti/Analysis/InnerProductSpace/Laplacian/Basic.lean proves that the Laplacian Δ is invariant under the rigid motions of a Euclidean space — affine isometry equivalences, with linear isometry equivalences and translations as special cases. This file transports that invariance to harmonic functions.

Smoothness enters here, where the ContDiffAt half of InnerProductSpace.HarmonicAt is transported across the equivalence: harmonicity is invariant under the full isometry group, the symmetry that underlies the mean-value property and the construction of radial harmonic functions (PDE roadmap, Lane C, item 12).

Main declarations

• TauCeti.harmonicAt_comp_affineIsometryEquiv_right_iff, TauCeti.harmonicOnNhd_comp_affineIsometryEquiv_right_iff: harmonicity is invariant under affine isometry equivalences.
• TauCeti.harmonicAt_comp_linearIsometryEquiv_right_iff, TauCeti.harmonicOnNhd_comp_linearIsometryEquiv_right_iff: harmonicity is invariant under linear isometric changes of variable.
• TauCeti.harmonicAt_comp_add_right_iff, TauCeti.harmonicOnNhd_comp_add_right_iff: harmonicity is invariant under translation.

theorem TauCeti.harmonicAt_comp_linearIsometryEquiv_right_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] [FiniteDimensional ℝ E'] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (l : E ≃ₗᵢ[ℝ] E') {f : E' → F} {x : E} : InnerProductSpace.HarmonicAt (f ∘ ⇑l) x ↔ InnerProductSpace.HarmonicAt f (l x)

Harmonicity is invariant under isometric changes of variable. For a linear isometry equivalence l, the function f ∘ l is harmonic at x iff f is harmonic at l x.

theorem TauCeti.harmonicAt_comp_add_right_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x a : E} : InnerProductSpace.HarmonicAt (fun (y : E) => f (y + a)) x ↔ InnerProductSpace.HarmonicAt f (x + a)

Harmonicity is invariant under translation. The function y ↦ f (y + a) is harmonic at x iff f is harmonic at x + a.

theorem TauCeti.harmonicAt_comp_affineIsometryEquiv_right_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] [FiniteDimensional ℝ E'] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ᵃⁱ[ℝ] E') {f : E' → F} {x : E} : InnerProductSpace.HarmonicAt (f ∘ ⇑e) x ↔ InnerProductSpace.HarmonicAt f (e x)

Harmonicity is invariant under affine isometries. For an affine isometry equivalence e, the function f ∘ e is harmonic at x iff f is harmonic at e x.

theorem TauCeti.harmonicOnNhd_comp_affineIsometryEquiv_right_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] [FiniteDimensional ℝ E'] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ᵃⁱ[ℝ] E') {f : E' → F} {s : Set E'} : InnerProductSpace.HarmonicOnNhd (f ∘ ⇑e) (⇑e ⁻¹' s) ↔ InnerProductSpace.HarmonicOnNhd f s

Harmonicity on a neighbourhood of a set is invariant under an affine isometry equivalence.

theorem TauCeti.harmonicOnNhd_comp_linearIsometryEquiv_right_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] [FiniteDimensional ℝ E'] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (l : E ≃ₗᵢ[ℝ] E') {f : E' → F} {s : Set E'} : InnerProductSpace.HarmonicOnNhd (f ∘ ⇑l) (⇑l ⁻¹' s) ↔ InnerProductSpace.HarmonicOnNhd f s

Harmonicity on a neighbourhood of a set is invariant under a linear isometric change of variable.

theorem TauCeti.harmonicOnNhd_comp_add_right_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} (a : E) : InnerProductSpace.HarmonicOnNhd (fun (y : E) => f (y + a)) ((fun (y : E) => y + a) ⁻¹' s) ↔ InnerProductSpace.HarmonicOnNhd f s

Harmonicity on a neighbourhood of a set is invariant under translation.