Documentation

Lean 4 Proof

theorem standardizationRate_pos {β_S I_over_Q ρ ρ_max : ℝ}
    (hβ : 0 < β_S) (hI : 0 < I_over_Q) (hρ : ρ < ρ_max) :
    0 < standardizationRate β_S I_over_Q ρ ρ_max := by
  simp only [standardizationRate]
  exact mul_pos (mul_pos hβ hI) (by linarith)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/Defs.lean:187

Module Section

Core definitions for the Lean formalization of Paper 3:

In the same file