PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell

Imports

/-
Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.SpaceAndTime.Space.ConstantSliceDist
public import Physlib.SpaceAndTime.Space.Norm.Basic
public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Spherical surfaces on Space.

@[expose] public section

A. The definition of the spherical shell surface

The inclusion into Space d of its unit sphere S^{d-1} (the subtype coercion x ↦ x.1).

def sphericalShell (d : ℕ) : Metric.sphere (0 : Space d) 1 → Space d := fun x => x.1

              lemma sphericalShell_injective (d : ℕ) : Function.Injective (sphericalShell d) := byd:ℕ⊢ Function.Injective (sphericalShell d)
  intro x y hd:ℕx:↑(Metric.sphere 0 1)y:↑(Metric.sphere 0 1)h:sphericalShell d x = sphericalShell d y⊢ x = y
  simp [sphericalShell] at hd:ℕx:↑(Metric.sphere 0 1)y:↑(Metric.sphere 0 1)h:↑x = ↑y⊢ x = y
  grindAll goals completed! 🐙lemma sphericalShell_continuous (d : ℕ) : Continuous (sphericalShell d) := continuous_subtype_vallemma sphericalShell_measurableEmbedding (d : ℕ) : MeasurableEmbedding (sphericalShell d) := byd:ℕ⊢ MeasurableEmbedding (sphericalShell d)
  apply Continuous.measurableEmbeddingf_contd:ℕ⊢ Continuous (sphericalShell d)f_injd:ℕ⊢ Function.Injective (sphericalShell d)
  ·f_contd:ℕ⊢ Continuous (sphericalShell d) exact sphericalShell_continuous dAll goals completed! 🐙
  ·f_injd:ℕ⊢ Function.Injective (sphericalShell d) exact sphericalShell_injective dAll goals completed! 🐙@[simp]
lemma norm_sphericalShell (d : ℕ) (x : Metric.sphere (0 : Space d) 1) :
    ‖sphericalShell d x‖ = 1 := byd:ℕx:↑(Metric.sphere 0 1)⊢ ‖sphericalShell d x‖ = 1
  simp [sphericalShell, Metric.sphere]All goals completed! 🐙

B. The measure associated with the spherical shell

The measure on Space d corresponding to integration around a spherical shell.

def sphericalShellMeasure (d : ℕ) : Measure (Space d) :=
  MeasureTheory.Measure.map (sphericalShell d) (MeasureTheory.Measure.toSphere volume)



instance sphericalShellMeasure_hasTemperateGrowth (d : ℕ) :
    (sphericalShellMeasure d).HasTemperateGrowth := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ (sphericalShellMeasure d).HasTemperateGrowth
  rw [sphericalShellMeasure𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ (Measure.map (sphericalShell d) volume.toSphere).HasTemperateGrowth𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ (Measure.map (sphericalShell d) volume.toSphere).HasTemperateGrowth]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ (Measure.map (sphericalShell d) volume.toSphere).HasTemperateGrowth
  refine { exists_integrable := ?_ }𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ ∃ n, Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) (Measure.map (sphericalShell d) volume.toSphere)
  use 0h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ Integrable (fun x => (1 + ‖x‖) ^ (-↑0)) (Measure.map (sphericalShell d) volume.toSphere)
  simpAll goals completed! 🐙

C. The distribution associated with the spherical shell

The distribution associated with a spherical shell. One can roughly think of this distribution as the distribution which takes test functions f (r) to ∫ d³r f(r) ρ(r) where ρ(r) is the mass, charge or current etc. distribution.

def sphericalShellDist (d : ℕ) : (Space d) →d[ℝ] ℝ  :=
  SchwartzMap.integralCLM ℝ (sphericalShellMeasure d)




lemma sphericalShellDist_apply_eq_integral_sphericalShellMeasure (d : ℕ) (f : 𝓢(Space d, ℝ)) :
    sphericalShellDist d f = ∫ x, f x ∂sphericalShellMeasure d := byd:ℕf:𝓢(Space d, ℝ)⊢ (sphericalShellDist d) f = ∫ (x : Space d), f x ∂sphericalShellMeasure d
  rw [sphericalShellDist,d:ℕf:𝓢(Space d, ℝ)⊢ (integralCLM ℝ (sphericalShellMeasure d)) f = ∫ (x : Space d), f x ∂sphericalShellMeasure dAll goals completed! 🐙 SchwartzMap.integralCLM_applyd:ℕf:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), f x ∂sphericalShellMeasure d = ∫ (x : Space d), f x ∂sphericalShellMeasure dAll goals completed! 🐙]All goals completed! 🐙



lemma sphericalShellDist_apply_eq_integral_sphere_volume (d : ℕ) (f : 𝓢(Space d, ℝ)) :
    sphericalShellDist d f =
    ∫ x, f (sphericalShell d x) ∂(MeasureTheory.Measure.toSphere volume) := byd:ℕf:𝓢(Space d, ℝ)⊢ (sphericalShellDist d) f = ∫ (x : ↑(Metric.sphere 0 1)), f (sphericalShell d x) ∂volume.toSphere
  rw [sphericalShellDist_apply_eq_integral_sphericalShellMeasure,d:ℕf:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), f x ∂sphericalShellMeasure d = ∫ (x : ↑(Metric.sphere 0 1)), f (sphericalShell d x) ∂volume.toSphereAll goals completed! 🐙 sphericalShellMeasure,d:ℕf:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), f x ∂Measure.map (sphericalShell d) volume.toSphere =
  ∫ (x : ↑(Metric.sphere 0 1)), f (sphericalShell d x) ∂volume.toSphereAll goals completed! 🐙
   MeasurableEmbedding.integral_map (sphericalShell_measurableEmbedding d)d:ℕf:𝓢(Space d, ℝ)⊢ ∫ (x : ↑(Metric.sphere 0 1)), f (sphericalShell d x) ∂volume.toSphere =
  ∫ (x : ↑(Metric.sphere 0 1)), f (sphericalShell d x) ∂volume.toSphereAll goals completed! 🐙]All goals completed! 🐙