Physlib.SpaceAndTime.Space.Integrals.Basic
Integrals in Space
i. Overview
In this module we give general properties of integrals over `Space d`. We focus here on the volume measure, which is the usual measure on `Space d`, i.e. `dx dy dz`.
ii. Key results
- `volume_eq_addHaar` : The volume measure on `Space d` is the same as the Haar measure associated with the basis of `Space d`. - `integral_volume_eq_spherical` : The integral of a function over `Space d.succ` with respect to the volume measure can be expressed as an integral over the unit sphere and the positive reals. - `lintegral_volume_eq_spherical` : The lower Lebesgue integral of a function over `Space d.succ` with respect to the volume measure can be expressed as a lower Lebesgue integral over the unit sphere and the positive reals.
A. Properties of the volume measure
B. Integrals over one-dimensional space
C. Integrals over volume to spherical
D. Lower Lebesgue integral over volume to spherical
12 declarations
The volume measure on equals the additive Haar measure
For any dimension , the volume measure on the -dimensional space is equal to the additive Haar measure normalized with respect to the standard orthonormal basis of the space.
The volume of a closed ball with positive radius in is non-zero.
In the -dimensional Euclidean space , for any point and any strictly positive radius , the volume (Lebesgue measure) of the closed ball is non-zero.
The volume of a closed ball in is finite
For any natural number , let be a point in the -dimensional real Euclidean space and be a real number. The volume (standard Lebesgue measure) of the closed ball centered at with radius is finite, i.e., .
The volume of the unit ball in is
In the 3D Euclidean space , the volume (Lebesgue measure) of the open unit ball centered at the origin, defined as , is equal to .
The volume of the unit ball in is
In the 2-dimensional Euclidean space , the volume (Lebesgue measure) of the open unit ball centered at the origin with radius , defined as , is equal to .
The volume of the unit ball in is
In the 2-dimensional Euclidean space , the real-valued volume (Lebesgue measure) of the open unit ball centered at the origin with radius is equal to : where the unit ball is defined as the set of points such that their norm is less than , and denotes the volume expressed as a real number.
The real volume of the unit ball in is
In the 3-dimensional Euclidean space , the real-valued volume (Lebesgue measure) of the open unit ball centered at the origin with radius , defined as , is equal to .
Let be a function. The integral of over the one-dimensional space with respect to the volume measure is equal to the integral of composed with the inverse of the linear isometric equivalence over the real numbers with respect to the standard Lebesgue measure: where is the map that sends a real number to the corresponding vector in .
Integration over in Spherical Coordinates
For any natural number , let be the -dimensional real inner product space and be a normed real vector space. For a function , the integral of over with respect to the standard volume measure can be expressed in spherical coordinates as: where is the unit sphere, is the surface measure on , and is the radial measure on the interval defined by , where is the dimension of the space minus one.
The Lebesgue measure on is -finite
Let be the standard Lebesgue measure (volume) on the real numbers . The measure on the interval of positive real numbers obtained by the pullback of under the inclusion map is -finite.
Spherical Integration Formula for Lebesgue Integral in
For any natural number and any measurable function , the Lebesgue integral of with respect to the volume measure on the -dimensional Euclidean space is given by: where is the unit sphere in , is a unit vector, is the radius, is the spherical measure, and is the radial measure on defined by .
Spherical Integration Formula with Radial Weight in
For any natural number and any measurable function , the Lebesgue integral of with respect to the volume measure on the -dimensional real vector space is given by: where is the unit sphere in , is the spherical measure on , and is the standard Lebesgue measure on the positive real line . In this expression, represents the radius and is a unit vector.
