Add all-dimensional fundamental solution theorem (#1172)

Author: Lemmy00

Physlib/SpaceAndTime/Space/Derivatives/Grad.lean

@@ -48,7 +48,8 @@ of the input function with respect to each spatial coordinate.
   - B.3. The gradient as a sum over basis vectors
   - B.4. The underlying function of the gradient distribution
   - B.5. The gradient applied to a Schwartz function
-  - B.6. The gradident of a Schwartz map
+  - B.6. Gradient of constant distributions
+  - B.7. The gradient of a Schwartz map
 
 ## iv. References
 
@@ -609,7 +610,20 @@ lemma distGrad_apply {d} (f : (Space d) →d[ℝ] ℝ) (ε : 𝓢(Space d, ℝ))
 
 /-!
 
-### B.6. The gradident of a Schwartz map
+### B.6. Gradient of constant distributions
+
+-/
+
+@[simp]
+lemma distGrad_const {d} (c : ℝ) :
+    ∇ᵈ (Distribution.const ℝ (Space d) c) = 0 := by
+  ext ε i
+  simp only [distGrad_apply, distDeriv_apply]
+  simp [Distribution.fderivD_const]
+
+/-!
+
+### B.7. The gradient of a Schwartz map
 
 -/
 

Physlib/SpaceAndTime/Space/Derivatives/Laplacian.lean

@@ -19,12 +19,15 @@ functions defined on `Space d`.
 
 - `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
 
@@ -75,6 +78,12 @@ scoped[Space] notation "Δᵥ" => laplacianVec
 
 open Physlib Distribution
 
+/-!
+
+## C. Laplacian of distributions
+
+-/
+
 /-- The distributional `distLaplacian` operator. -/
 noncomputable def distLaplacian {d} :
     ((Space d) →d[ℝ] ℝ) →ₗ[ℝ] (Space d) →d[ℝ] ℝ :=
@@ -83,4 +92,15 @@ noncomputable def distLaplacian {d} :
 @[inherit_doc distLaplacian]
 scoped[Space] notation "Δᵈ" => distLaplacian
 
+/-!
+
+### C.1. Laplacian of constant distributions
+
+-/
+
+@[simp]
+lemma distLaplacian_const {d : ℕ} (c : ℝ) :
+    Δᵈ (Distribution.const ℝ (Space d) c) = 0 := by
+  simp [distLaplacian, distGrad_const]
+
 end Space

Physlib/SpaceAndTime/Space/Norm.lean

@@ -35,8 +35,8 @@ We use properties of this power series to prove various results about distributi
   of the norm.
 - `distDiv_inv_pow_eq_dim` : The divergence of the distribution defined by the
   inverse power of the norm proportional to the Dirac delta distribution.
-- `distLaplacian_fundamentalSolution_norm_zpow` : The Laplacian of the fundamental solution
-  power of the norm.
+- `distLaplacian_fundamentalSolution_norm_zpow_eq` : The Laplacian of the fundamental
+  solution power of the norm.
 
 ## iii. Table of contents
 
@@ -1464,4 +1464,37 @@ lemma distLaplacian_fundamentalSolution_norm_zpow {d : ℕ} :
   rw [smul_smul]
   ring_nf
 
+/-- Version of `distLaplacian_fundamentalSolution_norm_zpow` stated using the dimension of
+the ambient space. -/
+lemma distLaplacian_fundamentalSolution_norm_zpow_of_three_le {d : ℕ} (hd : 3 ≤ d) :
+    Δᵈ (distOfFunction (fun x : Space d => ‖x‖ ^ ((2 : ℤ) - (d : ℤ)))
+      (IsDistBounded.pow ((2 : ℤ) - (d : ℤ)) (by omega))) =
+      (((2 : ℝ) - (d : ℝ)) * (d : ℝ) *
+        (volume (α := Space d)).real (Metric.ball 0 1)) • diracDelta ℝ 0 := by
+  rcases d with _ | _ | _ | d
+  · omega
+  · omega
+  · omega
+  · convert distLaplacian_fundamentalSolution_norm_zpow (d := d) using 1
+    ext x
+    simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul]
+    simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one]
+    ring_nf
+
+/-- Version of `distLaplacian_fundamentalSolution_norm_zpow` stated for every dimension.
+In dimensions less than three, the exponent is zero and both sides are zero. -/
+lemma distLaplacian_fundamentalSolution_norm_zpow_eq {d : ℕ} :
+    Δᵈ (distOfFunction (fun x : Space d => ‖x‖ ^ (- ((d - 2 : ℕ) : ℤ)))
+      (IsDistBounded.pow _ (by grind))) =
+      (- ((d - 2 : ℕ) : ℝ) * (d : ℝ) *
+        (volume (α := Space d)).real (Metric.ball 0 1)) • diracDelta ℝ 0 := by
+  by_cases hd : d < 3
+  · have hdim : d - 2 = 0 := by omega
+    simp [hdim]
+    exact distLaplacian_const 1
+  · convert distLaplacian_fundamentalSolution_norm_zpow_of_three_le
+      (d := d) (by grind) using 4 <;>
+      rw [Nat.cast_sub (by omega : 2 ≤ d)] <;>
+      ring_nf
+
 end Space