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

phi_energy_rung_pos

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)

  77lemma phi_energy_rung_pos (n : ℝ) : 0 < phi_energy_rung n :=

proof body

Term-mode proof.

  78  mul_pos E_base_pos (Real.rpow_pos_of_pos phi_pos n)
  79
  80/-- Adjacent rungs scale by φ. -/

depends on (3)

Lean names referenced from this declaration's body.