lemma
proved
tactic proof
vrot_flat_of_linear_Menc
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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`. -/