Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian public import Physlib.SpaceAndTime.Space.Integrals.NormPow public import Physlib.Mathematics.Distribution.PowMul

The norm on space

i. Overview

The main content of this file is defining Space.normPowerSeries, a power series which is differentiable everywhere, and which tends to the norm in the limit as n → ∞.

We use properties of this power series to prove various results about distributions involving norms.

ii. Key results

    normPowerSeries : A power series which is differentiable everywhere, and in the limit as n → ∞ tends to ‖x‖.

    normPowerSeries_differentiable : The power series is differentiable everywhere.

    normPowerSeries_tendsto : The power series tends to the norm in the limit as n → ∞.

    distGrad_distOfFunction_norm_zpow : The gradient of the distribution defined by a power of the norm.

    distGrad_distOfFunction_log_norm : The gradient of the distribution defined by the logarithm of the norm.

    distDiv_norm_zpow_smul_repr_self_eq_smul : The divergence of the distribution defined by x ↦ ‖x‖ ^ q • x.

    distLaplacian_distOfFunction_norm_zpow : The Laplacian of the distribution defined by a power of the norm.

    distDiv_inv_pow_eq_dim : The divergence of x ↦ ‖x‖ ^ (-d) • x equals d * volume (ball 0 1) times the Dirac delta at the origin.

    distLaplacian_fundamentalSolution_norm_zpow : The Laplacian of the power-form fundamental solution ‖x‖ ^ (2 - d), in every dimension (trivial at d = 0, 2).

    distLaplacian_fundamentalSolution_log_norm : The Laplacian of the two-dimensional logarithmic fundamental solution Real.log ‖x‖.

iii. Table of contents

    A. The norm as a power series

      A.1. Differentiability of the norm power series

      A.2. The limit of the norm power series

      A.3. The derivative of the norm power series

      A.4. Limits of the derivative of the power series

      A.5. The power series is AEStronglyMeasurable

      A.6. Bounds on the norm power series

      A.7. The IsDistBounded property of the norm power series

      A.8. Differentiability of functions

      A.9. Derivatives of functions

      A.10. Gradients of distributions based on powers

        A.10.1. The limits of gradients of distributions based on powers

      A.11. Gradients of distributions based on logs

        A.11.1. The limits of gradients of distributions based on logs

    B. Distributions involving norms

      B.1. The gradient of distributions based on powers

      B.2. The gradient of distributions based on logs

      B.3. Divergence of radial norm-power distributions

      B.4. The Laplacian of distributions based on powers

      B.5. Divergence equal dirac delta

      B.6. The Laplacian of the fundamental solution

iv. References

@[expose] public section

A. The norm as a power series

A power series which is differentiable everywhere, and in the limit as n → ∞ tends to ‖x‖.

def normPowerSeries {d} : Space d := fun n x => (x ^ 2 + 1/(n + 1))
lemma normPowerSeries_eq (n : ) : normPowerSeries (d := d) n = fun x => (x ^ 2 + 1/(n + 1)) := rfllemma normPowerSeries_eq_rpow {d} (n : ) : normPowerSeries (d := d) n = fun x => ((x ^ 2 + 1/(n + 1))) ^ (1/2 : ) := funext fun _ => Real.sqrt_eq_rpow _

A.1. Differentiability of the norm power series

d:n:Differentiable fun x => (fun x => (x ^ 2 + 1 / (n + 1))) x d:n:x:Space dDifferentiableAt (fun x => (fun x => (x ^ 2 + 1 / (n + 1))) x) x exact ((differentiable_id.norm_sq ).add_const _).differentiableAt.sqrt (d:n:x:Space did x ^ 2 + 1 / (n + 1) 0 All goals completed! 🐙)

A.2. The limit of the norm power series

lemma normPowerSeries_tendsto {d} (x : Space d) (hx : x 0) : Filter.Tendsto (fun n => normPowerSeries n x) Filter.atTop (𝓝 (x)) := d:x:Space dhx:x 0Filter.Tendsto (fun n => normPowerSeries n x) Filter.atTop (𝓝 x) d:x:Space dhx:x 0h:Filter.Tendsto ((fun x => x) fun x_1 => x ^ 2 + 1 / (x_1 + 1)) Filter.atTop (𝓝 (x ^ 2 + 0))Filter.Tendsto (fun n => normPowerSeries n x) Filter.atTop (𝓝 x) All goals completed! 🐙lemma normPowerSeries_inv_tendsto {d} (x : Space d) (hx : x 0) : Filter.Tendsto (fun n => (normPowerSeries n x)⁻¹) Filter.atTop (𝓝 (x⁻¹)) := (normPowerSeries_tendsto x hx).inv₀ (norm_ne_zero_iff.mpr hx)

A.3. The derivative of the norm power series

