vrot_flat_of_linear_Menc

formal source

  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) :
  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