Documentation

Lean 4 Proof

theorem margin_monotone_in_Tstar {T Tstar1 Tstar2 : ℝ}
    (hTs1 : 0 < Tstar1) (hTs2 : 0 < Tstar2) (h : Tstar1 ≤ Tstar2) (hT : 0 ≤ T) :
    institutionalMargin T Tstar1 ≤ institutionalMargin T Tstar2 := by
  simp only [institutionalMargin]
  apply max_le_max_left 0
  -- Goal: 1 - T / Tstar1 ≤ 1 - T / Tstar2
  -- Suffices: T / Tstar2 ≤ T / Tstar1
  suffices T / Tstar2 ≤ T / Tstar1 by linarith
  rw [div_le_div_iff₀ hTs2 hTs1]
  exact mul_le_mul_of_nonneg_left h hT

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:226

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file