Geometric invariance of the Laplacian

Mathlib's Mathlib/Analysis/InnerProductSpace/Laplacian.lean records that the Laplacian Δ commutes with left composition by a continuous linear map or equivalence acting on the values of a function (ContDiffAt.laplacian_CLM_comp_left, laplacian_CLE_comp_left). This file supplies the complementary right composition, acting on the domain variable: the geometric invariance of Δ under rigid motions and scalar homotheties of a Euclidean space: affine isometry equivalences, with orthogonal changes of variable (linear isometry equivalences) and translations as special cases, and affine homotheties with the expected quadratic scaling.

For an affine isometry equivalence e : E ≃ᵃⁱ[ℝ] E' and any f : E' → F,

Δ (f ∘ e) = (Δ f) ∘ e.

In particular, for a linear isometry equivalence l : E ≃ₗᵢ[ℝ] E',

Δ (f ∘ l) = (Δ f) ∘ l,

and for a translation by a : E,

Δ (fun y ↦ f (y + a)) = fun y ↦ (Δ f) (y + a).

All three identities hold with no differentiability hypothesis on f, because the underlying iteratedFDeriv composition laws are unconditional (the iterated derivative is junk-valued off the smooth locus, yet still transforms correctly under a linear change of variable). The harmonic corollaries, where smoothness re-enters, live in the companion files TauCeti/Analysis/InnerProductSpace/Harmonic/Isometry.lean and TauCeti/Analysis/InnerProductSpace/Harmonic/Dilation.lean.

The file also records the characterization laplacian_eq_traceL of the Laplacian as the trace of the second Fréchet derivative and the base second-derivative computation laplacian_norm_sq (Δ ‖x‖² = 2 · dim E), a reusable characteristic value of the Laplacian on the squared norm, its chain-rule generalization ContDiff.laplacian_comp_norm_sq to radial functions x ↦ ρ (‖x‖²), the Leibniz rules ContDiffAt.laplacian_fun_mul and ContDiffAt.laplacian_fun_smul for products with a scalar function, the companion rule ContDiffAt.laplacian_norm_sq for the squared norm of a vector-valued function, and the locality statement tsupport_laplacian_subset that Δ f vanishes wherever f vanishes identically.

Main declarations

• TauCeti.laplacian_comp_affineIsometryEquiv_right: Δ (f ∘ e) = (Δ f) ∘ e for an affine isometry equivalence e.
• TauCeti.laplacian_comp_linearIsometryEquiv_right: Δ (f ∘ l) = (Δ f) ∘ l for an isometry l.
• TauCeti.laplacian_comp_add_right: translation invariance of Δ.
• TauCeti.laplacian_comp_homothety_right: Δ scales by c ^ 2 under AffineMap.homothety a c.
• TauCeti.laplacian_comp_smul_right: the origin-centered homothety special case.
• TauCeti.laplacian_eq_traceL: the Laplacian as the trace of the second Fréchet derivative.
• TauCeti.laplacian_norm_sq: Δ (fun x => ‖x‖ ^ 2) x = 2 * dim E, the Laplacian of the squared norm.
• ContDiff.laplacian_comp_norm_sq: the Laplacian of a radial function x ↦ ρ (‖x‖ ^ 2) is 4 ‖x‖² ρ'' (‖x‖²) + 2 (dim E) ρ' (‖x‖²).
• ContDiffAt.laplacian_fun_mul: the Leibniz rule Δ (f g) = f Δg + 2 ⟪∇f, ∇g⟫ + g Δf.
• ContDiffAt.laplacian_fun_smul: its vector-valued form Δ (f • g) = f • Δg + 2 Dg(∇f) + Δf • g.
• ContDiffAt.laplacian_norm_sq: the Laplacian of a squared norm, Δ ‖f‖² = 2 ∑ᵢ ‖Df (bᵢ)‖² + 2 ⟪f, Δf⟫ for an orthonormal basis b.
• TauCeti.tsupport_laplacian_subset: tsupport (Δ f) ⊆ tsupport f.

theorem TauCeti.laplacian_eq_traceL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (x : E) : Laplacian.laplacian f x = (∑ i : Fin (Module.finrank ℝ E), (ContinuousLinearMap.apply ℝ F) ((stdOrthonormalBasis ℝ E) i) ∘SL (ContinuousLinearMap.apply ℝ (E →L[ℝ] F)) ((stdOrthonormalBasis ℝ E) i)) (fderiv ℝ (fderiv ℝ f) x)

The Laplacian of a function is the trace of its second Fréchet derivative, expressed as a continuous linear functional of fderiv ℝ (fderiv ℝ f) x in the standard orthonormal basis.

theorem TauCeti.laplacian_comp_linearIsometryEquiv_right {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) : Laplacian.laplacian (f ∘ ⇑l) = Laplacian.laplacian f ∘ ⇑l

