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)={y∈Space(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({y∈Space(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 {x∈Space 3∣∥x∥<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 {x∈Space 2∣∥x∥<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({x∈Space 2∣∥x∥<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 {x∈Space 3∣∥x∥<1}\{x \in \text{Space } 3 \mid \|x\| < 1\}, is equal to 43π\frac{4}{3}\pi.

theorem

∫Space(1)f=∫Rf∘oneEquiv−1\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(oneEquiv−1(x)) dx \int_{\text{Space}(1)} f(x) \, dV = \int_{\mathbb{R}} f(\text{oneEquiv}^{-1}(x)) \, dx where oneEquiv−1\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:V→Ff: 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 Sd⊂VS^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)=rd drd\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ω)⋅rd d(σ×λ)\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.