PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalCylinder

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.Ring
public import Physlib.SpaceAndTime.Space.Integrals.Basic
public import Mathlib.MeasureTheory.Integral.Prod

Spherical cylinder surface in `Space 3`

The spherical cylinder is the unit circular shell in Space 2 extruded along the third coordinate.

@[expose] public section

A. The definition of the spherical cylinder surface

The map embedding the unit circular shell extruded along the axis into Space 3.

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

              lemma sphericalCylinder_eq :
    sphericalCylinder = (slice 2).symm ∘ (fun x => (x.2, sphericalShell 2 x.1)) := rfllemma sphericalCylinder_injective : Function.Injective sphericalCylinder := by⊢ Function.Injective sphericalCylinder
  intro x y hx:↑(Metric.sphere 0 1) × ℝy:↑(Metric.sphere 0 1) × ℝh:sphericalCylinder x = sphericalCylinder y⊢ x = y
  have h' := congrArg (slice 2) hx:↑(Metric.sphere 0 1) × ℝy:↑(Metric.sphere 0 1) × ℝh:sphericalCylinder x = sphericalCylinder yh':(slice 2) (sphericalCylinder x) = (slice 2) (sphericalCylinder y)⊢ x = y
  simp [sphericalCylinder] at h'x:↑(Metric.sphere 0 1) × ℝy:↑(Metric.sphere 0 1) × ℝh:sphericalCylinder x = sphericalCylinder yh':x.2 = y.2 ∧ sphericalShell 2 x.1 = sphericalShell 2 y.1⊢ x = y
  exact Prod.ext (sphericalShell_injective 2 h'.2) h'.1All goals completed! 🐙@[fun_prop]
lemma sphericalCylinder_continuous : Continuous sphericalCylinder := by⊢ Continuous sphericalCylinder
  apply Continuous.comphg⊢ Continuous ⇑(slice 2).symmhf⊢ Continuous fun x => (x.2, sphericalShell 2 x.1)
  ·hg⊢ Continuous ⇑(slice 2).symm fun_propAll goals completed! 🐙
  ·hf⊢ Continuous fun x => (x.2, sphericalShell 2 x.1) fun_propAll goals completed! 🐙lemma sphericalCylinder_measurableEmbedding : MeasurableEmbedding sphericalCylinder :=
  Continuous.measurableEmbedding sphericalCylinder_continuous sphericalCylinder_injective

@[simp]
lemma norm_sphericalCylinder (x : Metric.sphere (0 : Space 2) 1 × ℝ) :
    ‖sphericalCylinder x‖ = √(‖x.2‖ ^ 2 + 1) := byx:↑(Metric.sphere 0 1) × ℝ⊢ ‖sphericalCylinder x‖ = √(‖x.2‖ ^ 2 + 1)
  rw [sphericalCylinder,x:↑(Metric.sphere 0 1) × ℝ⊢ ‖(slice 2).symm (x.2, sphericalShell 2 x.1)‖ = √(‖x.2‖ ^ 2 + 1)x:↑(Metric.sphere 0 1) × ℝ⊢ √(‖x.2‖ ^ 2 + 1 ^ 2) = √(‖x.2‖ ^ 2 + 1) norm_slice_symm_eq,x:↑(Metric.sphere 0 1) × ℝ⊢ √(‖x.2‖ ^ 2 + ‖sphericalShell 2 x.1‖ ^ 2) = √(‖x.2‖ ^ 2 + 1)x:↑(Metric.sphere 0 1) × ℝ⊢ √(‖x.2‖ ^ 2 + 1 ^ 2) = √(‖x.2‖ ^ 2 + 1) norm_sphericalShellx:↑(Metric.sphere 0 1) × ℝ⊢ √(‖x.2‖ ^ 2 + 1 ^ 2) = √(‖x.2‖ ^ 2 + 1)x:↑(Metric.sphere 0 1) × ℝ⊢ √(‖x.2‖ ^ 2 + 1 ^ 2) = √(‖x.2‖ ^ 2 + 1)]x:↑(Metric.sphere 0 1) × ℝ⊢ √(‖x.2‖ ^ 2 + 1 ^ 2) = √(‖x.2‖ ^ 2 + 1)
  norm_numAll goals completed! 🐙

B. The measure associated with the spherical cylinder

The measure on Space 3 corresponding to integration over a spherical cylinder.

def sphericalCylinderMeasure : Measure (Space 3) :=
  MeasureTheory.Measure.map sphericalCylinder
    ((MeasureTheory.Measure.toSphere volume).prod (volume (α := ℝ)))



instance sphericalCylinderMeasure_hasTemperateGrowth :
    sphericalCylinderMeasure.HasTemperateGrowth := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ sphericalCylinderMeasure.HasTemperateGrowth
  rw [sphericalCylinderMeasure𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ (Measure.map sphericalCylinder (volume.toSphere.prod volume)).HasTemperateGrowth𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ (Measure.map sphericalCylinder (volume.toSphere.prod volume)).HasTemperateGrowth]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ (Measure.map sphericalCylinder (volume.toSphere.prod volume)).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 sphericalCylinder (volume.toSphere.prod volume))
  obtain ⟨n, hn⟩ := MeasureTheory.Measure.HasTemperateGrowth.exists_integrable
    (μ := volume (α := ℝ))𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ ∃ n, Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) (Measure.map sphericalCylinder (volume.toSphere.prod volume))
  use nh𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) (Measure.map sphericalCylinder (volume.toSphere.prod volume))
  rw [MeasurableEmbedding.integrable_map_iff sphericalCylinder_measurableEmbeddingh𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ Integrable ((fun x => (1 + ‖x‖) ^ (-↑n)) ∘ sphericalCylinder) (volume.toSphere.prod volume)h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ Integrable ((fun x => (1 + ‖x‖) ^ (-↑n)) ∘ sphericalCylinder) (volume.toSphere.prod volume)]h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ Integrable ((fun x => (1 + ‖x‖) ^ (-↑n)) ∘ sphericalCylinder) (volume.toSphere.prod volume)
  change Integrable
    (fun x : Metric.sphere (0 : Space 2) 1 × ℝ =>
      (1 + ‖sphericalCylinder x‖) ^ (-(n : ℝ)))
    ((MeasureTheory.Measure.toSphere volume).prod (volume (α := ℝ)))h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ Integrable (fun x => (1 + ‖sphericalCylinder x‖) ^ (-↑n)) (volume.toSphere.prod volume)
  apply Integrable.mono' (hn.comp_snd (MeasureTheory.Measure.toSphere volume))h.hf𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ AEStronglyMeasurable (fun x => (1 + ‖sphericalCylinder x‖) ^ (-↑n)) (volume.toSphere.prod volume)h.h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ ∀ᵐ (a : ↑(Metric.sphere 0 1) × ℝ) ∂volume.toSphere.prod volume,
  ‖(1 + ‖sphericalCylinder a‖) ^ (-↑n)‖ ≤ (1 + ‖a.2‖) ^ (-↑n)
  ·h.hf𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ AEStronglyMeasurable (fun x => (1 + ‖sphericalCylinder x‖) ^ (-↑n)) (volume.toSphere.prod volume) apply AEMeasurable.aestronglyMeasurableh.hf𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ AEMeasurable (fun x => (1 + ‖sphericalCylinder x‖) ^ (-↑n)) (volume.toSphere.prod volume)
    exact ((continuous_const.add sphericalCylinder_continuous.norm).rpow_const
      (fun x => Or.inl (by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ 1 + ‖sphericalCylinder x‖ ≠ 0 positivityAll goals completed! 🐙 : (1 : ℝ) + ‖sphericalCylinder x‖ ≠ 0))).aemeasurable
  ·h.h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ ∀ᵐ (a : ↑(Metric.sphere 0 1) × ℝ) ∂volume.toSphere.prod volume,
  ‖(1 + ‖sphericalCylinder a‖) ^ (-↑n)‖ ≤ (1 + ‖a.2‖) ^ (-↑n) filter_upwards with xh.h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ ‖(1 + ‖sphericalCylinder x‖) ^ (-↑n)‖ ≤ (1 + ‖x.2‖) ^ (-↑n)
    rw [Real.norm_eq_abs,h.h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ |(1 + ‖sphericalCylinder x‖) ^ (-↑n)| ≤ (1 + ‖x.2‖) ^ (-↑n)h.h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ (1 + ‖sphericalCylinder x‖) ^ (-↑n) ≤ (1 + ‖x.2‖) ^ (-↑n) abs_of_nonneg (Real.rpow_nonneg (by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ 0 ≤ 1 + ‖sphericalCylinder x‖h.h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ (1 + ‖sphericalCylinder x‖) ^ (-↑n) ≤ (1 + ‖x.2‖) ^ (-↑n) positivityAll goals completed! 🐙h.h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ (1 + ‖sphericalCylinder x‖) ^ (-↑n) ≤ (1 + ‖x.2‖) ^ (-↑n)) _)]h.h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ (1 + ‖sphericalCylinder x‖) ^ (-↑n) ≤ (1 + ‖x.2‖) ^ (-↑n)
    apply Real.rpow_le_rpow_of_nonposh.h.hx𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ 0 < 1 + ‖x.2‖h.h.hxy𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ 1 + ‖x.2‖ ≤ 1 + ‖sphericalCylinder x‖h.h.hz𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ -↑n ≤ 0
    ·h.h.hx𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ 0 < 1 + ‖x.2‖ positivityAll goals completed! 🐙
    ·h.h.hxy𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ 1 + ‖x.2‖ ≤ 1 + ‖sphericalCylinder x‖ simp only [norm_sphericalCylinder]h.h.hxy𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ 1 + ‖x.2‖ ≤ 1 + √(‖x.2‖ ^ 2 + 1)
      exact add_le_add_right (Real.le_sqrt_of_sq_le (le_add_of_nonneg_right zero_le_one)) 1All goals completed! 🐙
    ·h.h.hz𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:↑(Metric.sphere 0 1) × ℝ⊢ -↑n ≤ 0 simpAll goals completed! 🐙



