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

eruption_recurrence_one_statement

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)

 113theorem eruption_recurrence_one_statement :
 114    (2.59 < vei_step_ratio ∧ vei_step_ratio < 2.63) ∧
 115    (∀ k : ℕ, cumulative_ratio k = vei_step_ratio ^ k) ∧
 116    cumulative_ratio 1 = vei_step_ratio :=

proof body

Term-mode proof.

 117  ⟨vei_step_ratio_band, cumulative_ratio_factors, cumulative_ratio_one_step⟩
 118
 119end
 120
 121end EruptionRecurrenceLadder
 122end Geology
 123end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.