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_inv_pow_eq_dim : The divergence of the distribution defined by the inverse power of the norm propotional to the Dirac delta distribution.

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 equal dirac delta

iv. References

A. The norm as a power series

def Space.normPowerSeries {d : ℕ} : ℕ → Space d → ℝ

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

Equations

• Space.normPowerSeries n x = √(‖x‖ ^ 2 + 1 / (↑n + 1))

theorem Space.normPowerSeries_eq {d : ℕ} (n : ℕ) : normPowerSeries n = fun (x : Space d) => √(‖x‖ ^ 2 + 1 / (↑n + 1))

theorem Space.normPowerSeries_eq_rpow {d : ℕ} (n : ℕ) : normPowerSeries n = fun (x : Space d) => (‖x‖ ^ 2 + 1 / (↑n + 1)) ^ (1 / 2)

A.1. Differentiability of the norm power series

theorem Space.normPowerSeries_differentiable {d : ℕ} (n : ℕ) : Differentiable ℝ fun (x : Space d) => normPowerSeries n x

A.2. The limit of the norm power series

theorem Space.normPowerSeries_tendsto {d : ℕ} (x : Space d) (hx : x ≠ 0) : Filter.Tendsto (fun (n : ℕ) => normPowerSeries n x) Filter.atTop (nhds ‖x‖)

theorem Space.normPowerSeries_inv_tendsto {d : ℕ} (x : Space d) (hx : x ≠ 0) : Filter.Tendsto (fun (n : ℕ) => (normPowerSeries n x)⁻¹) Filter.atTop (nhds ‖x‖⁻¹)

A.3. The derivative of the norm power series

theorem Space.deriv_normPowerSeries {d : ℕ} (n : ℕ) (x : Space d) (i : Fin d) : deriv i (normPowerSeries n) x = x.val i * (normPowerSeries n x)⁻¹

theorem Space.fderiv_normPowerSeries {d : ℕ} (n : ℕ) (x y : Space d) : (fderiv ℝ (fun (x : Space d) => normPowerSeries n x) x) y = inner ℝ y x * (normPowerSeries n x)⁻¹

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

theorem Space.deriv_normPowerSeries_tendsto {d : ℕ} (x : Space d) (hx : x ≠ 0) (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => deriv i (normPowerSeries n) x) Filter.atTop (nhds (x.val i * ‖x‖⁻¹))

theorem Space.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 (nhds (inner ℝ y x * ‖x‖⁻¹))

A.5. The power series is AEStronglyMeasurable

theorem Space.normPowerSeries_aestronglyMeasurable {d : ℕ} (n : ℕ) : MeasureTheory.AEStronglyMeasurable (normPowerSeries n) MeasureTheory.volume

A.6. Bounds on the norm power series

@[simp]

theorem Space.normPowerSeries_nonneg {d : ℕ} (n : ℕ) (x : Space d) : 0 ≤ normPowerSeries n x

@[simp]

theorem Space.normPowerSeries_pos {d : ℕ} (n : ℕ) (x : Space d) : 0 < normPowerSeries n x

@[simp]

theorem Space.normPowerSeries_ne_zero {d : ℕ} (n : ℕ) (x : Space d) : normPowerSeries n x ≠ 0

theorem Space.normPowerSeries_le_norm_sq_add_one {d : ℕ} (n : ℕ) (x : Space d) : normPowerSeries n x ≤ ‖x‖ + 1

@[simp]

theorem Space.norm_lt_normPowerSeries {d : ℕ} (n : ℕ) (x : Space d) : ‖x‖ < normPowerSeries n x

theorem Space.norm_le_normPowerSeries {d : ℕ} (n : ℕ) (x : Space d) : ‖x‖ ≤ normPowerSeries n x

theorem Space.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

theorem Space.normPowerSeries_inv_le {d : ℕ} (n : ℕ) (x : Space d) (hx : x ≠ 0) : (normPowerSeries n x)⁻¹ ≤ ‖x‖⁻¹

