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

volume_dominates_surface

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)

 112theorem volume_dominates_surface (coeff : BindingCoefficients) (A : ℕ) (hA : 8 ≤ A) :
 113    coeff.a_V * A > coeff.a_S * (A : ℝ) ^ ((2:ℝ)/3) := by

proof body

Tactic-mode proof.

 114  have hA_pos : (0 : ℝ) < A := by exact_mod_cast Nat.pos_of_ne_zero (by omega)
 115  nlinarith [coeff.h_V_pos, coeff.h_S_pos, hA_pos,
 116             show (A : ℝ) ^ ((2:ℝ)/3) ≤ A from by
 117               exact Real.rpow_le_self_of_one_le_of_le_one_right (by linarith) (by norm_num)]
 118
 119/-! ## Certificate -/
 120

depends on (6)

Lean names referenced from this declaration's body.