Geometric invariance of the Laplacian under isometries. For a linear isometry equivalence l, the Laplacian commutes with right composition by l: Δ (f ∘ l) = (Δ f) ∘ l. No differentiability hypothesis is needed.

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

Translation invariance of the Laplacian. Shifting the argument by a constant a commutes with the Laplacian: Δ (fun y ↦ f (y + a)) = fun y ↦ (Δ f) (y + a). No differentiability hypothesis is needed.

theorem TauCeti.laplacian_comp_affineIsometryEquiv_right {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) : Laplacian.laplacian (f ∘ ⇑e) = Laplacian.laplacian f ∘ ⇑e

Geometric invariance of the Laplacian under affine isometries. For an affine isometry equivalence e, the Laplacian commutes with right composition by e: Δ (f ∘ e) = (Δ f) ∘ e. No differentiability hypothesis is needed.

theorem TauCeti.laplacian_comp_smul_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (f : E → F) : (Laplacian.laplacian fun (x : E) => f (c • x)) = fun (x : E) => c ^ 2 • Laplacian.laplacian f (c • x)

Scaling law for the Laplacian under origin-centered dilation.

Right-composition by x ↦ c • x multiplies the Laplacian by c ^ 2. The statement is unconditional in f, matching Mathlib's unconditional definition of Δ through iterated Fréchet derivatives.

theorem TauCeti.laplacian_comp_homothety_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (a : E) (c : ℝ) (f : E → F) : (Laplacian.laplacian fun (x : E) => f ((AffineMap.homothety a c) x)) = fun (x : E) => c ^ 2 • Laplacian.laplacian f ((AffineMap.homothety a c) x)

Scaling law for the Laplacian under a homothety.

Right-composition by AffineMap.homothety a c multiplies the Laplacian by c ^ 2.

@[simp]

theorem TauCeti.laplacian_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (x : E) : Laplacian.laplacian (fun (y : E) => ‖y‖ ^ 2) x = 2 * ↑(Module.finrank ℝ E)

The Laplacian of the squared norm on a finite-dimensional real inner product space is twice the dimension.

@[simp]

theorem ContDiff.laplacian_comp_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ρ : ℝ → ℝ} (hρ : ContDiff ℝ 2 ρ) (x : E) : Laplacian.laplacian (fun (y : E) => ρ (‖y‖ ^ 2)) x = 4 * ‖x‖ ^ 2 * deriv (deriv ρ) (‖x‖ ^ 2) + 2 * ↑(Module.finrank ℝ E) * deriv ρ (‖x‖ ^ 2)

The Laplacian of a radial function. For a C² function ρ : ℝ → ℝ, the Laplacian of x ↦ ρ (‖x‖ ^ 2) is 4 ‖x‖² ρ'' (‖x‖²) + 2 (dim E) ρ' (‖x‖²).

theorem ContDiffAt.laplacian_fun_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f g : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (hg : ContDiffAt ℝ 2 g x) : Laplacian.laplacian (fun (y : E) => f y * g y) x = f x * Laplacian.laplacian g x + 2 * Inner.inner ℝ (gradient f x) (gradient g x) + g x * Laplacian.laplacian f x

The Leibniz rule for the Laplacian. For scalar functions twice differentiable at x, Δ (f g) = f Δg + 2 ⟪∇f, ∇g⟫ + g Δf at x.

theorem ContDiffAt.laplacian_fun_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → ℝ} {g : E → F} {x : E} (hf : ContDiffAt ℝ 2 f x) (hg : ContDiffAt ℝ 2 g x) : Laplacian.laplacian (fun (y : E) => f y • g y) x = f x • Laplacian.laplacian g x + 2 • (fderiv ℝ g x) (gradient f x) + Laplacian.laplacian f x • g x

The Leibniz rule for the Laplacian, vector-valued form. For a scalar function f and a vector-valued function g, both twice differentiable at x, Δ (f • g) = f • Δg + 2 • Dg(∇f) + Δf • g at x.

theorem ContDiffAt.laplacian_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace ℝ G] {f : E → G} {x : E} (hf : ContDiffAt ℝ 2 f x) {ι : Type u_5} [Fintype ι] (b : OrthonormalBasis ι ℝ E) : Laplacian.laplacian (fun (y : E) => ‖f y‖ ^ 2) x = 2 * ∑ i : ι, ‖(fderiv ℝ f x) (b i)‖ ^ 2 + 2 * Inner.inner ℝ (f x) (Laplacian.laplacian f x)

The Laplacian of a squared norm. For a function f with values in a real inner product space, twice differentiable at x, and any orthonormal basis b of E, Δ ‖f‖² = 2 ∑ᵢ ‖Df (bᵢ)‖² + 2 ⟪f, Δf⟫ at x. The first term does not depend on b: it is twice the squared Hilbert--Schmidt norm of Df x.

theorem TauCeti.tsupport_laplacian_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) : tsupport (Laplacian.laplacian f) ⊆ tsupport f

The Laplacian vanishes wherever the function vanishes identically: Δ is local.