Documentation

TauCeti.Analysis.InnerProductSpace.Harmonic.Dilation

Dilation invariance of the Laplacian and harmonic functions #

TauCeti.Analysis.InnerProductSpace.Laplacian.Basic records invariance under rigid motions and the Laplacian scaling law under affine homotheties. This file transports the homothety bookkeeping to harmonicity: under the right-composition AffineMap.homothety a c, harmonicity is preserved and reflected when c ≠ 0.

These lemmas are a small Lane C prerequisite from the PDE roadmap. They let later mean-value, maximum-principle, and Poisson-kernel arguments normalize balls by translating and rescaling without reproving the Laplacian calculation each time.

Main declarations #

source
theorem TauCeti.harmonicAt_comp_homothety_right_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (a : E) (c : ℝ) (hc : c ≠ 0) {f : E → F} {x : E} :
InnerProductSpace.HarmonicAt (fun (y : E) => f ((AffineMap.homothety a c) y)) x ↔ InnerProductSpace.HarmonicAt f ((AffineMap.homothety a c) x)

Harmonicity is invariant under nonzero homothety.

For c ≠ 0, the function y ↦ f (AffineMap.homothety a c y) is harmonic at x iff f is harmonic at AffineMap.homothety a c x.

source
theorem TauCeti.harmonicOnNhd_comp_homothety_right_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (a : E) (c : ℝ) (hc : c ≠ 0) {f : E → F} {s : Set E} :
InnerProductSpace.HarmonicOnNhd (fun (y : E) => f ((AffineMap.homothety a c) y)) ((fun (y : E) => (AffineMap.homothety a c) y) ⁻¹' s) ↔ InnerProductSpace.HarmonicOnNhd f s

Harmonicity on a neighbourhood of a set is invariant under nonzero homothety.

source
theorem TauCeti.harmonicAt_comp_smul_right_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (hc : c ≠ 0) {f : E → F} {x : E} :
InnerProductSpace.HarmonicAt (fun (y : E) => f (c • y)) x ↔ InnerProductSpace.HarmonicAt f (c • x)

Harmonicity is invariant under nonzero dilation.

For c ≠ 0, the function x ↦ f (c • x) is harmonic at x iff f is harmonic at c • x.

source
theorem TauCeti.harmonicOnNhd_comp_smul_right_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (hc : c ≠ 0) {f : E → F} {s : Set E} :
InnerProductSpace.HarmonicOnNhd (fun (y : E) => f (c • y)) ((fun (y : E) => c • y) ⁻¹' s) ↔ InnerProductSpace.HarmonicOnNhd f s

Harmonicity on a neighbourhood of a set is invariant under nonzero dilation.

source
theorem TauCeti.harmonicAt_comp_const_add_smul_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (x : E) {c : ℝ} (hc : c ≠ 0) {f : E → F} {y : E} :
InnerProductSpace.HarmonicAt (fun (z : E) => f (x + c • z)) y ↔ InnerProductSpace.HarmonicAt f (x + c • y)

Harmonicity is invariant under the affine normalization z ↦ x + c • z when the scale is nonzero.

For c ≠ 0, the function z ↦ f (x + c • z) is harmonic at y iff f is harmonic at x + c • y.

source
theorem TauCeti.harmonicOnNhd_comp_const_add_smul_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (x : E) {c : ℝ} (hc : c ≠ 0) {f : E → F} {s : Set E} :
InnerProductSpace.HarmonicOnNhd (fun (z : E) => f (x + c • z)) ((fun (z : E) => x + c • z) ⁻¹' s) ↔ InnerProductSpace.HarmonicOnNhd f s

Harmonicity on a neighbourhood of a set is invariant under the affine normalization z ↦ x + c • z when the scale is nonzero.

For c ≠ 0, the function z ↦ f (x + c • z) is harmonic near (fun z ↦ x + c • z) ⁻¹' s iff f is harmonic near s.