Physlib

Physlib.SpaceAndTime.Space.Norm.Basic

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

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

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

B.6. The Laplacian of the fundamental solution

4 declarations

theorem

The distributional divergence (xqx)=(q+d)xq\nabla \cdot (\|x\|^q \mathbf{x}) = (q + d) \|x\|^q

Let Space d\text{Space } d be a dd-dimensional real inner product space with d>0d > 0. For any integer qq satisfying q+d>0q + d > 0, the distributional divergence of the distribution associated with the function xxqrepr(x)x \mapsto \|x\|^q \cdot \text{repr}(x) is given by: Txqrepr(x)=(q+d)Txq \nabla \cdot \mathcal{T}_{\|x\|^q \text{repr}(x)} = (q + d) \mathcal{T}_{\|x\|^q} where repr(x)Rd\text{repr}(x) \in \mathbb{R}^d denotes the coordinate representation of xx with respect to the standard orthonormal basis of Space d\text{Space } d, and Tg\mathcal{T}_g denotes the distribution associated with a distribution-bounded function gg.

theorem

Distributional Laplacian of xm\|x\|^m equals m(m2+d)xm2m(m - 2 + d) \|x\|^{m-2}

Let dd be a positive natural number and let Space d\text{Space } d be a dd-dimensional real inner product space. For any integer mm satisfying the condition m2+d>0m - 2 + d > 0, the distributional Laplacian Δ\Delta of the distribution associated with the function xxmx \mapsto \|x\|^m is equal to the scalar m(m2+d)m(m - 2 + d) multiplied by the distribution associated with the function xxm2x \mapsto \|x\|^{m-2}. That is, Δ(xm)=m(m2+d)xm2. \Delta (\|x\|^m) = m(m - 2 + d) \|x\|^{m-2}.

theorem

Δx2d=(2d)dvol(B(0,1))δ0\Delta \|x\|^{2-d} = (2-d) d \cdot \text{vol}(B(0, 1)) \cdot \delta_0

In a dd-dimensional Euclidean space VV (where dNd \in \mathbb{N}), the distributional Laplacian of the function f(x)=x2df(x) = \|x\|^{2-d} is given by: Δ(x2d)=(2d)dvol(B(0,1))δ0\Delta (\|x\|^{2-d}) = (2 - d) \cdot d \cdot \text{vol}(B(0, 1)) \cdot \delta_0 where x\|x\| denotes the Euclidean norm, vol(B(0,1))\text{vol}(B(0, 1)) is the volume of the unit ball in VV, and δ0\delta_0 is the Dirac delta distribution at the origin. For d3d \ge 3, this function x2d\|x\|^{2-d} is the singular fundamental solution of the Laplacian; for d=1d=1, it corresponds to x=x\|x\| = |x|; for d=2d=2, the identity simplifies to Δ1=0\Delta 1 = 0.

theorem

Δ(lnx)=2vol(B1)δ0\Delta (\ln \|x\|) = 2 \cdot \text{vol}(B_1) \cdot \delta_0 in 2D

In a 2-dimensional Euclidean space VV, the distributional Laplacian Δ\Delta of the distribution associated with the function f(x)=lnxf(x) = \ln \|x\| is equal to 2vol(B(0,1))δ02 \cdot \text{vol}(B(0, 1)) \cdot \delta_0, where vol(B(0,1))\text{vol}(B(0, 1)) is the volume of the unit ball in VV and δ0\delta_0 is the Dirac delta distribution at the origin.