vrot_sq

formal source

  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) :
  39  ∀ {r : ℝ}, 0 < r → vrot S r = Real.sqrt (S.G * α) := by
  40  intro r hr
  41  have hM : S.Menc r = α * r := hlin hr
  42  have hrne : r ≠ 0 := ne_of_gt hr
  43  have hfrac : S.G * S.Menc r / r = S.G * α := by
  44    calc
  45      S.G * S.Menc r / r = S.G * (α * r) / r := by rw [hM]
  46      _ = S.G * α * r / r := by ring
  47      _ = S.G * α := by field_simp [hrne]
  48  dsimp [vrot]
  49  rw [hfrac]
  50
  51/-- Under linear mass growth `Menc(r) = α r`, the centripetal acceleration scales as `g(r) = (G α)/r`. -/
  52lemma g_of_linear_Menc (S : RotSys) (α : ℝ)
  53  (hlin : ∀ {r : ℝ}, 0 < r → S.Menc r = α * r) :