Documentation

Mathlib.Analysis.InnerProductSpace.Laplacian

The Laplacian #

This file defines the Laplacian for functions f : E → F on real, finite-dimensional, inner product spaces E. In essence, we define the Laplacian of f as the second derivative, applied to the canonical covariant tensor of E, as defined and discussed in Mathlib.Analysis.InnerProductSpace.CanonicalTensor.

We show that the Laplacian is ℝ-linear on continuously differentiable functions, and establish the standard formula for computing the Laplacian in terms of orthonormal bases of E.

Supporting API #

The definition of the Laplacian of a function f : E → F involves the notion of the second derivative, which can be seen as a continuous multilinear map ContinuousMultilinearMap 𝕜 (fun (i : Fin 2) ↦ E) F, a bilinear map E →ₗ[𝕜] E →ₗ[𝕜] F, or a linear map on tensors E ⊗[𝕜] E →ₗ[𝕜] F. This section provides convenience API to convert between these notions.

noncomputable def bilinearIteratedFDerivWithinTwo (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (s : Set E) :

E → E →ₗ[𝕜] E →ₗ[𝕜] F

Convenience reformulation of the second iterated derivative, as a map from E to bilinear maps `E →ₗ[ℝ] E →ₗ[ℝ] ℝ

Equations

bilinearIteratedFDerivWithinTwo 𝕜 f s x = (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x).toLinearMap₂

Instances For

noncomputable def bilinearIteratedFDerivTwo (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) :

E → E →ₗ[𝕜] E →ₗ[𝕜] F

Convenience reformulation of the second iterated derivative, as a map from E to bilinear maps `E →ₗ[ℝ] E →ₗ[ℝ] ℝ

Equations

bilinearIteratedFDerivTwo 𝕜 f x = (fderiv 𝕜 (fderiv 𝕜 f) x).toLinearMap₂

Instances For

theorem bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {e : E} {s : Set E} (f : E → F) (hs : UniqueDiffOn 𝕜 s) (he : e ∈ s) (e₁ e₂ : E) :

((bilinearIteratedFDerivWithinTwo 𝕜 f s e) e₁) e₂ = (iteratedFDerivWithin 𝕜 2 f s e) ![e₁, e₂]

Expression of bilinearIteratedFDerivWithinTwo in terms of iteratedFDerivWithin.

theorem bilinearIteratedFDerivTwo_eq_iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (e e₁ e₂ : E) :

((bilinearIteratedFDerivTwo 𝕜 f e) e₁) e₂ = (iteratedFDeriv 𝕜 2 f e) ![e₁, e₂]

Expression of bilinearIteratedFDerivTwo in terms of iteratedFDeriv.

noncomputable def tensorIteratedFDerivWithinTwo (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (s : Set E) :

E → TensorProduct 𝕜 E E →ₗ[𝕜] F

Convenience reformulation of the second iterated derivative, as a map from E to linear maps E ⊗[𝕜] E →ₗ[𝕜] F.

Equations

tensorIteratedFDerivWithinTwo 𝕜 f s e = TensorProduct.lift (bilinearIteratedFDerivWithinTwo 𝕜 f s e)

Instances For

noncomputable def tensorIteratedFDerivTwo (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) :

E → TensorProduct 𝕜 E E →ₗ[𝕜] F

Convenience reformulation of the second iterated derivative, as a map from E to linear maps E ⊗[𝕜] E →ₗ[𝕜] F.

Equations

tensorIteratedFDerivTwo 𝕜 f e = TensorProduct.lift (bilinearIteratedFDerivTwo 𝕜 f e)

Instances For

theorem tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {e : E} {s : Set E} (f : E → F) (hs : UniqueDiffOn 𝕜 s) (he : e ∈ s) (e₁ e₂ : E) :

(tensorIteratedFDerivWithinTwo 𝕜 f s e) (e₁ ⊗ₜ[𝕜] e₂) = (iteratedFDerivWithin 𝕜 2 f s e) ![e₁, e₂]

Expression of tensorIteratedFDerivTwo in terms of iteratedFDerivWithin.

theorem tensorIteratedFDerivTwo_eq_iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (e e₁ e₂ : E) :

(tensorIteratedFDerivTwo 𝕜 f e) (e₁ ⊗ₜ[𝕜] e₂) = (iteratedFDeriv 𝕜 2 f e) ![e₁, e₂]

Expression of tensorIteratedFDerivTwo in terms of iteratedFDeriv.

Definition of the Laplacian #

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

E → F

Laplacian for functions on real inner product spaces, with respect to a set s. Use open InnerProductSpace to access the notation Δ[s] for InnerProductSpace.LaplacianWithin.

Equations

InnerProductSpace.laplacianWithin f s x = (tensorIteratedFDerivWithinTwo ℝ f s x) (InnerProductSpace.canonicalCovariantTensor E)

Instances For

def InnerProductSpace.«termΔ[_]_» :

Lean.ParserDescr

Laplacian for functions on real inner product spaces, with respect to a set s. Use open InnerProductSpace to access the notation Δ[s] for InnerProductSpace.LaplacianWithin.

Equations

One or more equations did not get rendered due to their size.

Instances For

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

E → F

Laplacian for functions on real inner product spaces. Use open InnerProductSpace to access the notation Δ for InnerProductSpace.Laplacian.

Equations

InnerProductSpace.laplacian f x = (tensorIteratedFDerivTwo ℝ f x) (InnerProductSpace.canonicalCovariantTensor E)

Instances For

def InnerProductSpace.termΔ :

Lean.ParserDescr

Laplacian for functions on real inner product spaces. Use open InnerProductSpace to access the notation Δ for InnerProductSpace.Laplacian.

Equations

InnerProductSpace.termΔ = Lean.ParserDescr.node `InnerProductSpace.termΔ 1024 (Lean.ParserDescr.symbol "Δ")

Instances For

@[simp]

theorem InnerProductSpace.laplacianWithin_univ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} :

laplacianWithin f Set.univ = laplacian f

The Laplacian equals the Laplacian with respect to Set.univ.

Computation of Δ in Terms of Orthonormal Bases #

theorem InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) {s : Set E} {ι : Type u_4} [Fintype ι] {e : E} (hs : UniqueDiffOn ℝ s) (he : e ∈ s) (v : OrthonormalBasis ι ℝ E) :

laplacianWithin f s e = ∑ i : ι, (iteratedFDerivWithin ℝ 2 f s e) ![v i, v i]

Standard formula, computing the Laplacian from any orthonormal basis.

theorem InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) {ι : Type u_4} [Fintype ι] (v : OrthonormalBasis ι ℝ E) :

laplacian f = fun (x : E) => ∑ i : ι, (iteratedFDeriv ℝ 2 f x) ![v i, v i]

Standard formula, computing the Laplacian from any orthonormal basis.

theorem InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) {s : Set E} {e : E} (hs : UniqueDiffOn ℝ s) (he : e ∈ s) :

laplacianWithin f s e = ∑ i : Fin (Module.finrank ℝ E), (iteratedFDerivWithin ℝ 2 f s e) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i]

Standard formula, computing the Laplacian from the standard orthonormal basis of a real inner product space.

theorem InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) :

laplacian f = fun (x : E) => ∑ i : Fin (Module.finrank ℝ E), (iteratedFDeriv ℝ 2 f x) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i]

Standard formula, computing the Laplacian from the standard orthonormal basis of a real inner product space.

theorem InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_complexPlane {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {e : ℂ} {s : Set ℂ} (f : ℂ → F) (hs : UniqueDiffOn ℝ s) (he : e ∈ s) :

laplacianWithin f s e = (iteratedFDerivWithin ℝ 2 f s e) ![1, 1] + (iteratedFDerivWithin ℝ 2 f s e) ![Complex.I , Complex.I ]

Special case of the standard formula for functions on ℂ, with the standard real inner product structure.

theorem InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : ℂ → F) :

laplacian f = fun (x : ℂ) => (iteratedFDeriv ℝ 2 f x) ![1, 1] + (iteratedFDeriv ℝ 2 f x) ![Complex.I , Complex.I ]

Special case of the standard formula for functions on ℂ, with the standard real inner product structure.

Congruence Lemmata for Δ #

theorem InnerProductSpace.laplacianWithin_congr_nhdsWithin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E} {s : Set E} (h : f₁ =ᶠ[nhdsWithin x s] f₂) (hs : UniqueDiffOn ℝ s) :

laplacianWithin f₁ s =ᶠ[nhdsWithin x s] laplacianWithin f₂ s

If two functions agree in a neighborhood of a point, then so do their Laplacians.

theorem InnerProductSpace.laplacian_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₂) :

laplacian f₁ =ᶠ[nhds x] laplacian f₂

If two functions agree in a neighborhood of a point, then so do their Laplacians.

ℝ-Linearity of Δ on Continuously Differentiable Functions #

theorem ContDiffWithinAt.laplacianWithin_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} {s : Set E} (h₁ : ContDiffWithinAt ℝ 2 f₁ s x) (h₂ : ContDiffWithinAt ℝ 2 f₂ s x) (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) :

InnerProductSpace.laplacianWithin (f₁ + f₂) s x = InnerProductSpace.laplacianWithin f₁ s x + InnerProductSpace.laplacianWithin f₂ s x

The Laplacian commutes with addition.

theorem ContDiffAt.laplacian_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₁ : ContDiffAt ℝ 2 f₁ x) (h₂ : ContDiffAt ℝ 2 f₂ x) :

InnerProductSpace.laplacian (f₁ + f₂) x = InnerProductSpace.laplacian f₁ x + InnerProductSpace.laplacian f₂ x

The Laplacian commutes with addition.

theorem ContDiffAt.laplacianWithin_add_nhdsWithin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E} {s : Set E} (h₁ : ContDiffWithinAt ℝ 2 f₁ s x) (h₂ : ContDiffWithinAt ℝ 2 f₂ s x) (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) :

InnerProductSpace.laplacianWithin (f₁ + f₂) s =ᶠ[nhdsWithin x s] InnerProductSpace.laplacianWithin f₁ s + InnerProductSpace.laplacianWithin f₂ s

The Laplacian commutes with addition.

theorem ContDiffAt.laplacian_add_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₁ : ContDiffAt ℝ 2 f₁ x) (h₂ : ContDiffAt ℝ 2 f₂ x) :

InnerProductSpace.laplacian (f₁ + f₂) =ᶠ[nhds x] InnerProductSpace.laplacian f₁ + InnerProductSpace.laplacian f₂

The Laplacian commutes with addition.

theorem InnerProductSpace.laplacianWithin_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} {s : Set E} (v : ℝ) (hf : ContDiffWithinAt ℝ 2 f s x) (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) :

laplacianWithin (v • f) s x = v • laplacianWithin f s x

The Laplacian commutes with scalar multiplication.

theorem InnerProductSpace.laplacian_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} (v : ℝ) (hf : ContDiffAt ℝ 2 f x) :

laplacian (v • f) x = v • laplacian f x

The Laplacian commutes with scalar multiplication.

theorem InnerProductSpace.laplacianWithin_smul_nhds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} {s : Set E} (v : ℝ) (hf : ContDiffWithinAt ℝ 2 f s x) (hs : UniqueDiffOn ℝ s) :

laplacianWithin (v • f) s =ᶠ[nhdsWithin x s] v • laplacianWithin f s

The Laplacian commutes with scalar multiplication.

theorem InnerProductSpace.laplacian_smul_nhds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} (v : ℝ) (h : ContDiffAt ℝ 2 f x) :

laplacian (v • f) =ᶠ[nhds x] v • laplacian f

The Laplacian commutes with scalar multiplication.

Commutativity of Δ with Linear Operators #

This section establishes commutativity with linear operators, showing in particular that Δ commutes with taking real and imaginary parts of complex-valued functions.

theorem ContDiffWithinAt.laplacianWithin_CLM_comp_left {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} {s : Set E} {l : F →L[ℝ ] G} (h : ContDiffWithinAt ℝ 2 f s x) (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) :

InnerProductSpace.laplacianWithin (⇑l ∘ f) s x = (⇑l ∘ InnerProductSpace.laplacianWithin f s) x

The Laplacian commutes with left composition by continuous linear maps.

theorem ContDiffAt.laplacian_CLM_comp_left {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} (h : ContDiffAt ℝ 2 f x) :

InnerProductSpace.laplacian (⇑l ∘ f) x = (⇑l ∘ InnerProductSpace.laplacian f) x

The Laplacian commutes with left composition by continuous linear maps.

theorem ContDiffWithinAt.laplacianWithin_CLM_comp_left_nhds {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} {s : Set E} {l : F →L[ℝ ] G} (h : ContDiffWithinAt ℝ 2 f s x) (hs : UniqueDiffOn ℝ s) :

InnerProductSpace.laplacianWithin (⇑l ∘ f) s =ᶠ[nhdsWithin x s] ⇑l ∘ InnerProductSpace.laplacianWithin f s

The Laplacian commutes with left composition by continuous linear maps.

theorem ContDiffAt.laplacian_CLM_comp_left_nhds {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} (h : ContDiffAt ℝ 2 f x) :

InnerProductSpace.laplacian (⇑l ∘ f) =ᶠ[nhds x] ⇑l ∘ InnerProductSpace.laplacian f

The Laplacian commutes with left composition by continuous linear maps.

theorem InnerProductSpace.laplacianWithin_CLE_comp_left {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} {s : Set E} {l : F ≃L[ℝ ] G} (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) :

laplacianWithin (⇑l ∘ f) s x = (⇑l ∘ laplacianWithin f s) x

The Laplacian commutes with left composition by continuous linear equivalences.

theorem InnerProductSpace.laplacian_CLE_comp_left {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} {l : F ≃L[ℝ ] G} :

laplacian (⇑l ∘ f) = ⇑l ∘ laplacian f

The Laplacian commutes with left composition by continuous linear equivalences.