theorem Space.normPowerSeries_log_le_normPowerSeries {d : ℕ} (n : ℕ) (x : Space d) : |Real.log (normPowerSeries n x)| ≤ (normPowerSeries n x)⁻¹ + normPowerSeries n x

theorem Space.normPowerSeries_log_le {d : ℕ} (n : ℕ) (x : Space d) (hx : x ≠ 0) : |Real.log (normPowerSeries n x)| ≤ ‖x‖⁻¹ + (‖x‖ + 1)

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

theorem Space.IsDistBounded.normPowerSeries_zpow {d n : ℕ} (m : ℤ) : IsDistBounded fun (x : Space d) => normPowerSeries n x ^ m

theorem Space.IsDistBounded.normPowerSeries_single {d n : ℕ} : IsDistBounded fun (x : Space d) => normPowerSeries n x

theorem Space.IsDistBounded.normPowerSeries_inv {d n : ℕ} : IsDistBounded fun (x : Space d) => (normPowerSeries n x)⁻¹

theorem Space.IsDistBounded.normPowerSeries_deriv {d : ℕ} (n : ℕ) (i : Fin d) : IsDistBounded fun (x : Space d) => deriv i (normPowerSeries n) x

theorem Space.IsDistBounded.normPowerSeries_fderiv {d : ℕ} (n : ℕ) (y : Space d) : IsDistBounded fun (x : Space d) => (fderiv ℝ (fun (x : Space d) => normPowerSeries n x) x) y

theorem Space.IsDistBounded.normPowerSeries_log {d : ℕ} (n : ℕ) : IsDistBounded fun (x : Space d) => Real.log (normPowerSeries n x)

A.8. Differentiability of functions

theorem Space.differentiable_normPowerSeries_zpow {d n : ℕ} (m : ℤ) : Differentiable ℝ fun (x : Space d) => normPowerSeries n x ^ m

theorem Space.differentiable_normPowerSeries_inv {d n : ℕ} : Differentiable ℝ fun (x : Space d) => (normPowerSeries n x)⁻¹

theorem Space.differentiable_log_normPowerSeries {d n : ℕ} : Differentiable ℝ fun (x : Space d) => Real.log (normPowerSeries n x)

A.9. Derivatives of functions

theorem Space.deriv_normPowerSeries_zpow {d n : ℕ} (m : ℤ) (x : Space d) (i : Fin d) : deriv i (fun (x : Space d) => normPowerSeries n x ^ m) x = ↑m * x.val i * normPowerSeries n x ^ (m - 2)

theorem Space.fderiv_normPowerSeries_zpow {d n : ℕ} (m : ℤ) (x y : Space d) : (fderiv ℝ (fun (x : Space d) => normPowerSeries n x ^ m) x) y = ↑m * inner ℝ y x * normPowerSeries n x ^ (m - 2)

theorem Space.deriv_log_normPowerSeries {d n : ℕ} (x : Space d) (i : Fin d) : deriv i (fun (x : Space d) => Real.log (normPowerSeries n x)) x = x.val i * normPowerSeries n x ^ (-2)

theorem Space.fderiv_log_normPowerSeries {d n : ℕ} (x y : Space d) : (fderiv ℝ (fun (x : Space d) => Real.log (normPowerSeries n x)) x) y = inner ℝ y x * normPowerSeries n x ^ (-2)

A.10. Gradients of distributions based on powers

theorem Space.gradient_dist_normPowerSeries_zpow {d n : ℕ} (m : ℤ) : distGrad (distOfFunction (fun (x : Space d) => normPowerSeries n x ^ m) ⋯) = distOfFunction (fun (x : Space d) => (↑m * normPowerSeries n x ^ (m - 2)) • basis.repr x) ⋯

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

