PhyslibAlpha.SpaceAndTime.Space.Surfaces.Line

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

Line surfaces in `Space d`

@[expose] public section

A. The definition of the line surface

The coordinate line embedded in Space d.

def line (d : ℕ) [NeZero d] : ℝ → Space d := fun r =>
  r • basis (0 : Fin d)

              lemma line_eq_smul_basis (d : ℕ) [NeZero d] :
    line d = fun r => r • basis (0 : Fin d) := rfllemma line_injective (d : ℕ) [NeZero d] : Function.Injective (line d) := byd:ℕinst✝:NeZero d⊢ Function.Injective (line d)
  intro x y hd:ℕinst✝:NeZero dx:ℝy:ℝh:line d x = line d y⊢ x = y
  have h0 := congrArg (fun p : Space d => p (0 : Fin d)) hd:ℕinst✝:NeZero dx:ℝy:ℝh:line d x = line d yh0:(line d x).val 0 = (line d y).val 0⊢ x = y
  simpa [line] using h0All goals completed! 🐙

@[fun_prop]
lemma line_continuous (d : ℕ) [NeZero d] : Continuous (line d) := byd:ℕinst✝:NeZero d⊢ Continuous (line d)
  rw [line_eq_smul_basisd:ℕinst✝:NeZero d⊢ Continuous fun r => r • basis 0d:ℕinst✝:NeZero d⊢ Continuous fun r => r • basis 0]d:ℕinst✝:NeZero d⊢ Continuous fun r => r • basis 0
  fun_propAll goals completed! 🐙lemma line_measurableEmbedding (d : ℕ) [NeZero d] : MeasurableEmbedding (line d) :=
  Continuous.measurableEmbedding (line_continuous d) (line_injective d)

@[simp]
lemma norm_line (d : ℕ) [NeZero d] (r : ℝ) : ‖line d r‖ = ‖r‖ := byd:ℕinst✝:NeZero dr:ℝ⊢ ‖line d r‖ = ‖r‖
  rw [line,d:ℕinst✝:NeZero dr:ℝ⊢ ‖r • basis 0‖ = ‖r‖d:ℕinst✝:NeZero dr:ℝ⊢ ‖r‖ * ‖basis 0‖ = ‖r‖ norm_smuld:ℕinst✝:NeZero dr:ℝ⊢ ‖r‖ * ‖basis 0‖ = ‖r‖d:ℕinst✝:NeZero dr:ℝ⊢ ‖r‖ * ‖basis 0‖ = ‖r‖]d:ℕinst✝:NeZero dr:ℝ⊢ ‖r‖ * ‖basis 0‖ = ‖r‖
  simpAll goals completed! 🐙

B. The measure associated with the line

The measure on Space d corresponding to integration along a coordinate line.

def lineMeasure (d : ℕ) [NeZero d] : Measure (Space d) :=
  MeasureTheory.Measure.map (line d) volume



instance lineMeasure_hasTemperateGrowth (d : ℕ) [NeZero d] :
    (lineMeasure d).HasTemperateGrowth := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero d⊢ (lineMeasure d).HasTemperateGrowth
  rw [lineMeasure𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero d⊢ (Measure.map (line d) volume).HasTemperateGrowth𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero d⊢ (Measure.map (line d) volume).HasTemperateGrowth]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero d⊢ (Measure.map (line d) volume).HasTemperateGrowth
  refine { exists_integrable := ?_ }𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero d⊢ ∃ n, Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) (Measure.map (line d) volume)
  obtain ⟨r, hr⟩ := Measure.HasTemperateGrowth.exists_integrable (μ := volume (α := ℝ))𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ ∃ n, Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) (Measure.map (line d) volume)
  use rh𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) (Measure.map (line d) volume)
  rw [MeasurableEmbedding.integrable_map_iffh𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ Integrable ((fun x => (1 + ‖x‖) ^ (-↑r)) ∘ line d) volumeh.hf𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ MeasurableEmbedding (line d)h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ Integrable ((fun x => (1 + ‖x‖) ^ (-↑r)) ∘ line d) volumeh.hf𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ MeasurableEmbedding (line d)]h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ Integrable ((fun x => (1 + ‖x‖) ^ (-↑r)) ∘ line d) volumeh.hf𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ MeasurableEmbedding (line d)
  ·h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ Integrable ((fun x => (1 + ‖x‖) ^ (-↑r)) ∘ line d) volume convert hr using 1𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ (fun x => (1 + ‖x‖) ^ (-↑r)) ∘ line d = fun x => (1 + ‖x‖) ^ (-↑r)
    ext x𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volumex:ℝ⊢ ((fun x => (1 + ‖x‖) ^ (-↑r)) ∘ line d) x = (1 + ‖x‖) ^ (-↑r)
    simp [norm_line]All goals completed! 🐙
  ·h.hf𝕜:TypeE:TypeF:TypeF':Typeinst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedAddCommGroup Finst✝³:NormedAddCommGroup F'inst✝²:NormedSpace ℝ Einst✝¹:NormedSpace ℝ Fd:ℕinst✝:NeZero dr:ℕhr:Integrable (fun x => (1 + ‖x‖) ^ (-↑r)) volume⊢ MeasurableEmbedding (line d) exact line_measurableEmbedding dAll goals completed! 🐙

