Generalized polar coordinate change #
Consider an n-dimensional normed space E and an additive Haar measure μ on E.
Then μ.toSphere is the measure on the unit sphere
such that μ.toSphere s equals n • μ (Set.Ioo 0 1 • s).
If n ≠ 0, then μ can be represented (up to homeomorphUnitSphereProd)
as the product of μ.toSphere
and the Lebesgue measure on (0, +∞) taken with density fun r ↦ r ^ n.
One can think about this fact as a version of polar coordinate change formula for a general nontrivial normed space.
In this file we provide a way to rewrite integrals and integrability
of functions that depend on the norm only in terms of integral over (0, +∞).
We also provide a positive lower estimate on the (Measure.toSphere μ)-measure
of a ball of radius ε > 0 on the unit sphere.
If μ is an additive Haar measure on a normed space E,
then μ.toSphere is the measure on the unit sphere in E
such that μ.toSphere s = Module.finrank ℝ E • μ (Set.Ioo (0 : ℝ) 1 • s).
Instances For
The measure on (0, +∞) that has density (· ^ n) with respect to the Lebesgue measure.
Instances For
The intervals (0, k + 1) have finite measure MeasureTheory.Measure.volumeIoiPow _
and cover the whole open ray (0, +∞).
Instances For
The homeomorphism homeomorphUnitSphereProd E sends an additive Haar measure μ
to the product of μ.toSphere and MeasureTheory.Measure.volumeIoiPow (dim E - 1),
where dim E = Module.finrank ℝ E is the dimension of E.
Lower estimate on the measure of the ε-cone in an n-dimensional normed space
divided by the measure of the ball.
Instances For
A ball of radius ε on the unit sphere in a real normed space
has measure at least toSphereBallBound n ε * μ (ball 0 1),
where n is the dimension of the space,
toSphereBallBound n ε is a lower estimate that depends only on the dimension and ε,
which is positive for positive n and ε.
A ball of radius ε on the unit sphere in a real normed space
has measure at least toSphereBallBound n ε * μ (ball 0 1),
where n is the dimension of the space,
toSphereBallBound n ε is a lower estimate that depends only on the dimension and ε,
which is positive for positive n and ε.
This is a version stated in terms MeasureTheory.Measure.real.