PhyslibAlpha.SpaceAndTime.Space.Surfaces.Ring

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 PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell
public import Physlib.SpaceAndTime.Space.Translations
public import Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Ring surface in `Space 3`

@[expose] public section

A. The definition of the ring surface

The embedding of the unit ring (a circle S¹ in Space 2) into Space 3.

def ring : Metric.sphere (0 : Space 2) 1 → Space 3 := fun x =>
  (slice 2).symm (0, Space.sphericalShell 2 x)

              lemma ring_eq : ring = (slice 2).symm ∘ (fun x => (0, sphericalShell 2 x)) := rfllemma ring_injective : Function.Injective ring := by⊢ Function.Injective ring
  intro x y hx:↑(Metric.sphere 0 1)y:↑(Metric.sphere 0 1)h:ring x = ring y⊢ x = y
  simp [ring] at hx:↑(Metric.sphere 0 1)y:↑(Metric.sphere 0 1)h:sphericalShell 2 x = sphericalShell 2 y⊢ x = y
  exact sphericalShell_injective _ hAll goals completed! 🐙@[fun_prop]
lemma ring_continuous : Continuous ring := by⊢ Continuous ring
  apply Continuous.comphg⊢ Continuous ⇑(slice 2).symmhf⊢ Continuous fun x => (0, sphericalShell 2 x)
  ·hg⊢ Continuous ⇑(slice 2).symm fun_propAll goals completed! 🐙
  ·hf⊢ Continuous fun x => (0, sphericalShell 2 x) fun_propAll goals completed! 🐙lemma ring_measurableEmbedding : MeasurableEmbedding ring :=
  Continuous.measurableEmbedding ring_continuous ring_injective

B. The measure associated with the ring

The measure on Space 3 corresponding to integration around a ring.

def ringMeasure : Measure (Space 3) :=
  MeasureTheory.Measure.map ring (MeasureTheory.Measure.toSphere volume)

              

instance ringMeasure_hasTemperateGrowth :
    ringMeasure.HasTemperateGrowth := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ ringMeasure.HasTemperateGrowth
  rw [ringMeasure𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ (Measure.map ring volume.toSphere).HasTemperateGrowth𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ (Measure.map ring volume.toSphere).HasTemperateGrowth]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ (Measure.map ring volume.toSphere).HasTemperateGrowth
  refine { exists_integrable := ?_ }𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ ∃ n, Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) (Measure.map ring volume.toSphere)
  use 0h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ Integrable (fun x => (1 + ‖x‖) ^ (-↑0)) (Measure.map ring volume.toSphere)
  simpAll goals completed! 🐙instance ringMeasure_prod_volume_hasTemperateGrowth :
    (ringMeasure.prod (volume (α := Space))).HasTemperateGrowth := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ (ringMeasure.prod volume).HasTemperateGrowth
  exact IsDistBounded.instHasTemperateGrowthProdProdOfOpensMeasurableSpace ringMeasure volumeAll goals completed! 🐙

instance ringMeasure_sFinite: SFinite ringMeasure := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ SFinite ringMeasure
  rw [ringMeasure𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ SFinite (Measure.map ring volume.toSphere)𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ SFinite (Measure.map ring volume.toSphere)]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ SFinite (Measure.map ring volume.toSphere)
  exact Measure.instSFiniteMap volume.toSphere ringAll goals completed! 🐙

instance ringMeasure_finite: IsFiniteMeasure ringMeasure := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ IsFiniteMeasure ringMeasure
  rw [ringMeasure𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ IsFiniteMeasure (Measure.map ring volume.toSphere)𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ IsFiniteMeasure (Measure.map ring volume.toSphere)]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ IsFiniteMeasure (Measure.map ring volume.toSphere)
  exact Measure.isFiniteMeasure_map volume.toSphere ringAll goals completed! 🐙

