Institutional Margin At Critical

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem institutionalMargin_at_critical {Tstar : ℝ} (hTs : 0 < Tstar) :
    institutionalMargin Tstar Tstar = 0 := by
  simp [institutionalMargin, div_self (ne_of_gt hTs)]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:89

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 institutionalAdjustmentTime adjustmentTimescale_connection adjustment_timescale_connection institutionalAdjustmentTime_pos 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