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
Regularized power of the norm
Given a dimension , a regularization parameter , and an exponent , this function maps an element of the -dimensional space to the value , where denotes the Euclidean norm on .
For any natural number and real numbers and , the function on is given by the expression , where denotes the Euclidean norm on .
Positivity of for non-zero
For any natural number , any element in the -dimensional space , and any non-zero real number , the sum of the square of the norm of and the square of is strictly positive: where denotes the Euclidean norm of .
Positivity of the Regularized Norm Power for
For any natural number , any non-zero real number , any real number , and any element in the -dimensional space , the regularized norm power is strictly positive: where denotes the Euclidean norm of .
The regularized norm power has temperate growth
For any dimension , any non-zero real number , and any real exponent , the regularized norm power function defined on the -dimensional space has temperate growth, where denotes the Euclidean norm on .
The regularized norm power is measurable
For any dimension and real numbers , the regularized power of the norm function from to is measurable, where denotes the Euclidean norm on and the space is equipped with its Borel -algebra.
