Uniform Euclidean spherical shells

Normalized sphere measure and spherical shell charges on Position.

noncomputable def LiebThirring.unitSphereMeasure : MeasureTheory.Measure ↑(Metric.sphere 0 1)

Uniform probability measure on the physical Euclidean unit sphere.

Equations

• LiebThirring.unitSphereMeasure = (MeasureTheory.volume.toSphere Set.univ)⁻¹ • MeasureTheory.volume.toSphere

instance LiebThirring.instIsProbabilityMeasureUnitSphereMeasure : MeasureTheory.IsProbabilityMeasure unitSphereMeasure

noncomputable def LiebThirring.shell (a : Position) (r : ℝ) : MeasureTheory.Measure Position

The pushforward of uniform unit-sphere probability by ω ↦ a + r • ω.

Equations

• LiebThirring.shell a r = MeasureTheory.Measure.map (fun (ω : ↑(Metric.sphere 0 1)) => a + r • ↑ω) LiebThirring.unitSphereMeasure

theorem LiebThirring.measurable_shellMap (a : Position) (r : ℝ) : Measurable fun (ω : ↑(Metric.sphere 0 1)) => a + r • ↑ω

instance LiebThirring.instIsProbabilityMeasureShell (a : Position) (r : ℝ) : MeasureTheory.IsProbabilityMeasure (shell a r)

theorem LiebThirring.ae_shell_norm (a : Position) {r : ℝ} (hr : 0 ≤ r) : ∀ᵐ (y : Position) ∂shell a r, ‖y - a‖ = r

theorem LiebThirring.sphere_area : MeasureTheory.volume.toSphere Set.univ = ENNReal.ofReal (4 * Real.pi)

The Euclidean unit sphere has area 4π in Mathlib's cone normalization.

def LiebThirring.unitSphereRotation (Q : Position ≃ₗᵢ[ℝ] Position) (ω : ↑(Metric.sphere 0 1)) : ↑(Metric.sphere 0 1)

The restriction of a linear isometry to the unit sphere.

Equations

• LiebThirring.unitSphereRotation Q ω = ⟨Q ↑ω, ⋯⟩

theorem LiebThirring.measurable_unitSphereRotation (Q : Position ≃ₗᵢ[ℝ] Position) : Measurable (unitSphereRotation Q)

theorem LiebThirring.map_toSphere_unitSphereRotation (Q : Position ≃ₗᵢ[ℝ] Position) : MeasureTheory.Measure.map (unitSphereRotation Q) MeasureTheory.volume.toSphere = MeasureTheory.volume.toSphere

theorem LiebThirring.map_unitSphereMeasure_rotation (Q : Position ≃ₗᵢ[ℝ] Position) : MeasureTheory.Measure.map (unitSphereRotation Q) unitSphereMeasure = unitSphereMeasure