Physlib

Physlib.SpaceAndTime.Space.Norm.Regularized

Regularized powers of the norm on space

i. Overview

This file contains basic API for regularized powers of the norm on `Space d`, namely `x ↦ (‖x‖ ^ 2 + ε ^ 2) ^ (s / 2)`.

ii. Key results

  • `normRegularizedPow` : The regularized norm power `x ↦ (‖x‖ ^ 2 + ε ^ 2) ^ (s / 2)`.
  • `normRegularizedPow_pos` : Positivity for nonzero regularization parameter.
  • `normRegularizedPow_hasTemperateGrowth` : Temperate growth of regularized norm powers.
  • `normRegularizedPow_measurable` : Measurability of regularized norm powers.

iii. Table of contents

  • A. Regularized powers of the norm

iv. References

A. Regularized powers of the norm

6 declarations

definition

Regularized power of the norm (x2+ϵ2)s/2(\|x\|^2 + \epsilon^2)^{s/2}

Given a dimension dd, a regularization parameter ϵR\epsilon \in \mathbb{R}, and an exponent sRs \in \mathbb{R}, this function maps an element xx of the dd-dimensional space Space d\text{Space } d to the value (x2+ϵ2)s/2(\|x\|^2 + \epsilon^2)^{s/2}, where x\|x\| denotes the Euclidean norm on Space d\text{Space } d.

theorem

normRegularizedPow(d,ϵ,s)=(x2+ϵ2)s/2\text{normRegularizedPow}(d, \epsilon, s) = (\|x\|^2 + \epsilon^2)^{s/2}

For any natural number dd and real numbers ϵ\epsilon and ss, the function normRegularizedPow(d,ϵ,s)\text{normRegularizedPow}(d, \epsilon, s) on Space d\text{Space } d is given by the expression x(x2+ϵ2)s/2x \mapsto (\|x\|^2 + \epsilon^2)^{s/2}, where x\|x\| denotes the Euclidean norm on Space d\text{Space } d.

theorem

Positivity of x2+ϵ2\|x\|^2 + \epsilon^2 for non-zero ϵ\epsilon

For any natural number dd, any element xx in the dd-dimensional space Space d\text{Space } d, and any non-zero real number ϵ\epsilon, the sum of the square of the norm of xx and the square of ϵ\epsilon is strictly positive: x2+ϵ2>0 \|x\|^2 + \epsilon^2 > 0 where x\|x\| denotes the Euclidean norm of xx.

theorem

Positivity of the Regularized Norm Power (x2+ϵ2)s/2(\|x\|^2 + \epsilon^2)^{s/2} for ϵ0\epsilon \neq 0

For any natural number dd, any non-zero real number ϵ\epsilon, any real number ss, and any element xx in the dd-dimensional space Space d\text{Space } d, the regularized norm power (x2+ϵ2)s/2(\|x\|^2 + \epsilon^2)^{s/2} is strictly positive: (x2+ϵ2)s/2>0 (\|x\|^2 + \epsilon^2)^{s/2} > 0 where x\|x\| denotes the Euclidean norm of xx.

theorem

The regularized norm power x(x2+ϵ2)s/2x \mapsto (\|x\|^2 + \epsilon^2)^{s/2} has temperate growth

For any dimension dNd \in \mathbb{N}, any non-zero real number ϵR×\epsilon \in \mathbb{R}^\times, and any real exponent sRs \in \mathbb{R}, the regularized norm power function x(x2+ϵ2)s/2x \mapsto (\|x\|^2 + \epsilon^2)^{s/2} defined on the dd-dimensional space Space d\text{Space } d has temperate growth, where x\|x\| denotes the Euclidean norm on Space d\text{Space } d.

theorem

The regularized norm power x(x2+ϵ2)s/2x \mapsto (\|x\|^2 + \epsilon^2)^{s/2} is measurable

For any dimension dNd \in \mathbb{N} and real numbers ϵ,sR\epsilon, s \in \mathbb{R}, the regularized power of the norm function x(x2+ϵ2)s/2x \mapsto (\|x\|^2 + \epsilon^2)^{s/2} from Space d\text{Space } d to R\mathbb{R} is measurable, where x\|x\| denotes the Euclidean norm on Space d\text{Space } d and the space is equipped with its Borel σ\sigma-algebra.