d:n:x:Space di:Fin d((x ^ 2 + (n + 1)⁻¹))⁻¹ * 2⁻¹ * (2 * x.val i) = x.val i * ((x ^ 2 + (n + 1)⁻¹))⁻¹d:n:x:Space di:Fin dDifferentiableAt (fun x => x ^ 2 + 1 / (n + 1)) xd:n:x:Space di:Fin dx ^ 2 + 1 / (n + 1) 0 d:n:x:Space di:Fin dDifferentiableAt (fun x => x ^ 2 + 1 / (n + 1)) xd:n:x:Space di:Fin dx ^ 2 + 1 / (n + 1) 0 d:n:x:Space di:Fin dDifferentiableAt (fun x => x ^ 2 + 1 / (n + 1)) x All goals completed! 🐙 d:n:x:Space di:Fin dx ^ 2 + 1 / (n + 1) 0 All goals completed! 🐙d:n:x:Space dy:Space d i, y.val i deriv i (fun x => normPowerSeries n x) x = i, y.val i * x.val i * (normPowerSeries n x)⁻¹ exact Finset.sum_congr rfl fun i _ => d:n:x:Space dy:Space di:Fin dx✝:i Finset.univy.val i deriv i (fun x => normPowerSeries n x) x = y.val i * x.val i * (normPowerSeries n x)⁻¹ All goals completed! 🐙

A.4. Limits of the derivative of the power series

lemma deriv_normPowerSeries_tendsto {d} (x : Space d) (hx : x 0) (i : Fin d) : Filter.Tendsto (fun n => ∂[i] (normPowerSeries n) x) Filter.atTop (𝓝 (x i * (x)⁻¹)) := d:x:Space dhx:x 0i:Fin dFilter.Tendsto (fun n => deriv i (normPowerSeries n) x) Filter.atTop (𝓝 (x.val i * x⁻¹)) d:x:Space dhx:x 0i:Fin dFilter.Tendsto (fun n => x.val i * (normPowerSeries n x)⁻¹) Filter.atTop (𝓝 (x.val i * x⁻¹)) All goals completed! 🐙lemma fderiv_normPowerSeries_tendsto {d} (x y : Space d) (hx : x 0) : Filter.Tendsto (fun n => fderiv (fun (x : Space d) => normPowerSeries n x) x y) Filter.atTop (𝓝 (y, x⟫_ * (x)⁻¹)) := d:x:Space dy:Space dhx:x 0Filter.Tendsto (fun n => (fderiv (fun x => normPowerSeries n x) x) y) Filter.atTop (𝓝 (y, x⟫_ * x⁻¹)) d:x:Space dy:Space dhx:x 0Filter.Tendsto (fun n => y, x⟫_ * (normPowerSeries n x)⁻¹) Filter.atTop (𝓝 (y, x⟫_ * x⁻¹)) All goals completed! 🐙

A.5. The power series is AEStronglyMeasurable

@[fun_prop] lemma normPowerSeries_aestronglyMeasurable {d} (n : ) : AEStronglyMeasurable (normPowerSeries n : Space d ) volume := (normPowerSeries_differentiable n).continuous.aestronglyMeasurable

A.6. Bounds on the norm power series

@[simp] lemma normPowerSeries_nonneg {d} (n : ) (x : Space d) : 0 normPowerSeries n x := Real.sqrt_nonneg _@[simp] lemma normPowerSeries_pos {d} (n : ) (x : Space d) : 0 < normPowerSeries n x := Real.sqrt_pos_of_pos (d:n:x:Space d0 < x ^ 2 + 1 / (n + 1) All goals completed! 🐙)@[simp] lemma normPowerSeries_ne_zero {d} (n : ) (x : Space d) : normPowerSeries n x 0 := (normPowerSeries_pos n x).ne'd:n:x:Space dh:1 / (n + 1) 1x ^ 2 + 1 / (n + 1) (x + 1) ^ 2 All goals completed! 🐙@[simp] lemma norm_lt_normPowerSeries {d} (n : ) (x : Space d) : x < normPowerSeries n x := Real.lt_sqrt_of_sq_lt (lt_add_of_pos_right _ (d:n:x:Space d0 < 1 / (n + 1) All goals completed! 🐙))lemma norm_le_normPowerSeries {d} (n : ) (x : Space d) : x normPowerSeries n x := (norm_lt_normPowerSeries n x).lelemma normPowerSeries_zpow_le_norm_sq_add_one {d} (n : ) (m : ) (x : Space d) (hx : x 0) : (normPowerSeries n x) ^ m (x + 1) ^ m + x ^ m := d:n:m:x:Space dhx:x 0normPowerSeries n x ^ m (x + 1) ^ m + x ^ m match m with d:n:m✝:x:Space dhx:x 0m:normPowerSeries n x ^ Int.ofNat m (x + 1) ^ Int.ofNat m + x ^ Int.ofNat m simpa using le_add_of_le_of_nonneg (pow_le_pow_left₀ (d:n:m✝:x:Space dhx:x 0m:0 normPowerSeries n x All goals completed! 🐙) (normPowerSeries_le_norm_sq_add_one n x) m) (d:n:m✝:x:Space dhx:x 0m:0 x ^ m All goals completed! 🐙) d:n:m✝:x:Space dhx:x 0m:normPowerSeries n x ^ Int.negSucc m (x + 1) ^ Int.negSucc m + x ^ Int.negSucc m d:n:m✝:x:Space dhx:x 0m:(normPowerSeries n x ^ (m + 1))⁻¹ ((x + 1) ^ (m + 1))⁻¹ + (x ^ (m + 1))⁻¹ exact le_add_of_nonneg_of_le (d:n:m✝:x:Space dhx:x 0m:0 ((x + 1) ^ (m + 1))⁻¹ All goals completed! 🐙) (inv_anti₀ (d:n:m✝:x:Space dhx:x 0m:0 < x ^ (m + 1) All goals completed! 🐙) (pow_le_pow_left₀ (d:n:m✝:x:Space dhx:x 0m:0 x All goals completed! 🐙) (norm_le_normPowerSeries n x) (m + 1)))lemma normPowerSeries_inv_le {d} (n : ) (x : Space d) (hx : x 0) : (normPowerSeries n x)⁻¹ x⁻¹ := inv_anti₀ (norm_pos_iff.mpr hx) (norm_le_normPowerSeries n x)d:n:x:Space dReal.log (normPowerSeries n x) (normPowerSeries n x)⁻¹ + normPowerSeries n x -Real.log (normPowerSeries n x) (normPowerSeries n x)⁻¹ + normPowerSeries n x exact (Real.log_le_rpow_div (x := normPowerSeries n x) (d:n:x:Space d0 normPowerSeries n x All goals completed! 🐙) one_pos).trans (d:n:x:Space dnormPowerSeries n x ^ 1 / 1 (normPowerSeries n x)⁻¹ + normPowerSeries n x All goals completed! 🐙), (neg_le.mp (Real.neg_inv_le_log (normPowerSeries_nonneg n x))).trans (le_add_of_nonneg_right (normPowerSeries_nonneg n x))lemma normPowerSeries_log_le {d} (n : ) (x : Space d) (hx : x 0) : |Real.log (normPowerSeries n x)| x⁻¹ + (x + 1) := (normPowerSeries_log_le_normPowerSeries n x).trans (add_le_add (normPowerSeries_inv_le n x hx) (normPowerSeries_le_norm_sq_add_one n x))

