1. PhyslibAlpha
  2. SpaceAndTime
  3. Space
  4. Surfaces
  5. SolidSphere
Imports
/- Copyright (c) 2026 Robert Sneiderman. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Robert Sneiderman -/ module public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell public import Physlib.SpaceAndTime.Space.Integrals.Basic public import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Solid sphere surfaces in Space d

The solid sphere is the closed unit ball in Space d. Unlike the line or the spherical shell, it is a region of positive ambient volume, so the measure associated with it is the ambient volume restricted to the ball rather than a pushforward of a lower-dimensional measure. The requirement that the surface has ambient measure zero is therefore not applicable here, and is replaced by a statement that the solid sphere has positive ambient volume.

@[expose] public section

A. The definition of the solid sphere surface

The inclusion into Space d of its closed unit ball B^d (the subtype coercion x ↦ x.1).

def solidSphere (d : ℕ) : Metric.closedBall (0 : Space d) 1 → Space d := fun x => x.1
lemma solidSphere_injective (d : ℕ) : Function.Injective (solidSphere d) := d:ℕ⊢ Function.Injective (solidSphere d) d:ℕx:↑(Metric.closedBall 0 1)y:↑(Metric.closedBall 0 1)h:solidSphere d x = solidSphere d y⊢ x = y d:ℕx:↑(Metric.closedBall 0 1)y:↑(Metric.closedBall 0 1)h:↑x = ↑y⊢ x = y All goals completed! 🐙lemma solidSphere_continuous (d : ℕ) : Continuous (solidSphere d) := continuous_subtype_vallemma solidSphere_measurableEmbedding (d : ℕ) : MeasurableEmbedding (solidSphere d) := d:ℕ⊢ MeasurableEmbedding (solidSphere d) d:ℕ⊢ Continuous (solidSphere d)d:ℕ⊢ Function.Injective (solidSphere d) d:ℕ⊢ Continuous (solidSphere d) All goals completed! 🐙 d:ℕ⊢ Function.Injective (solidSphere d) All goals completed! 🐙d:ℕx:↑(Metric.closedBall 0 1)hx:‖↑x‖ ≤ 1⊢ ‖solidSphere d x‖ ≤ 1 All goals completed! 🐙

B. The measure associated with the solid sphere

The measure on Space d corresponding to integration over a solid sphere, i.e. the ambient volume measure restricted to the closed unit ball.

def solidSphereMeasure (d : ℕ) : Measure (Space d) := volume.restrict (Metric.closedBall (0 : Space d) 1)
𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ volume (Metric.closedBall 0 1) ≠ ⊤ All goals completed! 🐙instance solidSphereMeasure_hasTemperateGrowth (d : ℕ) : (solidSphereMeasure d).HasTemperateGrowth := inferInstance

C. The distribution associated with the solid sphere

The distribution on Space d corresponding to integration over a solid sphere. One can roughly think of this distribution as taking a test function f to its integral against a mass, charge or current density spread over a solid ball.

def solidSphereDist (d : ℕ) : (Space d) →d[ℝ] ℝ := SchwartzMap.integralCLM ℝ (solidSphereMeasure d)
All goals completed! 🐙All goals completed! 🐙

D. The solid sphere has positive ambient volume

lemma solidSphere_volume_pos (d : ℕ) : 0 < volume (Metric.closedBall (0 : Space d) 1) := d:ℕ⊢ 0 < volume (Metric.closedBall 0 1) d:ℕ⊢ 0 < volume (Metric.ball 0 1)d:ℕ⊢ volume (Metric.ball 0 1) ≤ volume (Metric.closedBall 0 1) d:ℕ⊢ 0 < volume (Metric.ball 0 1) All goals completed! 🐙 d:ℕ⊢ volume (Metric.ball 0 1) ≤ volume (Metric.closedBall 0 1) All goals completed! 🐙d:ℕ⊢ 0 < volume (Metric.closedBall 0 1) All goals completed! 🐙