Documentation

Lean 4 Proof

theorem inst_adjustment_decreasing_margin {eps sigma m1 m2 : ℝ}
    (heps : 0 < eps) (hsigma : 0 < sigma) (hm1 : 0 < m1) (_hm2 : 0 < m2)
    (hm : m1 < m2) :
    institutionalAdjustmentTime eps sigma m2 <
    institutionalAdjustmentTime eps sigma m1 := by
  simp only [institutionalAdjustmentTime]
  exact div_lt_div_of_pos_left heps (mul_pos hsigma hm1)
    (mul_lt_mul_of_pos_left hm hsigma)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:125

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file