A.7. The IsDistBounded property of the norm power series

d:n:m✝:m:x:Space d(n + 1)⁻¹ (fun x => (x ^ 2 + 1 / (n + 1))) x exact Real.sqrt_le_sqrt (d:n:m✝:m:x:Space d(n + 1)⁻¹ x ^ 2 + 1 / (n + 1) All goals completed! 🐙)@[fun_prop] lemma IsDistBounded.normPowerSeries_single {d : } {n : } : IsDistBounded (d := d) (fun x => (normPowerSeries n x)) := d:n:IsDistBounded fun x => normPowerSeries n x All goals completed! 🐙@[fun_prop] lemma IsDistBounded.normPowerSeries_inv {d : } {n : } : IsDistBounded (d := d) (fun x => (normPowerSeries n x)⁻¹) := d:n:IsDistBounded fun x => (normPowerSeries n x)⁻¹ All goals completed! 🐙@[fun_prop] lemma IsDistBounded.normPowerSeries_deriv {d : } (n : ) (i : Fin d) : IsDistBounded (d := d) (fun x => ∂[i] (normPowerSeries n) x) := d:n:i:Fin dIsDistBounded fun x => deriv i (normPowerSeries n) x d:n:i:Fin dIsDistBounded fun x => x.val i * (normPowerSeries n x)⁻¹ All goals completed! 🐙@[fun_prop] lemma IsDistBounded.normPowerSeries_fderiv {d : } (n : ) (y : Space d) : IsDistBounded (d := d) (fun x => fderiv (fun (x : Space d) => normPowerSeries n x) x y) := d:n:y:Space dIsDistBounded fun x => (fderiv (fun x => normPowerSeries n x) x) y d:n:y:Space dIsDistBounded fun x => i, y.val i deriv i (fun x => normPowerSeries n x) x exact IsDistBounded.sum_fun (d:n:y:Space d i Finset.univ, IsDistBounded fun x => y.val i deriv i (fun x => normPowerSeries n x) x All goals completed! 🐙)@[fun_prop] lemma IsDistBounded.normPowerSeries_log {d : } (n : ) : IsDistBounded (d := d) (fun x => Real.log (normPowerSeries n x)) := d:n:IsDistBounded fun x => Real.log (normPowerSeries n x) d:n:IsDistBounded fun x => (normPowerSeries n x)⁻¹ + normPowerSeries n xd:n:AEStronglyMeasurable (fun x => Real.log (normPowerSeries n x)) volumed:n: (x : Space d), Real.log (normPowerSeries n x) (normPowerSeries n x)⁻¹ + normPowerSeries n x d:n:IsDistBounded fun x => (normPowerSeries n x)⁻¹ + normPowerSeries n x All goals completed! 🐙 d:n:AEStronglyMeasurable (fun x => Real.log (normPowerSeries n x)) volume All goals completed! 🐙 d:n: (x : Space d), Real.log (normPowerSeries n x) (normPowerSeries n x)⁻¹ + normPowerSeries n x All goals completed! 🐙

A.8. Differentiability of functions

