pith. machine review for the scientific record. sign in
theorem proved term proof

G_ratio_mono

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 109theorem G_ratio_mono (r : ℝ) (hr : 0 < r) (R1 R2 : ℝ)
 110    (hR1 : 0 < R1) (hR12 : R1 ≤ R2) :
 111    G_ratio r R1 ≤ G_ratio r R2 := by

proof body

Term-mode proof.

 112  unfold G_ratio
 113  have hab : 0 < abs beta_running := abs_beta_running_pos
 114  have hbeta_neg : beta_running < 0 := beta_running_neg
 115  suffices h : (r / R1) ^ beta_running ≤ (r / R2) ^ beta_running by
 116    linarith [mul_le_mul_of_nonneg_left h (le_of_lt hab)]
 117  apply Real.rpow_le_rpow_of_exponent_le
 118  · exact le_of_lt (div_pos hr hR1)
 119  · exact div_le_div_of_nonneg_left hr hR1 hR12
 120  · exact le_of_lt hbeta_neg
 121
 122/-- For any target M, there exists R > r with G_ratio(r, R) > M.
 123    G_ratio grows without bound as r_ref increases. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.