Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhi Kai Pong, Joseph Tooby-Smith, Lode Vermeulen
-/
module
public import Physlib.SpaceAndTime.Space.Derivatives.Div
The Laplacian operator on Space d
i. Overview
In this module we define the Laplacian operator on functions and vector-valued
functions defined on Space d.
ii. Key results
laplacian : The Laplacian operator on scalar functions on Space d.
laplacianVec : The Laplacian operator on vector-valued functions on Space d.
distLaplacian : The Laplacian operator on distributions on Space d.
iii. Table of contents
A. Laplacian on functions to ℝ
A.1. Relation between laplacian and divergence of gradient
B. Laplacian on vector valued functions
C. Laplacian of distributions
C.1. Laplacian of constant distributions
iv. References
@[expose] public sectionA. Laplacian on functions to ℝ
A.1. Relation between laplacian and divergence of gradient
lemma laplacian_eq_sum_snd_deriv {d} (f : Space d → ℝ) :
Δ f = fun x => ∑ i, ∂[i] (∂[i] f) x := d:ℕf:Space d → ℝ⊢ Δ f = fun x => ∑ i, deriv i (deriv i f) x
d:ℕf:Space d → ℝ⊢ (fun x => ∑ i, deriv i (fun x => (WithLp.toLp 2 fun i => deriv i f x).ofLp i) x) = fun x => ∑ i, deriv i (deriv i f) x
All goals completed! 🐙B. Laplacian on vector valued functions
@[inherit_doc laplacianVec]
scoped[Space] notation "Δᵥ" => laplacianVecC. Laplacian of distributions
@[inherit_doc distLaplacian]
scoped[Space] notation "Δᵈ" => distLaplacianC.1. Laplacian of constant distributions
@[simp]
lemma distLaplacian_const {d : ℕ} (c : ℝ) :
Δᵈ (Distribution.const ℝ (Space d) c) = 0 := d:ℕc:ℝ⊢ Δᵈ (const ℝ (Space d) c) = 0
All goals completed! 🐙