unitSphereSurface_D2

formal source

  88  ring
  89
  90/-- For D = 2, the "unit sphere" is a circle with circumference 2π. -/
  91theorem unitSphereSurface_D2 : unitSphereSurface 2 = 2 * Real.pi := by
  92  unfold unitSphereSurface
  93  -- Γ(1) = 1, π^1 = π
  94  -- 2 * π^1 / 1 = 2π
  95  have h : ((2 : ℝ) / 2) = (1 : ℝ) := by norm_num
  96  -- `simp` knows Γ(1)=1 and π^1=π for `Real.rpow`.
  97  simp [h, Real.Gamma_one, Real.rpow_one]
  98
  99/-! ## Part 2: Uniqueness of Isotropic Measure -/
 100
 101/-- **Uniqueness Theorem**: For any dimension D, the uniform measure on S^{D-1}
 102    is unique up to scaling.
 103
 104    This is a consequence of the uniqueness of Haar measure on compact groups:
 105    SO(D) acts transitively on S^{D-1}, so any SO(D)-invariant measure is
 106    proportional to the uniform surface measure. -/
 107theorem isotropic_measure_unique_principle :
 108    ∀ D : ℕ, D ≥ 1 →
 109    ∃! (surface_area : ℝ), surface_area = unitSphereSurface D := by
 110  intro D _
 111  exact ⟨unitSphereSurface D, rfl, fun _ h => h⟩
 112
 113/-! ## Part 3: Why 4π Specifically -/
 114
 115/-- The solid angle is defined as 4π in D=3. -/
 116noncomputable def solidAngle : ℝ := 4 * Real.pi
 117
 118/-- The solid angle equals the sphere surface area. -/
 119theorem solidAngle_is_sphere_area : solidAngle = unitSphereSurface 3 := by
 120  unfold solidAngle
 121  rw [unitSphereSurface_D3]