@[fun_prop] lemma differentiable_normPowerSeries_zpow {d : } {n : } (m : ) : Differentiable (fun x : Space d => (normPowerSeries n x) ^ m) := Differentiable.zpow (d:n:m:Differentiable (normPowerSeries n) All goals completed! 🐙) (.inl (normPowerSeries_ne_zero n))@[fun_prop] lemma differentiable_normPowerSeries_inv {d : } {n : } : Differentiable (fun x : Space d => (normPowerSeries n x)⁻¹) := Differentiable.inv (d:n:Differentiable (normPowerSeries n) All goals completed! 🐙) (normPowerSeries_ne_zero n)@[fun_prop] lemma differentiable_log_normPowerSeries {d : } {n : } : Differentiable (fun x : Space d => Real.log (normPowerSeries n x)) := Differentiable.log (d:n:Differentiable (normPowerSeries n) All goals completed! 🐙) (normPowerSeries_ne_zero n)

A.9. Derivatives of functions

d:n:m:x:Space di:Fin dx.val i * (normPowerSeries n x)⁻¹ * (m * normPowerSeries n x ^ (m - 1)) = m * x.val i * (normPowerSeries n x ^ (m - 1) * (normPowerSeries n x)⁻¹)d:n:m:x:Space di:Fin dDifferentiableAt (fun x => x ^ m) (normPowerSeries n x)d:n:m:x:Space di:Fin dDifferentiableAt (normPowerSeries n) x d:n:m:x:Space di:Fin dDifferentiableAt (fun x => x ^ m) (normPowerSeries n x)d:n:m:x:Space di:Fin dDifferentiableAt (normPowerSeries n) x d:n:m:x:Space di:Fin dDifferentiableAt (fun x => x ^ m) (normPowerSeries n x) All goals completed! 🐙 d:n:m:x:Space di:Fin dDifferentiableAt (normPowerSeries n) x All goals completed! 🐙d:n:m:x:Space dy:Space d i, y.val i deriv i (fun x => normPowerSeries n x ^ m) x = i, m * (y.val i * x.val i) * normPowerSeries n x ^ (m - 2) exact Finset.sum_congr rfl fun i _ => d:n:m:x:Space dy:Space di:Fin dx✝:i Finset.univy.val i deriv i (fun x => normPowerSeries n x ^ m) x = m * (y.val i * x.val i) * normPowerSeries n x ^ (m - 2) All goals completed! 🐙d:n:x:Space di:Fin d(fderiv Real.log (normPowerSeries n x) ∘SL fderiv (normPowerSeries n) x) (basis i) = x.val i * normPowerSeries n x ^ (-2)d:n:x:Space di:Fin dDifferentiableAt Real.log (normPowerSeries n x)d:n:x:Space di:Fin dDifferentiableAt (normPowerSeries n) x d:n:x:Space di:Fin d(fderiv (normPowerSeries n) x) (basis i) * (normPowerSeries n x)⁻¹ = x.val i * (normPowerSeries n x ^ 2)⁻¹d:n:x:Space di:Fin dDifferentiableAt Real.log (normPowerSeries n x)d:n:x:Space di:Fin dDifferentiableAt (normPowerSeries n) x d:n:x:Space di:Fin dx.val i * (normPowerSeries n x)⁻¹ * (normPowerSeries n x)⁻¹ = x.val i * ((normPowerSeries n x)⁻¹ * (normPowerSeries n x)⁻¹)d:n:x:Space di:Fin dDifferentiableAt Real.log (normPowerSeries n x)d:n:x:Space di:Fin dDifferentiableAt (normPowerSeries n) x d:n:x:Space di:Fin dDifferentiableAt Real.log (normPowerSeries n x)d:n:x:Space di:Fin dDifferentiableAt (normPowerSeries n) x d:n:x:Space di:Fin dDifferentiableAt Real.log (normPowerSeries n x) All goals completed! 🐙 d:n:x:Space di:Fin dDifferentiableAt (normPowerSeries n) x All goals completed! 🐙d:n:x:Space dy:Space d i, y.val i deriv i (fun x => Real.log (normPowerSeries n x)) x = i, y.val i * x.val i * normPowerSeries n x ^ (-2) exact Finset.sum_congr rfl fun i _ => d:n:x:Space dy:Space di:Fin dx✝:i Finset.univy.val i deriv i (fun x => Real.log (normPowerSeries n x)) x = y.val i * x.val i * normPowerSeries n x ^ (-2) All goals completed! 🐙

A.10. Gradients of distributions based on powers

