The uniform law on the unit sphere #
On a finite-dimensional real inner product space E of dimension d ≥ 1, the uniform law
uniformSphereMeasure E on the unit sphere is Mathlib's polar-coordinate surface measure
volume.toSphere normalized to total mass one. The surface measure has total mass
2 π ^ (d / 2) / Γ (d / 2) (TauCeti.toSphere_volume_apply_univ). In dimension zero the sphere
is empty and there is no probability law on it.
The uniform law is invariant under linear isometries, so its embedded mean vanishes. It is also
the law of the direction of a standard Gaussian vector, and that direction is independent of the
Gaussian radius, which has the chi law with d degrees of freedom. More generally, the joint
law of direction and radius of any finite measure with a radial density against Lebesgue measure
is the product of the uniform law and the radius law; for a probability measure this says the
direction is uniform and independent of the radius. The direction is read through
TauCeti.sphereDirection e, which sends a nonzero vector x to ‖x‖⁻¹ • x and the origin to an
assigned point e of the sphere; the origin is a null set for these laws, so the results hold
for every choice of e.
The radial factorization comes from the polar-coordinate formula
TauCeti.lintegral_eq_lintegral_toSphere_lintegral_Ioi, which is Mathlib's
MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd read on integrals.
Main definitions #
TauCeti.Probability.uniformSphereMeasure: the uniform law on the unit sphere.
Main results #
TauCeti.Probability.support_uniformSphereMeasure: the uniform sphere law has full support.LinearIsometryEquiv.map_uniformSphereMeasure: invariance under linear isometric equivalences.TauCeti.Probability.integral_coe_uniformSphereMeasure: the embedded mean is zero.TauCeti.Probability.map_sphereDirection_prod_norm_withDensity: the joint law of direction and radius of a finite radial density is the product of the uniform law and the radius law.TauCeti.Probability.stdGaussian_map_sphereDirection_prod_norm: the direction and radius of a standard Gaussian vector are independent, uniform on the sphere and chi distributed.ProbabilityTheory.HasLaw.sphereDirection_stdGaussian,ProbabilityTheory.HasLaw.indepFun_sphereDirection_norm_stdGaussian: the same statements for a random vector with standard Gaussian law.
References #
- R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982, section 1.5.
The uniform law on the unit sphere of a finite-dimensional real inner product space: the
surface measure volume.toSphere divided by its total mass. It is a probability measure in every
positive dimension; in dimension zero the sphere is empty.
Instances For
The uniform law on the sphere is the normalized surface measure.
The uniform law of a set of the sphere is its surface measure divided by the surface area
2 π ^ (d / 2) / Γ (d / 2) of the sphere.
In every positive dimension the uniform law on the sphere is a probability measure.
The uniform sphere measure has full topological support. In dimension zero both the sphere and its universal set are empty.
The exponential of every real linear observable of a uniform sphere point is integrable.
The exponential moment of a linear observable is positive in positive dimension.
Isometry invariance of the uniform sphere law. A linear isometric equivalence, restricted
to the unit spheres, carries the uniform law on the sphere of E to the uniform law on the
sphere of F. With F = E this is invariance under orthogonal transformations.
The uniform law on the sphere has embedded mean zero.
Polar factorization of a radial law. If a finite measure has a density against Lebesgue
measure depending only on the norm, then the joint law of its direction and its radius is the
product of the uniform law on the sphere and the law of the radius. For a probability measure this
says that the direction is uniform on the sphere and independent of the radius; in general the
direction marginal is the uniform law scaled by the total mass. The assigned direction e of the
origin is irrelevant since the origin is a null set.
The direction of a standard Gaussian vector is uniform and independent of its radius.
The pair of the direction and the norm of a standard Gaussian vector has the product of the
uniform law on the sphere and the chi law with d degrees of freedom.
The direction of a standard Gaussian vector is uniform on the sphere.
The direction of a random vector with standard Gaussian law is uniform on the sphere.
The direction of a random vector with standard Gaussian law is independent of its norm.