unitSphereSurface_D3

formal source

  48  2 * Real.pi ^ ((D : ℝ) / 2) / Real.Gamma ((D : ℝ) / 2)
  49
  50/-- For D = 3, the unit sphere surface area is 4π. -/
  51theorem unitSphereSurface_D3 : unitSphereSurface 3 = 4 * Real.pi := by
  52  unfold unitSphereSurface
  53  -- Γ(3/2) = (1/2)·Γ(1/2) = √π/2
  54  have hGamma : Real.Gamma ((3 : ℝ) / 2) = (Real.sqrt Real.pi) / 2 := by
  55    -- Use Γ(s+1) = s·Γ(s) with s = 1/2.
  56    have : Real.Gamma ((1 / 2 : ℝ) + 1) = (1 / 2 : ℝ) * Real.Gamma (1 / 2 : ℝ) := by
  57      simpa using (Real.Gamma_add_one (s := (1 / 2 : ℝ)) (by norm_num))
  58    -- Rewrite (1/2)+1 = 3/2 and Γ(1/2) = √π.
  59    simpa [Real.Gamma_one_half_eq, add_comm, add_left_comm, add_assoc, div_eq_mul_inv] using this
  60
  61  -- Simplify π^(3/2) = π^(1 + 1/2) = π * π^(1/2) = π * √π.
  62  have hPiPow : Real.pi ^ ((3 : ℝ) / 2) = Real.pi * Real.sqrt Real.pi := by
  63    have hpi_pos : (0 : ℝ) < Real.pi := Real.pi_pos
  64    -- 3/2 = 1 + 1/2
  65    have : (Real.pi : ℝ) ^ ((3 : ℝ) / 2) = Real.pi ^ ((1 : ℝ) + (1 / 2 : ℝ)) := by
  66      norm_num
  67    -- Expand with rpow_add.
  68    calc
  69      Real.pi ^ ((3 : ℝ) / 2)
  70          = Real.pi ^ ((1 : ℝ) + (1 / 2 : ℝ)) := this
  71      _ = Real.pi ^ (1 : ℝ) * Real.pi ^ (1 / 2 : ℝ) := by
  72            simpa [add_comm, add_left_comm, add_assoc] using (Real.rpow_add hpi_pos (1 : ℝ) (1 / 2 : ℝ))
  73      _ = Real.pi * Real.sqrt Real.pi := by
  74            -- π^1 = π, and √π = π^(1/2) (via `sqrt_eq_rpow`).
  75            simp [Real.rpow_one, Real.sqrt_eq_rpow]
  76
  77  -- Now compute the surface area.
  78  -- 2 * π^(3/2) / (√π/2) = 4π
  79  -- First normalize the coercion: (↑3 / 2) = (3 / 2 : ℝ)
  80  have hcoerce : ((3 : ℕ) : ℝ) / 2 = (3 / 2 : ℝ) := by norm_num
  81  simp only [hcoerce] at *