instance sphericalCylinderMeasure_sFinite : SFinite sphericalCylinderMeasure := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ SFinite sphericalCylinderMeasure
  rw [sphericalCylinderMeasure𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ SFinite (Measure.map sphericalCylinder (volume.toSphere.prod volume))𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ SFinite (Measure.map sphericalCylinder (volume.toSphere.prod volume))]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ SFinite (Measure.map sphericalCylinder (volume.toSphere.prod volume))
  exact Measure.instSFiniteMap ((MeasureTheory.Measure.toSphere volume).prod (volume (α := ℝ)))
    sphericalCylinderAll goals completed! 🐙

C. The distribution associated with the spherical cylinder

The distribution on Space 3 corresponding to integration over a spherical cylinder.

def sphericalCylinderDist : (Space 3) →d[ℝ] ℝ :=
  SchwartzMap.integralCLM ℝ sphericalCylinderMeasure



lemma sphericalCylinderDist_apply_eq_integral_sphericalCylinderMeasure (f : 𝓢(Space 3, ℝ)) :
    sphericalCylinderDist f = ∫ x, f x ∂sphericalCylinderMeasure := byf:𝓢(Space, ℝ)⊢ sphericalCylinderDist f = ∫ (x : Space), f x ∂sphericalCylinderMeasure
  rw [sphericalCylinderDist,f:𝓢(Space, ℝ)⊢ (integralCLM ℝ sphericalCylinderMeasure) f = ∫ (x : Space), f x ∂sphericalCylinderMeasureAll goals completed! 🐙 SchwartzMap.integralCLM_applyf:𝓢(Space, ℝ)⊢ ∫ (x : Space), f x ∂sphericalCylinderMeasure = ∫ (x : Space), f x ∂sphericalCylinderMeasureAll goals completed! 🐙]All goals completed! 🐙