lemma integrable_ringMeasure_of_continuous (f : Space → ℝ) (hf : Continuous (f ∘ ring)) :
    Integrable f ringMeasure := byf:Space → ℝhf:Continuous (f ∘ ring)⊢ Integrable f ringMeasure
  rw [ringMeasuref:Space → ℝhf:Continuous (f ∘ ring)⊢ Integrable f (Measure.map ring volume.toSphere)f:Space → ℝhf:Continuous (f ∘ ring)⊢ Integrable f (Measure.map ring volume.toSphere)]f:Space → ℝhf:Continuous (f ∘ ring)⊢ Integrable f (Measure.map ring volume.toSphere)
  rw [MeasurableEmbedding.integrable_map_ifff:Space → ℝhf:Continuous (f ∘ ring)⊢ Integrable (f ∘ ring) volume.toSpherehff:Space → ℝhf:Continuous (f ∘ ring)⊢ MeasurableEmbedding ringf:Space → ℝhf:Continuous (f ∘ ring)⊢ Integrable (f ∘ ring) volume.toSpherehff:Space → ℝhf:Continuous (f ∘ ring)⊢ MeasurableEmbedding ring]f:Space → ℝhf:Continuous (f ∘ ring)⊢ Integrable (f ∘ ring) volume.toSpherehff:Space → ℝhf:Continuous (f ∘ ring)⊢ MeasurableEmbedding ring
  ·f:Space → ℝhf:Continuous (f ∘ ring)⊢ Integrable (f ∘ ring) volume.toSphere let f' : BoundedContinuousFunction (Metric.sphere (0 : Space 2) 1) ℝ :=
      BoundedContinuousFunction.mkOfCompact ⟨f ∘ ring, hf⟩f:Space → ℝhf:Continuous (f ∘ ring)f':BoundedContinuousFunction ↑(Metric.sphere 0 1) ℝ := BoundedContinuousFunction.mkOfCompact { toFun := f ∘ ring, continuous_toFun := hf }⊢ Integrable (f ∘ ring) volume.toSphere
    exact BoundedContinuousFunction.integrable _ f'All goals completed! 🐙
  ·hff:Space → ℝhf:Continuous (f ∘ ring)⊢ MeasurableEmbedding ring exact ring_measurableEmbeddingAll goals completed! 🐙

lemma integrable_ringMeasure_of_continuous_euclid (f : Space → EuclideanSpace ℝ (Fin n))
    (hf : Continuous (f ∘ ring)) :
    Integrable f ringMeasure := byn:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ Integrable f ringMeasure
  rw [ringMeasuren:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ Integrable f (Measure.map ring volume.toSphere)n:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ Integrable f (Measure.map ring volume.toSphere)]n:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ Integrable f (Measure.map ring volume.toSphere)
  rw [MeasurableEmbedding.integrable_map_iffn:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ Integrable (f ∘ ring) volume.toSpherehfn:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ MeasurableEmbedding ringn:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ Integrable (f ∘ ring) volume.toSpherehfn:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ MeasurableEmbedding ring]n:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ Integrable (f ∘ ring) volume.toSpherehfn:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ MeasurableEmbedding ring
  ·n:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ Integrable (f ∘ ring) volume.toSphere exact BoundedContinuousFunction.integrable _
      (BoundedContinuousFunction.mkOfCompact ⟨f ∘ ring, hf⟩)All goals completed! 🐙
  ·hfn:ℕf:Space → EuclideanSpace ℝ (Fin n)hf:Continuous (f ∘ ring)⊢ MeasurableEmbedding ring exact ring_measurableEmbeddingAll goals completed! 🐙lemma ringMeasure_prod_volume_map :
    (ringMeasure.prod (volume (α := Space))).map (fun x : Space × Space => (x.1, x.2 + x.1))
     = (ringMeasure.prod (volume (α := Space))) := by⊢ Measure.map (fun x => (x.1, x.2 + x.1)) (ringMeasure.prod volume) = ringMeasure.prod volume
  refine (MeasureTheory.MeasurePreserving.skew_product (f := id) (g := fun x => fun y => y + x)
    ?_ ?_ ?_).map_eqrefine_1⊢ MeasurePreserving id ringMeasure ringMeasurerefine_2⊢ Measurable (Function.uncurry fun x y => y + x)refine_3⊢ ∀ᵐ (a : Space) ∂ringMeasure, Measure.map (fun y => y + a) volume = volume
  ·refine_1⊢ MeasurePreserving id ringMeasure ringMeasure exact MeasurePreserving.id ringMeasureAll goals completed! 🐙
  ·refine_2⊢ Measurable (Function.uncurry fun x y => y + x) fun_propAll goals completed! 🐙
  ·refine_3⊢ ∀ᵐ (a : Space) ∂ringMeasure, Measure.map (fun y => y + a) volume = volume filter_upwards with xrefine_3x:Space⊢ Measure.map (fun y => y + x) volume = volume
    exact Measure.IsAddRightInvariant.map_add_right_eq_self (x)All goals completed! 🐙