d:n:m:η:𝓢(Space d, )y:EuclideanSpace (Fin d)x:Space dm * x, basis.repr.symm y⟫_ * normPowerSeries n x ^ (m - 2) = m * normPowerSeries n x ^ (m - 2) * x, basis.repr.symm y⟫_ All goals completed! 🐙
A.10.1. The limits of gradients of distributions based on powers
d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d)h1:Integrable (fun x => (fderiv (⇑η) x) (basis.repr.symm y) * ((x + 1) ^ m + x ^ m)) volumeIntegrable (fun x => |(fderiv (⇑η) x) (basis.repr.symm y)| * ((x + 1) ^ m + x ^ m)) volume d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d)h1:Integrable (fun x => (fderiv (⇑η) x) (basis.repr.symm y) * ((x + 1) ^ m + x ^ m)) volumex:Space d(fun a => |(fderiv (⇑η) a) (basis.repr.symm y) * ((a + 1) ^ m + a ^ m)|) x = (fun x => |(fderiv (⇑η) x) (basis.repr.symm y)| * ((x + 1) ^ m + x ^ m)) x d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d)h1:Integrable (fun x => (fderiv (⇑η) x) (basis.repr.symm y) * ((x + 1) ^ m + x ^ m)) volumex:Space d|(fderiv (⇑η) x) (basis.repr.symm y)| * |(x + 1) ^ m + x ^ m| = |(fderiv (⇑η) x) (basis.repr.symm y)| * ((x + 1) ^ m + x ^ m) d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d)h1:Integrable (fun x => (fderiv (⇑η) x) (basis.repr.symm y) * ((x + 1) ^ m + x ^ m)) volumex:Space d|(x + 1) ^ m + x ^ m| = (x + 1) ^ m + x ^ m exact abs_of_nonneg (d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d)h1:Integrable (fun x => (fderiv (⇑η) x) (basis.repr.symm y) * ((x + 1) ^ m + x ^ m)) volumex:Space d0 (x + 1) ^ m + x ^ m All goals completed! 🐙) d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d) (n : ), ∀ᵐ (a : Space d), (fderiv (⇑η) a) (basis.repr.symm y) * normPowerSeries n a ^ m |(fderiv (⇑η) a) (basis.repr.symm y)| * ((a + 1) ^ m + a ^ m) d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d)n:∀ᵐ (a : Space d), (fderiv (⇑η) a) (basis.repr.symm y) * normPowerSeries n a ^ m |(fderiv (⇑η) a) (basis.repr.symm y)| * ((a + 1) ^ m + a ^ m) filter_upwards [Measure.ae_ne volume 0] with x d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d)n:x:Space dhx:x 0(fderiv (⇑η) x) (basis.repr.symm y) * normPowerSeries n x ^ m |(fderiv (⇑η) x) (basis.repr.symm y)| * ((x + 1) ^ m + x ^ m) d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d)n:x:Space dhx:x 0|(fderiv (⇑η) x) (basis.repr.symm y)| * normPowerSeries n x ^ m |(fderiv (⇑η) x) (basis.repr.symm y)| * ((x + 1) ^ m + x ^ m) All goals completed! 🐙 d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d)∀ᵐ (a : Space d), Filter.Tendsto (fun n => (fderiv (⇑η) a) (basis.repr.symm y) * normPowerSeries n a ^ m) Filter.atTop (𝓝 ((fderiv (⇑η) a) (basis.repr.symm y) * a ^ m)) filter_upwards [Measure.ae_ne volume 0] with x d:inst✝:NeZero dm:hm:-(d - 1) mη:𝓢(Space d, )y:EuclideanSpace (Fin d)x:Space dhx:x 0Filter.Tendsto (fun n => (fderiv (⇑η) x) (basis.repr.symm y) * normPowerSeries n x ^ m) Filter.atTop (𝓝 ((fderiv (⇑η) x) (basis.repr.symm y) * x ^ m)) All goals completed! 🐙d:inst✝:NeZero dm:hm:-(d - 1) + 1 mη:𝓢(Space d, )y:EuclideanSpace (Fin d)h1: (n : ) (x : Space d), η x * (m * normPowerSeries n x ^ (m - 2)) basis.repr x, y⟫_ = η x * (m * (basis.repr x, y⟫_ * normPowerSeries n x ^ (m - 2)))x:Space dhx:x 0h2:(m * x ^ (m - 2)) basis.repr x, y⟫_ = m * (basis.repr x, y⟫_ * x ^ (m - 2))Filter.Tendsto (fun n => η x * (m * (basis.repr x, y⟫_ * normPowerSeries n x ^ (m - 2)))) Filter.atTop (𝓝 (η x * (m * (basis.repr x, y⟫_ * x ^ (m - 2))))) All goals completed! 🐙

A.11. Gradients of distributions based on logs