lemma sphericalCylinderDist_apply_eq_integral_sphere_volume (f : 𝓢(Space 3, ℝ)) :
    sphericalCylinderDist f =
    ∫ x, f (sphericalCylinder x)
      ∂((MeasureTheory.Measure.toSphere volume).prod (volume (α := ℝ))) := byf:𝓢(Space, ℝ)⊢ sphericalCylinderDist f = ∫ (x : ↑(Metric.sphere 0 1) × ℝ), f (sphericalCylinder x) ∂volume.toSphere.prod volume
  rw [sphericalCylinderDist_apply_eq_integral_sphericalCylinderMeasure,f:𝓢(Space, ℝ)⊢ ∫ (x : Space), f x ∂sphericalCylinderMeasure =
  ∫ (x : ↑(Metric.sphere 0 1) × ℝ), f (sphericalCylinder x) ∂volume.toSphere.prod volumeAll goals completed! 🐙 sphericalCylinderMeasure,f:𝓢(Space, ℝ)⊢ ∫ (x : Space), f x ∂Measure.map sphericalCylinder (volume.toSphere.prod volume) =
  ∫ (x : ↑(Metric.sphere 0 1) × ℝ), f (sphericalCylinder x) ∂volume.toSphere.prod volumeAll goals completed! 🐙
    MeasurableEmbedding.integral_map sphericalCylinder_measurableEmbeddingf:𝓢(Space, ℝ)⊢ ∫ (x : ↑(Metric.sphere 0 1) × ℝ), f (sphericalCylinder x) ∂volume.toSphere.prod volume =
  ∫ (x : ↑(Metric.sphere 0 1) × ℝ), f (sphericalCylinder x) ∂volume.toSphere.prod volumeAll goals completed! 🐙]All goals completed! 🐙

Spherical cylinder surface in Space 3

A. The definition of the spherical cylinder surface

B. The measure associated with the spherical cylinder

C. The distribution associated with the spherical cylinder

Spherical cylinder surface in `Space 3`