RotSys

formal source

   5namespace Rotation
   6
   7/-- Rotation system with gravitational constant G and enclosed mass function `Menc`. -/
   8structure RotSys where
   9  G : ℝ
  10  posG : 0 < G
  11  Menc : ℝ → ℝ
  12  nonnegM : ∀ r, 0 ≤ Menc r
  13
  14/-- Rotation velocity as a function of radius. -/
  15noncomputable def vrot (S : RotSys) (r : ℝ) : ℝ :=
  16  Real.sqrt (S.G * S.Menc r / r)
  17
  18/-- Centripetal acceleration as a function of radius. -/
  19noncomputable def g (S : RotSys) (r : ℝ) : ℝ :=
  20  (vrot S r) ^ 2 / r
  21
  22/-- Algebraic identity: `vrot^2 = G Menc / r` for `r > 0`. -/
  23lemma vrot_sq (S : RotSys) {r : ℝ} (hr : 0 < r) :
  24  (vrot S r) ^ 2 = S.G * S.Menc r / r := by
  25  dsimp [vrot]
  26  have hnum_nonneg : 0 ≤ S.G * S.Menc r := by
  27    have hM : 0 ≤ S.Menc r := S.nonnegM r
  28    exact mul_nonneg (le_of_lt S.posG) hM
  29  have hfrac_nonneg : 0 ≤ S.G * S.Menc r / r := by
  30    exact div_nonneg hnum_nonneg (le_of_lt hr)
  31  calc
  32    (Real.sqrt (S.G * S.Menc r / r)) ^ 2 = S.G * S.Menc r / r := by
  33      rw [Real.sq_sqrt hfrac_nonneg]
  34
  35/-- If the enclosed mass grows linearly, `Menc(r) = α r` with `α ≥ 0`, then the rotation curve is flat:
  36    `vrot(r) = √(G α)` for all `r > 0`. -/
  37lemma vrot_flat_of_linear_Menc (S : RotSys) (α : ℝ)
  38  (hlin : ∀ {r : ℝ}, 0 < r → S.Menc r = α * r) :