d:n:η:𝓢(Space d, )y:EuclideanSpace (Fin d)x:Space dx, basis.repr.symm y⟫_ * (normPowerSeries n x ^ 2)⁻¹ = (normPowerSeries n x ^ 2)⁻¹ * x, basis.repr.symm y⟫_ All goals completed! 🐙
A.11.1. The limits of gradients of distributions based on logs
d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero dh1:Integrable (fun x => (fderiv (⇑η) x) (basis.repr.symm y) * (x⁻¹ + (x + 1))) volumeIntegrable (fun x => |(fderiv (⇑η) x) (basis.repr.symm y)| * (x⁻¹ + (x + 1))) volume d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero dh1:Integrable (fun x => (fderiv (⇑η) x) (basis.repr.symm y) * (x⁻¹ + (x + 1))) volumex:Space d(fun a => |(fderiv (⇑η) a) (basis.repr.symm y) * (a⁻¹ + (a + 1))|) x = (fun x => |(fderiv (⇑η) x) (basis.repr.symm y)| * (x⁻¹ + (x + 1))) x d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero dh1:Integrable (fun x => (fderiv (⇑η) x) (basis.repr.symm y) * (x⁻¹ + (x + 1))) volumex:Space d|(fderiv (⇑η) x) (basis.repr.symm y)| * |x⁻¹ + (x + 1)| = |(fderiv (⇑η) x) (basis.repr.symm y)| * (x⁻¹ + (x + 1)) d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero dh1:Integrable (fun x => (fderiv (⇑η) x) (basis.repr.symm y) * (x⁻¹ + (x + 1))) volumex:Space d|x⁻¹ + (x + 1)| = x⁻¹ + (x + 1) exact abs_of_nonneg (d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero dh1:Integrable (fun x => (fderiv (⇑η) x) (basis.repr.symm y) * (x⁻¹ + (x + 1))) volumex:Space d0 x⁻¹ + (x + 1) All goals completed! 🐙) d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero d (n : ), ∀ᵐ (a : Space d), (fderiv (⇑η) a) (basis.repr.symm y) * Real.log (normPowerSeries n a) |(fderiv (⇑η) a) (basis.repr.symm y)| * (a⁻¹ + (a + 1)) d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero dn:∀ᵐ (a : Space d), (fderiv (⇑η) a) (basis.repr.symm y) * Real.log (normPowerSeries n a) |(fderiv (⇑η) a) (basis.repr.symm y)| * (a⁻¹ + (a + 1)) filter_upwards [Measure.ae_ne volume 0] with x d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero dn:x:Space dhx:x 0(fderiv (⇑η) x) (basis.repr.symm y) * Real.log (normPowerSeries n x) |(fderiv (⇑η) x) (basis.repr.symm y)| * (x⁻¹ + (x + 1)) d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero dn:x:Space dhx:x 0|(fderiv (⇑η) x) (basis.repr.symm y)| * |Real.log (normPowerSeries n x)| |(fderiv (⇑η) x) (basis.repr.symm y)| * (x⁻¹ + (x + 1)) All goals completed! 🐙 d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero d∀ᵐ (a : Space d), Filter.Tendsto (fun n => (fderiv (⇑η) a) (basis.repr.symm y) * Real.log (normPowerSeries n a)) Filter.atTop (𝓝 ((fderiv (⇑η) a) (basis.repr.symm y) * Real.log a)) filter_upwards [Measure.ae_ne volume 0] with x d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero dx:Space dhx:x 0Filter.Tendsto (fun n => (fderiv (⇑η) x) (basis.repr.symm y) * Real.log (normPowerSeries n x)) Filter.atTop (𝓝 ((fderiv (⇑η) x) (basis.repr.symm y) * Real.log x)) All goals completed! 🐙d:hd:2 dη:𝓢(Space d, )y:EuclideanSpace (Fin d)this:NeZero dh1: (n : ) (x : Space d), η x * normPowerSeries n x ^ (-2) basis.repr x, y⟫_ = η x * (basis.repr x, y⟫_ * normPowerSeries n x ^ (-2))x:Space dhx:x 0h2:x ^ (-2) basis.repr x, y⟫_ = basis.repr x, y⟫_ * x ^ (-2)Filter.Tendsto (fun n => η x * (basis.repr x, y⟫_ * normPowerSeries n x ^ (-2))) Filter.atTop (𝓝 (η x * (basis.repr x, y⟫_ * x ^ (-2)))) All goals completed! 🐙

B. Distributions involving norms

B.1. The gradient of distributions based on powers

lemma distGrad_distOfFunction_norm_zpow {d : } [NeZero d] (m : ) (hm : - (d - 1 : ) + 1 m) : ∇ᵈ (distOfFunction (fun x : Space d => x ^ m) (IsDistBounded.pow m (𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace Einst✝¹:NormedSpace Fd:inst✝:NeZero dm:hm:-(d - 1) + 1 m-(d - 1) m All goals completed! 🐙))) = distOfFunction (fun x : Space d => (m * x ^ (m - 2)) basis.repr x) (𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace Einst✝¹:NormedSpace Fd:inst✝:NeZero dm:hm:-(d - 1) + 1 mIsDistBounded fun x => (m * x ^ (m - 2)) basis.repr x 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace Einst✝¹:NormedSpace Fd:inst✝:NeZero dm:hm:-(d - 1) + 1 mIsDistBounded fun x => m x ^ (m - 2) basis.repr x 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace Einst✝¹:NormedSpace Fd:inst✝:NeZero dm:hm:-(d - 1) + 1 mIsDistBounded fun x => x ^ (m - 2) basis.repr x 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace Einst✝¹:NormedSpace Fd:inst✝:NeZero dm:hm:-(d - 1) + 1 m-(d - 1) - 1 m - 2 All goals completed! 🐙) := d:inst✝:NeZero dm:hm:-(d - 1) + 1 m∇ᵈ (distOfFunction (fun x => x ^ m) ) = distOfFunction (fun x => (m * x ^ (m - 2)) basis.repr x) d:inst✝:NeZero dm:hm:-(d - 1) + 1 mη:𝓢(Space d, )(∇ᵈ (distOfFunction (fun x => x ^ m) )) η = (distOfFunction (fun x => (m * x ^ (m - 2)) basis.repr x) ) η exact ext_inner_right fun y => tendsto_nhds_unique (gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm m (d:inst✝:NeZero dm:hm:-(d - 1) + 1 mη:𝓢(Space d, )y:EuclideanSpace (Fin d)-(d - 1) m All goals completed! 🐙) η y) (gradient_dist_normPowerSeries_zpow_tendsTo m hm η y)