C. The distribution associated with the line

The distribution on Space d corresponding to integration along a coordinate line. One can roughly think of this distribution as taking a test function f to its integral against a mass, charge or current density concentrated on a line.

def lineDist (d : ℕ) [NeZero d] : (Space d) →d[ℝ] ℝ :=
  SchwartzMap.integralCLM ℝ (lineMeasure d)



lemma lineDist_apply_eq_integral_lineMeasure (d : ℕ) [NeZero d] (f : 𝓢(Space d, ℝ)) :
    lineDist d f = ∫ x, f x ∂lineMeasure d := byd:ℕinst✝:NeZero df:𝓢(Space d, ℝ)⊢ (lineDist d) f = ∫ (x : Space d), f x ∂lineMeasure d
  rw [lineDist,d:ℕinst✝:NeZero df:𝓢(Space d, ℝ)⊢ (integralCLM ℝ (lineMeasure d)) f = ∫ (x : Space d), f x ∂lineMeasure dAll goals completed! 🐙 SchwartzMap.integralCLM_applyd:ℕinst✝:NeZero df:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), f x ∂lineMeasure d = ∫ (x : Space d), f x ∂lineMeasure dAll goals completed! 🐙]All goals completed! 🐙



lemma lineDist_apply_eq_integral_volume (d : ℕ) [NeZero d] (f : 𝓢(Space d, ℝ)) :
    lineDist d f = ∫ r : ℝ, f (line d r) := byd:ℕinst✝:NeZero df:𝓢(Space d, ℝ)⊢ (lineDist d) f = ∫ (r : ℝ), f (line d r)
  rw [lineDist_apply_eq_integral_lineMeasure,d:ℕinst✝:NeZero df:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), f x ∂lineMeasure d = ∫ (r : ℝ), f (line d r)All goals completed! 🐙 lineMeasure,d:ℕinst✝:NeZero df:𝓢(Space d, ℝ)⊢ ∫ (x : Space d), f x ∂Measure.map (line d) volume = ∫ (r : ℝ), f (line d r)All goals completed! 🐙
    MeasurableEmbedding.integral_map (line_measurableEmbedding d)d:ℕinst✝:NeZero df:𝓢(Space d, ℝ)⊢ ∫ (x : ℝ), f (line d x) ∂volume = ∫ (r : ℝ), f (line d r)All goals completed! 🐙]All goals completed! 🐙

D. The line has ambient volume zero

The linear subspace spanned by the coordinate line in Space d.

def lineSubmodule (d : ℕ) [NeZero d] : Submodule ℝ (Space d) :=
  ℝ ∙ basis (0 : Fin d)

              

lemma line_mem_lineSubmodule (d : ℕ) [NeZero d] (r : ℝ) : line d r ∈ lineSubmodule d := byd:ℕinst✝:NeZero dr:ℝ⊢ line d r ∈ lineSubmodule d
  rw [line_eq_smul_basisd:ℕinst✝:NeZero dr:ℝ⊢ (fun r => r • basis 0) r ∈ lineSubmodule dd:ℕinst✝:NeZero dr:ℝ⊢ (fun r => r • basis 0) r ∈ lineSubmodule d]d:ℕinst✝:NeZero dr:ℝ⊢ (fun r => r • basis 0) r ∈ lineSubmodule d
  exact Submodule.smul_mem _ r (Submodule.mem_span_singleton_self (basis (0 : Fin d)))All goals completed! 🐙lemma range_line_subset_lineSubmodule (d : ℕ) [NeZero d] :
    Set.range (line d) ⊆ (lineSubmodule d : Set (Space d)) := byd:ℕinst✝:NeZero d⊢ Set.range (line d) ⊆ ↑(lineSubmodule d)
  rintro x ⟨r, rfl⟩d:ℕinst✝:NeZero dr:ℝ⊢ line d r ∈ ↑(lineSubmodule d)
  exact line_mem_lineSubmodule d rAll goals completed! 🐙

