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