g_of_linear_Menc

formal source

  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) :
  54  ∀ {r : ℝ}, 0 < r → g S r = (S.G * α) / r := by
  55  intro r hr
  56  have hM : S.Menc r = α * r := hlin hr
  57  have hrne : r ≠ 0 := ne_of_gt hr
  58  dsimp [g]
  59  have hvrot_sq : (vrot S r) ^ 2 = S.G * α := by
  60    have hfrac : S.G * S.Menc r / r = S.G * α := by
  61      calc
  62        S.G * S.Menc r / r = S.G * (α * r) / r := by rw [hM]
  63        _ = S.G * α * r / r := by ring
  64        _ = S.G * α := by field_simp [hrne]
  65    dsimp [vrot]
  66    have hnonneg : 0 ≤ S.G * S.Menc r / r := by
  67      have hnum_nonneg : 0 ≤ S.G * S.Menc r := by
  68        have hM : 0 ≤ S.Menc r := S.nonnegM r
  69        exact mul_nonneg (le_of_lt S.posG) hM
  70      exact div_nonneg hnum_nonneg (le_of_lt hr)
  71    calc
  72      Real.sqrt (S.G * S.Menc r / r) ^ 2 = S.G * S.Menc r / r := by
  73        rw [Real.sq_sqrt hnonneg]
  74      _ = S.G * α := by rw [hfrac]
  75  calc
  76    g S r = (vrot S r) ^ 2 / r := by dsimp [g]
  77    _ = (S.G * α) / r := by rw [hvrot_sq]
  78
  79/-- Newtonian rotation curve is flat when the enclosed mass grows linearly:
  80    if `Menc(r) = γ r` (γ ≥ 0) then `vrot(r) = √(G γ)` for all r > 0. -/
  81lemma vrot_flat_of_linear_Menc_Newtonian (S : RotSys) (γ : ℝ)
  82  (hγ : 0 ≤ γ) (hlin : ∀ {r : ℝ}, 0 < r → S.Menc r = γ * r) :