Invariance of the Laplacian and radial Laplacians (ported from TauCeti)

For a finite-dimensional real inner product space E and any f : E → F:

• laplacian_comp_linearIsometryEquiv_right: Δ (f ∘ l) = (Δ f) ∘ l for a linear isometry equivalence l;
• laplacian_comp_add_right: Δ (fun y ↦ f (y + a)) = fun y ↦ Δ f (y + a);
• ContDiff.laplacian_comp_norm_sq: for ρ : ℝ → ℝ of class C², Δ (fun y ↦ ρ (‖y‖²)) x = 4 ‖x‖² ρ'' (‖x‖²) + 2 (dim E) ρ' (‖x‖²);
• tsupport_laplacian_subset: tsupport (Δ f) ⊆ tsupport f.

The invariance statements need no differentiability hypothesis on f.

Provenance

Pool port: imports relocated under LeanPool.ViscositySolutionTheory; original mathematical namespaces and copyright retained; checked with Lean/Mathlib v4.34.0.

• Upstream: TauCeti, https://github.com/TauCetiProject/TauCeti
• Path: TauCeti/Analysis/InnerProductSpace/Laplacian/Basic.lean
• Commit: 91f66a0514e6523efdccddb9e35fb82c96dd6405 (2026-09-24)
• License: Apache-2.0. Upstream NOTICE: none.
• Upstream notice: Copyright (c) 2026 The Tau Ceti contributors. All rights reserved.; upstream authors: The Tau Ceti contributors.
• Extent: iteratedFDeriv_comp_linearIsometryEquiv_apply, laplacian_comp_linearIsometryEquiv_right, laplacian_comp_add_right, ContDiff.laplacian_comp_norm_sq, tsupport_laplacian_subset (verbatim up to namespace).
• Changes: ported from Lean v4.34.0-rc2 to Lean/Mathlib v4.30.0; module/public import removed; namespace TauCeti → ViscositySolns.Analysis; the affine-isometry, homothety and laplacian_norm_sq statements are not ported (not needed here).

theorem ViscositySolns.Analysis.iteratedFDeriv_comp_linearIsometryEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (l : E ≃ₗᵢ[ℝ] E') (f : E' → F) (i : ℕ) (x : E) (m : Fin i → E) : (iteratedFDeriv ℝ i (f ∘ ⇑l) x) m = (iteratedFDeriv ℝ i f (l x)) fun (j : Fin i) => l (m j)

The iterated derivative transforms under a linear isometry equivalence on the right by pulling the directions through the isometry.

theorem ViscositySolns.Analysis.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

Invariance of the Laplacian under isometries. Δ (f ∘ l) = (Δ f) ∘ l for a linear isometry equivalence l. No differentiability hypothesis is needed.

theorem ViscositySolns.Analysis.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. No differentiability hypothesis is needed.

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 ViscositySolns.Analysis.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.