lemma lineSubmodule_ne_top (d : ℕ) [NeZero d] (hd : 2 ≤ d) : lineSubmodule d ≠ ⊤ := byd:ℕinst✝:NeZero dhd:2 ≤ d⊢ lineSubmodule d ≠ ⊤
  intro htopd:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤⊢ False
  have hbasis : basis (1 : Fin d) ∈ lineSubmodule d := byd:ℕinst✝:NeZero dhd:2 ≤ d⊢ lineSubmodule d ≠ ⊤d:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤hbasis:basis 1 ∈ lineSubmodule d⊢ False
    rw [htopd:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤⊢ basis 1 ∈ ⊤d:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤⊢ basis 1 ∈ ⊤d:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤hbasis:basis 1 ∈ lineSubmodule d⊢ False]d:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤⊢ basis 1 ∈ ⊤d:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤hbasis:basis 1 ∈ lineSubmodule d⊢ False
    exact Submodule.mem_topd:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤hbasis:basis 1 ∈ lineSubmodule d⊢ Falsed:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤hbasis:basis 1 ∈ lineSubmodule d⊢ False
  obtain ⟨c, hc⟩ := (Submodule.mem_span_singleton.mp hbasis)d:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤hbasis:basis 1 ∈ lineSubmodule dc:ℝhc:c • basis 0 = basis 1⊢ False
  have hcoord := congrArg (fun p : Space d => p (1 : Fin d)) hcd:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤hbasis:basis 1 ∈ lineSubmodule dc:ℝhc:c • basis 0 = basis 1hcoord:(c • basis 0).val 1 = (basis 1).val 1⊢ False
  have hd1 : d ≠ 1 := byd:ℕinst✝:NeZero dhd:2 ≤ d⊢ lineSubmodule d ≠ ⊤d:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤hbasis:basis 1 ∈ lineSubmodule dc:ℝhc:c • basis 0 = basis 1hcoord:(c • basis 0).val 1 = (basis 1).val 1hd1:d ≠ 1⊢ False omegad:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤hbasis:basis 1 ∈ lineSubmodule dc:ℝhc:c • basis 0 = basis 1hcoord:(c • basis 0).val 1 = (basis 1).val 1hd1:d ≠ 1⊢ Falsed:ℕinst✝:NeZero dhd:2 ≤ dhtop:lineSubmodule d = ⊤hbasis:basis 1 ∈ lineSubmodule dc:ℝhc:c • basis 0 = basis 1hcoord:(c • basis 0).val 1 = (basis 1).val 1hd1:d ≠ 1⊢ False
  simp [basis_apply, hd1] at hcoordAll goals completed! 🐙

lemma volume_line_range (d : ℕ) [NeZero d] (hd : 2 ≤ d) :
    volume (Set.range (line d) : Set (Space d)) = 0 := byd:ℕinst✝:NeZero dhd:2 ≤ d⊢ volume (Set.range (line d)) = 0
  refine measure_mono_null (range_line_subset_lineSubmodule d) ?_d:ℕinst✝:NeZero dhd:2 ≤ d⊢ volume ↑(lineSubmodule d) = 0
  rw [volume_eq_addHaard:ℕinst✝:NeZero dhd:2 ≤ d⊢ basis.toBasis.addHaar ↑(lineSubmodule d) = 0d:ℕinst✝:NeZero dhd:2 ≤ d⊢ basis.toBasis.addHaar ↑(lineSubmodule d) = 0]d:ℕinst✝:NeZero dhd:2 ≤ d⊢ basis.toBasis.addHaar ↑(lineSubmodule d) = 0
  exact MeasureTheory.Measure.addHaar_submodule
    (Space.basis.toBasis.addHaar : Measure (Space d))
    (lineSubmodule d) (lineSubmodule_ne_top d hd)All goals completed! 🐙

Line surfaces in Space d

A. The definition of the line surface

B. The measure associated with the line

C. The distribution associated with the line

D. The line has ambient volume zero

Line surfaces in `Space d`