@[simp]
lemma ringMeasure_univ : ringMeasure Set.univ = ENNReal.ofReal ((2 : ℝ) * π) := by⊢ ringMeasure Set.univ = ENNReal.ofReal (2 * π)
  rw [ringMeasure,⊢ (Measure.map ring volume.toSphere) Set.univ = ENNReal.ofReal (2 * π)⊢ volume.toSphere (ring ⁻¹' Set.univ) = ENNReal.ofReal (2 * π)hf⊢ Measurable ringhs⊢ MeasurableSet Set.univ Measure.map_apply⊢ volume.toSphere (ring ⁻¹' Set.univ) = ENNReal.ofReal (2 * π)hf⊢ Measurable ringhs⊢ MeasurableSet Set.univ⊢ volume.toSphere (ring ⁻¹' Set.univ) = ENNReal.ofReal (2 * π)hf⊢ Measurable ringhs⊢ MeasurableSet Set.univ]⊢ volume.toSphere (ring ⁻¹' Set.univ) = ENNReal.ofReal (2 * π)hf⊢ Measurable ringhs⊢ MeasurableSet Set.univ
  simp only [Set.preimage_univ, Measure.toSphere_apply_univ, finrank_eq_dim, Nat.cast_ofNat,
    volume_metricBall_two, Nat.ofNat_nonneg, ENNReal.ofReal_mul, ENNReal.ofReal_ofNat]hf⊢ Measurable ringhs⊢ MeasurableSet Set.univ
  ·hf⊢ Measurable ring fun_propAll goals completed! 🐙
  ·hs⊢ MeasurableSet Set.univ exact MeasurableSet.univAll goals completed! 🐙

C. The distribution associated with the ring

The distribution on Space 3 corresponding to integration around a ring.

def ringDist : (Space 3) →d[ℝ] ℝ  :=
  SchwartzMap.integralCLM ℝ ringMeasure



lemma ringDist_apply_eq_integral_ringMeasure (f : 𝓢(Space 3, ℝ)) :
    ringDist f = ∫ x, f x ∂ringMeasure := byf:𝓢(Space, ℝ)⊢ ringDist f = ∫ (x : Space), f x ∂ringMeasure
  rw [ringDist,f:𝓢(Space, ℝ)⊢ (integralCLM ℝ ringMeasure) f = ∫ (x : Space), f x ∂ringMeasureAll goals completed! 🐙 SchwartzMap.integralCLM_applyf:𝓢(Space, ℝ)⊢ ∫ (x : Space), f x ∂ringMeasure = ∫ (x : Space), f x ∂ringMeasureAll goals completed! 🐙]All goals completed! 🐙



lemma ringDist_eq_integral_delta (f : 𝓢(Space 3, ℝ)) :
    ringDist f = ∫ z, diracDelta ℝ z f ∂ringMeasure := byf:𝓢(Space, ℝ)⊢ ringDist f = ∫ (z : Space), (diracDelta ℝ z) f ∂ringMeasure
  rw [ringDist_apply_eq_integral_ringMeasuref:𝓢(Space, ℝ)⊢ ∫ (x : Space), f x ∂ringMeasure = ∫ (z : Space), (diracDelta ℝ z) f ∂ringMeasuref:𝓢(Space, ℝ)⊢ ∫ (x : Space), f x ∂ringMeasure = ∫ (z : Space), (diracDelta ℝ z) f ∂ringMeasure]f:𝓢(Space, ℝ)⊢ ∫ (x : Space), f x ∂ringMeasure = ∫ (z : Space), (diracDelta ℝ z) f ∂ringMeasure
  simpAll goals completed! 🐙

Ring surface in Space 3

A. The definition of the ring surface

B. The measure associated with the ring

C. The distribution associated with the ring

Ring surface in `Space 3`