Documentation

Lean 4 Proof

theorem standardization_slows {beta_S I_Q rho_1 rho_2 rho_max : ℝ}
    (hbeta : 0 < beta_S) (hI : 0 < I_Q)
    (h12 : rho_1 < rho_2) (_h2 : rho_2 < rho_max) :
    standardizationRate beta_S I_Q rho_2 rho_max <
    standardizationRate beta_S I_Q rho_1 rho_max := by
  simp only [standardizationRate]
  apply mul_lt_mul_of_pos_left _ (mul_pos hbeta hI)
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:67

Module Section

Results 70-79: Endogenous Complementarity Evolution

In the same file