Documentation

Lean 4 Proof

theorem log_linear_standardization_rate {beta_S I_Q rho_0 rho_max : ℝ}
    (hbeta : 0 < beta_S) (hI : 0 < I_Q) (hrho : rho_0 < rho_max) :
    0 < standardizationRate beta_S I_Q rho_0 rho_max :=
  standardizationRate_pos hbeta hI hrho

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:61

Module Section

Results 70-79: Endogenous Complementarity Evolution

In the same file