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.SolidSphere
public import Physlib.SpaceAndTime.Space.Integrals.Basic
public import Mathlib.MeasureTheory.Integral.Prod
Solid cylinder surface in Space 3
The solid cylinder is the closed unit disk in Space 2 extruded along the third coordinate.
It is the solid analogue of the spherical cylinder, in the same way that the solid sphere is the
solid analogue of the spherical shell. Like the solid sphere it is a region of positive ambient
volume, so the measure associated with it is built from the ambient volume of the cross-sectional
disk (the solid-sphere measure in Space 2) extruded along the axis, rather than a pushforward of
a lower-dimensional surface measure. The measure-zero requirement is therefore not applicable here
and is replaced by a statement that the solid cylinder has positive ambient volume.
@[expose] public sectionA. The definition of the solid cylinder surface
The map embedding a cross-sectional disk extruded along the axis into Space 3. The disk is
cut out by the solid-cylinder measure, which is supported on the closed unit disk.
lemma solidCylinder_eq :
solidCylinder = (slice 2).symm ∘ (fun x : Space 2 × ℝ => (x.2, x.1)) := rfllemma solidCylinder_injective : Function.Injective solidCylinder := ⊢ Function.Injective solidCylinder
x:Space 2 × ℝy:Space 2 × ℝh:solidCylinder x = solidCylinder y⊢ x = y
x:Space 2 × ℝy:Space 2 × ℝh:solidCylinder x = solidCylinder yh':(slice 2) (solidCylinder x) = (slice 2) (solidCylinder y)⊢ x = y
x:Space 2 × ℝy:Space 2 × ℝh:solidCylinder x = solidCylinder yh':x.2 = y.2 ∧ x.1 = y.1⊢ x = y
All goals completed! 🐙⊢ Continuous (⇑(slice 2).symm ∘ fun x => (x.2, x.1))
All goals completed! 🐙lemma solidCylinder_measurableEmbedding : MeasurableEmbedding solidCylinder :=
Continuous.measurableEmbedding solidCylinder_continuous solidCylinder_injectiveAll goals completed! 🐙B. The measure associated with the solid cylinder
The measure on Space 3 corresponding to integration over a solid cylinder, i.e. the
pushforward of the product of the solid-sphere (closed unit disk) measure on Space 2 with the
line measure along the axis.
def solidCylinderMeasure : Measure (Space 3) :=
MeasureTheory.Measure.map solidCylinder ((solidSphereMeasure 2).prod (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)) volumex:Space 2 × ℝ⊢ 1 + ‖x.2‖ ≤ 1 + √(‖x.2‖ ^ 2 + ‖x.1‖ ^ 2)
𝕜: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:Space 2 × ℝ⊢ ‖x.2‖ ≤ √(‖x.2‖ ^ 2 + ‖x.1‖ ^ 2)
𝕜: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:Space 2 × ℝ⊢ ‖x.2‖ ^ 2 ≤ ‖x.2‖ ^ 2 + ‖x.1‖ ^ 2
All goals completed! 🐙
𝕜: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:Space 2 × ℝ⊢ -↑n ≤ 0 All goals completed! 🐙𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ SFinite (Measure.map solidCylinder ((solidSphereMeasure 2).prod volume))
All goals completed! 🐙C. The distribution associated with the solid cylinder
The distribution on Space 3 corresponding to integration over a solid cylinder.
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 cylinder.
def solidCylinderDist : (Space 3) →d[ℝ] ℝ :=
SchwartzMap.integralCLM ℝ solidCylinderMeasureAll goals completed! 🐙All goals completed! 🐙D. The solid cylinder has positive ambient volume
⊢ 0 < (solidSphereMeasure 2) Set.univ * volume Set.univ
⊢ volume Set.univ ≠ 0
All goals completed! 🐙