B.2. The gradient of distributions based on logs

lemma distGrad_distOfFunction_log_norm {d : } (hd : 2 d := by omega) : ∇ᵈ (distOfFunction (fun x : Space d => Real.log x) (IsDistBounded.log_norm)) = distOfFunction (fun x : Space d => (x ^ (- 2 : )) basis.repr x) (𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace Einst✝:NormedSpace Fd:hd:autoParam (2 d) distGrad_distOfFunction_log_norm._auto_1IsDistBounded fun x => x ^ (-2) basis.repr x 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace Einst✝:NormedSpace Fd:hd:autoParam (2 d) distGrad_distOfFunction_log_norm._auto_1-(d - 1) - 1 -2 All goals completed! 🐙) := d:hd:2 d∇ᵈ (distOfFunction (fun x => Real.log x) ) = distOfFunction (fun x => x ^ (-2) basis.repr x) d:hd:2 dη:𝓢(Space d, )(∇ᵈ (distOfFunction (fun x => Real.log x) )) η = (distOfFunction (fun x => x ^ (-2) basis.repr x) ) η All goals completed! 🐙

B.3. Divergence of radial norm-power distributions

private lemma integrable_real_pow_mul_schwartz (ψ : 𝓢(, )) (k : ) : Integrable (fun x : => x ^ k * ψ x) volume := ψ:𝓢(, )k:Integrable (fun x => x ^ k * ψ x) volume refine (ψ.integrable_pow_mul volume k).mono' (ψ:𝓢(, )k:AEStronglyMeasurable (fun x => x ^ k * ψ x) volume All goals completed! 🐙) (ae_of_all _ fun x => ψ:𝓢(, )k:x:x ^ k * ψ x x ^ k * ψ x All goals completed! 🐙)d:η:𝓢(Space d, )n:(Metric.sphere 0 1)p:hp:0 < pη':𝓢(, ) := (compCLM ) ηhη'_apply: (x : ), η' x = η (x n)hmul_iter_apply: (k : ) (x : ), ((⇑(powOneMul ))^[k] η') x = x ^ k * η' xhleft_subtype: (r : (Set.Ioi 0)), r ^ p * _root_.deriv (fun a => η (a n)) r Measure.comap Subtype.val volume = (x : ) in Set.Ioi 0, x ^ p * _root_.deriv (fun a => η (a n)) xhright_subtype: (r : (Set.Ioi 0)), r ^ (p - 1) * η (r n) Measure.comap Subtype.val volume = (x : ) in Set.Ioi 0, x ^ (p - 1) * η (x n)hIBP: (x : ) in Set.Ioi 0, x ^ p * _root_.deriv (fun a => η (a n)) x = 0 - 0 - (x : ) in Set.Ioi 0, p * x ^ (p - 1) * η (x n)-(0 - 0 - (x : ) in Set.Ioi 0, p * x ^ (p - 1) * η (x n)) = (x : ) in Set.Ioi 0, p * x ^ (p - 1) * η (x n) All goals completed! 🐙 _ = (p : ) * (x : ) in Set.Ioi (0 : ), x ^ (p - 1) * η (x n.1) := d:η:𝓢(Space d, )n:(Metric.sphere 0 1)p:hp:0 < pη':𝓢(, ) := (compCLM ) ηhη'_apply: (x : ), η' x = η (x n)hmul_iter_apply: (k : ) (x : ), ((⇑(powOneMul ))^[k] η') x = x ^ k * η' xhleft_subtype: (r : (Set.Ioi 0)), r ^ p * _root_.deriv (fun a => η (a n)) r Measure.comap Subtype.val volume = (x : ) in Set.Ioi 0, x ^ p * _root_.deriv (fun a => η (a n)) xhright_subtype: (r : (Set.Ioi 0)), r ^ (p - 1) * η (r n) Measure.comap Subtype.val volume = (x : ) in Set.Ioi 0, x ^ (p - 1) * η (x n)hIBP: (x : ) in Set.Ioi 0, x ^ p * _root_.deriv (fun a => η (a n)) x = 0 - 0 - (x : ) in Set.Ioi 0, p * x ^ (p - 1) * η (x n) (x : ) in Set.Ioi 0, p * x ^ (p - 1) * η (x n) = p * (x : ) in Set.Ioi 0, x ^ (p - 1) * η (x n) All goals completed! 🐙d:p:inst✝:NeZero dq:hq:0 < q + dhp_int:p = q + dη:𝓢(Space d, )F:Space d := fun x => x ^ q basis.repr x, (⇑η) x⟫_n:(Metric.sphere 0 1)r:(Set.Ioi 0)hr:0 < rhnorm:r n = rr ^ (d - 1) * (r ^ q * (r * (⇑η) (r n), basis.repr n⟫_)) = r ^ (d - 1) * (r ^ q * r) * (⇑η) (r n), basis.repr n⟫_ All goals completed! 🐙All goals completed! 🐙 _ = (((q + (d : ) : ) : ) distOfFunction (fun x : Space d => x ^ q) (IsDistBounded.pow q (d:inst✝:NeZero dq:hq:0 < q + dη:𝓢(Space d, )p: := (q + d).toNathp_int:p = q + dhp_pos:0 < phcoef:(q + d) = p-(d - 1) q All goals completed! 🐙))) η := d:inst✝:NeZero dq:hq:0 < q + dη:𝓢(Space d, )p: := (q + d).toNathp_int:p = q + dhp_pos:0 < phcoef:(q + d) = pp * (x : Space d), η x * x ^ q = ((q + d) distOfFunction (fun x => x ^ q) ) η All goals completed! 🐙

