Physlib

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

theorem

The volume measure on Space d\text{Space } d equals the additive Haar measure

For any dimension dd, the volume measure on the dd-dimensional space Space d\text{Space } d is equal to the additive Haar measure normalized with respect to the standard orthonormal basis of the space.

theorem

The volume of a closed ball with positive radius in Space(d+1)\text{Space}(d+1) is non-zero.

In the (d+1)(d+1)-dimensional Euclidean space Space(d+1)\text{Space}(d+1), for any point xx and any strictly positive radius r>0r > 0, the volume (Lebesgue measure) of the closed ball Bˉ(x,r)={ySpace(d+1)dist(x,y)r}\bar{B}(x, r) = \{y \in \text{Space}(d+1) \mid \text{dist}(x, y) \leq r\} is non-zero.

theorem

The volume of a closed ball in Space(d+1)\text{Space}(d+1) is finite

For any natural number dd, let xx be a point in the (d+1)(d+1)-dimensional real Euclidean space Space(d+1)\text{Space}(d+1) and rr be a real number. The volume (standard Lebesgue measure) of the closed ball centered at xx with radius rr is finite, i.e., volume({ySpace(d+1)dist(x,y)r})\text{volume}(\{y \in \text{Space}(d+1) \mid \text{dist}(x, y) \leq r\}) \neq \infty.

theorem

The volume of the unit ball in Space 3\text{Space } 3 is 43π\frac{4}{3}\pi

In the 3D Euclidean space Space 3\text{Space } 3, the volume (Lebesgue measure) of the open unit ball centered at the origin, defined as {xSpace 3x<1}\{x \in \text{Space } 3 \mid \|x\| < 1\}, is equal to 43π\frac{4}{3}\pi.

theorem

The volume of the unit ball in Space 2\text{Space } 2 is π\pi

In the 2-dimensional Euclidean space Space 2\text{Space } 2, the volume (Lebesgue measure) of the open unit ball centered at the origin with radius 11, defined as {xSpace 2x<1}\{x \in \text{Space } 2 \mid \|x\| < 1\}, is equal to π\pi.

theorem

The volume of the unit ball in Space 2\text{Space } 2 is π\pi

In the 2-dimensional Euclidean space Space 2\text{Space } 2, the real-valued volume (Lebesgue measure) of the open unit ball centered at the origin with radius 11 is equal to π\pi: volumeR({xSpace 2x<1})=π \text{volume}_{\mathbb{R}}(\{x \in \text{Space } 2 \mid \|x\| < 1\}) = \pi where the unit ball is defined as the set of points xx such that their norm x\|x\| is less than 11, and volumeR\text{volume}_{\mathbb{R}} denotes the volume expressed as a real number.

theorem

The real volume of the unit ball in Space 3\text{Space } 3 is 43π\frac{4}{3}\pi

In the 3-dimensional Euclidean space Space 3\text{Space } 3, the real-valued volume (Lebesgue measure) of the open unit ball centered at the origin with radius 11, defined as {xSpace 3x<1}\{x \in \text{Space } 3 \mid \|x\| < 1\}, is equal to 43π\frac{4}{3}\pi.

theorem

Space(1)f=RfoneEquiv1\int_{\text{Space}(1)} f = \int_{\mathbb{R}} f \circ \text{oneEquiv}^{-1}

Let f:Space(1)Rf: \text{Space}(1) \to \mathbb{R} be a function. The integral of ff over the one-dimensional space Space(1)\text{Space}(1) with respect to the volume measure is equal to the integral of ff composed with the inverse of the linear isometric equivalence oneEquiv:Space(1)R\text{oneEquiv} : \text{Space}(1) \cong \mathbb{R} over the real numbers R\mathbb{R} with respect to the standard Lebesgue measure: Space(1)f(x)dV=Rf(oneEquiv1(x))dx \int_{\text{Space}(1)} f(x) \, dV = \int_{\mathbb{R}} f(\text{oneEquiv}^{-1}(x)) \, dx where oneEquiv1\text{oneEquiv}^{-1} is the map that sends a real number xx to the corresponding vector in Space(1)\text{Space}(1).

theorem

Integration over Space(d+1)\text{Space}(d+1) in Spherical Coordinates

For any natural number dd, let V=Space(d+1)V = \text{Space}(d+1) be the (d+1)(d+1)-dimensional real inner product space and FF be a normed real vector space. For a function f:VFf: V \to F, the integral of ff over VV with respect to the standard volume measure can be expressed in spherical coordinates as: Vf(x)dV(x)=Sd×(0,)f(rω)d(σμd)(ω,r)\int_{V} f(x) \, dV(x) = \int_{S^d \times (0, \infty)} f(r \omega) \, d(\sigma \otimes \mu_d)(\omega, r) where SdVS^d \subset V is the unit sphere, σ\sigma is the surface measure on SdS^d, and μd\mu_d is the radial measure on the interval (0,)(0, \infty) defined by dμd(r)=rddrd\mu_d(r) = r^d \, dr, where dd is the dimension of the space minus one.

instance

The Lebesgue measure on (0,)(0, \infty) is ss-finite

Let λ\lambda be the standard Lebesgue measure (volume) on the real numbers R\mathbb{R}. The measure on the interval of positive real numbers (0,)(0, \infty) obtained by the pullback of λ\lambda under the inclusion map ι:(0,)R\iota: (0, \infty) \hookrightarrow \mathbb{R} is ss-finite.

theorem

Spherical Integration Formula for Lebesgue Integral in Space(d+1)\text{Space}(d+1)

For any natural number dd and any measurable function f:Space(d+1)[0,]f: \text{Space}(d+1) \to [0, \infty], the Lebesgue integral of ff with respect to the volume measure on the (d+1)(d+1)-dimensional Euclidean space Space(d+1)\text{Space}(d+1) is given by: Space(d+1)f(x)dvol=Sd×(0,)f(rω)d(σ×μd)\int_{\text{Space}(d+1)} f(x) \, d\text{vol} = \int_{S^d \times (0, \infty)} f(r\omega) \, d(\sigma \times \mu_d) where SdS^d is the unit sphere in Space(d+1)\text{Space}(d+1), ωSd\omega \in S^d is a unit vector, r(0,)r \in (0, \infty) is the radius, σ\sigma is the spherical measure, and μd\mu_d is the radial measure on (0,)(0, \infty) defined by rddrr^d dr.

theorem

Spherical Integration Formula with Radial Weight rdr^d in Space(d+1)\text{Space}(d+1)

For any natural number dd and any measurable function f:Space(d+1)[0,]f: \text{Space}(d+1) \to [0, \infty], the Lebesgue integral of ff with respect to the volume measure on the (d+1)(d+1)-dimensional real vector space Space(d+1)\text{Space}(d+1) is given by: Space(d+1)f(x)dvol=Sd×(0,)f(rω)rdd(σ×λ)\int_{\text{Space}(d+1)} f(x) \, d\text{vol} = \int_{S^d \times (0, \infty)} f(r\omega) \cdot r^d \, d(\sigma \times \lambda) where SdS^d is the unit sphere in Space(d+1)\text{Space}(d+1), σ\sigma is the spherical measure on SdS^d, and λ\lambda is the standard Lebesgue measure on the positive real line (0,)(0, \infty). In this expression, r(0,)r \in (0, \infty) represents the radius and ωSd\omega \in S^d is a unit vector.