77theorem G_ratio_at_self (r : ℝ) (hr : 0 < r) : 78 G_ratio r r = 1 + abs beta_running := by
proof body
Term-mode proof.
79 unfold G_ratio 80 rw [div_self (ne_of_gt hr), Real.one_rpow] 81 ring 82 83/-- G_ratio at r_ref = r is less than 2 (and hence far below 31). 84 Since |β| < 0.06 < 1, we have 1 + |β| < 2. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.