Institutional Adjustment Time Pos

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem institutionalAdjustmentTime_pos {eps sigma margin : ℝ}
    (heps : 0 < eps) (hsigma : 0 < sigma) (hm : 0 < margin) :
    0 < institutionalAdjustmentTime eps sigma margin :=
  div_pos heps (mul_pos hsigma hm)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:115

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file

reform_scaling_sigma reform_scaling_beta reform_substitutability institutionalMargin institutionalMargin_nonneg institutionalMargin_at_zero institutionalMargin_at_critical institutionalAdjustmentTime adjustment_timescale_connection adjustmentTimescale_connection inst_adjustment_decreasing_margin effectiveWelfareContribution eff_welfare_at_full_margin eff_welfare_decreasing_margin eff_welfare_nonneg fragility_at_critical margin_monotone_in_Tstar margin_strict_in_Tstar