theorem Space.gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm {d : ℕ} (m : ℤ) (hm : -↑(d.succ - 1) ≤ m) (η : SchwartzMap (Space d.succ) ℝ) (y : EuclideanSpace ℝ (Fin d.succ)) : Filter.Tendsto (fun (n : ℕ) => inner ℝ ((distGrad (distOfFunction (fun (x : Space d.succ) => normPowerSeries n x ^ m) ⋯)) η) y) Filter.atTop (nhds (inner ℝ ((distGrad (distOfFunction (fun (x : Space d.succ) => ‖x‖ ^ m) ⋯)) η) y))

theorem Space.gradient_dist_normPowerSeries_zpow_tendsTo {d : ℕ} (m : ℤ) (hm : -↑(d.succ - 1) + 1 ≤ m) (η : SchwartzMap (Space d.succ) ℝ) (y : EuclideanSpace ℝ (Fin d.succ)) : Filter.Tendsto (fun (n : ℕ) => inner ℝ ((distGrad (distOfFunction (fun (x : Space d.succ) => normPowerSeries n x ^ m) ⋯)) η) y) Filter.atTop (nhds (inner ℝ ((distOfFunction (fun (x : Space d.succ) => (↑m * ‖x‖ ^ (m - 2)) • basis.repr x) ⋯) η) y))

A.11. Gradients of distributions based on logs

theorem Space.gradient_dist_normPowerSeries_log {d n : ℕ} : distGrad (distOfFunction (fun (x : Space d) => Real.log (normPowerSeries n x)) ⋯) = distOfFunction (fun (x : Space d) => normPowerSeries n x ^ (-2) • basis.repr x) ⋯

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

theorem Space.gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm {d : ℕ} (η : SchwartzMap (Space d.succ.succ) ℝ) (y : EuclideanSpace ℝ (Fin d.succ.succ)) : Filter.Tendsto (fun (n : ℕ) => inner ℝ ((distGrad (distOfFunction (fun (x : Space d.succ.succ) => Real.log (normPowerSeries n x)) ⋯)) η) y) Filter.atTop (nhds (inner ℝ ((distGrad (distOfFunction (fun (x : Space d.succ.succ) => Real.log ‖x‖) ⋯)) η) y))

theorem Space.gradient_dist_normPowerSeries_log_tendsTo {d : ℕ} (η : SchwartzMap (Space d.succ.succ) ℝ) (y : EuclideanSpace ℝ (Fin d.succ.succ)) : Filter.Tendsto (fun (n : ℕ) => inner ℝ ((distGrad (distOfFunction (fun (x : Space d.succ.succ) => Real.log (normPowerSeries n x)) ⋯)) η) y) Filter.atTop (nhds (inner ℝ ((distOfFunction (fun (x : Space d.succ.succ) => ‖x‖ ^ (-2) • basis.repr x) ⋯) η) y))

B. Distributions involving norms

B.1. The gradient of distributions based on powers

theorem Space.distGrad_distOfFunction_norm_zpow {d : ℕ} (m : ℤ) (hm : -↑(d.succ - 1) + 1 ≤ m) : distGrad (distOfFunction (fun (x : Space d.succ) => ‖x‖ ^ m) ⋯) = distOfFunction (fun (x : Space d.succ) => (↑m * ‖x‖ ^ (m - 2)) • basis.repr x) ⋯

B.2. The gradient of distributions based on logs

theorem Space.distGrad_distOfFunction_log_norm {d : ℕ} : distGrad (distOfFunction (fun (x : Space d.succ.succ) => Real.log ‖x‖) ⋯) = distOfFunction (fun (x : Space d.succ.succ) => ‖x‖ ^ (-2) • basis.repr x) ⋯

B.3. 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 proof

theorem Space.distDiv_inv_pow_eq_dim {d : ℕ} : distDiv (distOfFunction (fun (x : Space d.succ) => ‖x‖ ^ (-↑d.succ) • basis.repr x) ⋯) = (↑d.succ * MeasureTheory.volume.real (Metric.ball 0 1)) • Distribution.diracDelta ℝ 0