B.4. The Laplacian of distributions based on powers

All goals completed! 🐙

B.5. Divergence equal dirac delta

We show that the divergence of x ↦ ‖x‖ ^ (- d) • x is equal to a multiple of the Dirac delta at 0.

The distributional divergence of the radial field x ↦ ‖x‖ ^ (-d) • x (i.e. x / ‖x‖ ^ d) equals d * volume (Metric.ball 0 1) — the surface area of the unit sphere S^{d-1} — times the Dirac delta at the origin. This is the Gauss-law identity underlying the fundamental solution of the Laplacian: away from 0 the field is divergence-free, and all of its flux concentrates at the origin.

d:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) η0 - η (0 n) = -η 0d:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) ηContinuousWithinAt (fun a => η (a n)) (Set.Ici 0) 0d:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) η x Set.Ioi 0, HasDerivAt (fun a => η (a n)) (_root_.deriv (fun a => η (a n)) x) xd:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) ηIntegrableOn (_root_.deriv fun a => η (a n)) (Set.Ioi 0) volumed:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) ηFilter.Tendsto (fun a => η (a n)) Filter.atTop (𝓝 0) d:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) η0 - η (0 n) = -η 0 All goals completed! 🐙 d:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) ηContinuousWithinAt (fun a => η (a n)) (Set.Ici 0) 0 exact ContinuousAt.continuousWithinAt (d:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) ηContinuousAt (fun a => η (a n)) 0 All goals completed! 🐙) d:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) η x Set.Ioi 0, HasDerivAt (fun a => η (a n)) (_root_.deriv (fun a => η (a n)) x) x exact fun x _ => DifferentiableAt.hasDerivAt (d:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) ηx:x✝:x Set.Ioi 0DifferentiableAt (fun a => η (a n)) x All goals completed! 🐙) d:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) ηIntegrableOn (_root_.deriv fun a => η (a n)) (Set.Ioi 0) volume All goals completed! 🐙 d:inst✝:NeZero dη:𝓢(Space d, )n:(Metric.sphere 0 1)η':(Metric.sphere 0 1) 𝓢(, ) := fun n => (compCLM ) ηFilter.Tendsto (fun a => η (a n)) Filter.atTop (𝓝 0) All goals completed! 🐙 _ = η 0 * (d * (volume (α := Space d)).real (Metric.ball 0 1)) := d:inst✝:NeZero dη:𝓢(Space d, )- (n : (Metric.sphere 0 1)), -η 0 volume.toSphere = η 0 * (d * volume.real (Metric.ball 0 1)) d:inst✝:NeZero dη:𝓢(Space d, )d * volume.real (Metric.ball 0 1) * η 0 = η 0 * (d * volume.real (Metric.ball 0 1)) All goals completed! 🐙 d:inst✝:NeZero dη:𝓢(Space d, )η 0 * (d * volume.real (Metric.ball 0 1)) = d * volume.real (Metric.ball 0 1) * η 0 All goals completed! 🐙

B.6. The Laplacian of the fundamental solution

The distributional Laplacian of ‖x‖ ^ (2 - d) is (2 - d) * d * volume (Metric.ball 0 1) times the Dirac delta at the origin. For d ≥ 3 this ‖x‖ ^ (2 - d) is the (singular) fundamental solution of the Laplacian, and for d = 1 it is ‖x‖. When d = 2 the exponent vanishes, so the identity collapses to the trivial Δᵈ 1 = 0; the genuine two-dimensional fundamental solution is the logarithm, proved in distLaplacian_fundamentalSolution_log_norm. The statement also holds vacuously for d = 0, where the space is trivial.

d:h:¬d = 0this:NeZero dhdist:distOfFunction (fun x => ((2 - d) * x ^ (-d)) basis.repr x) = (2 - d) distOfFunction (fun x => x ^ (-d) basis.repr x) ((2 - d) * (d * volume.real (Metric.ball 0 1))) diracDelta 0 = ((2 - d) * d * volume.real (Metric.ball 0 1)) diracDelta 0 All goals completed! 🐙

In dimension two the fundamental solution of the Laplacian is the logarithm: the distributional Laplacian of Real.log ‖x‖ is 2 * volume (Metric.ball 0 1) times the Dirac delta at the origin.

distDiv (distOfFunction (fun x => x ^ (-2) basis.repr x) ) = (2 * volume.real (Metric.ball 0 1)) diracDelta 0 All goals completed! 🐙