Documentation

Lean 4 Proof

theorem margin_strict_in_Tstar {T Tstar1 Tstar2 : ℝ}
    (hTs1 : 0 < Tstar1) (hTs2 : 0 < Tstar2)
    (h : Tstar1 < Tstar2) (hT : 0 < T)
    (hTlt : T < Tstar1) :
    institutionalMargin T Tstar1 < institutionalMargin T Tstar2 := by
  simp only [institutionalMargin]
  -- Both margins are positive (T < T*₁ < T*₂)
  have hm1 : 0 < 1 - T / Tstar1 := by
    rw [sub_pos, div_lt_one hTs1]; exact hTlt
  have hm2 : 0 < 1 - T / Tstar2 := by
    rw [sub_pos, div_lt_one hTs2]; linarith
  rw [max_eq_right (le_of_lt hm1), max_eq_right (le_of_lt hm2)]
  -- Goal: 1 - T / Tstar1 < 1 - T / Tstar2
  -- Suffices: T / Tstar2 < T / Tstar1
  suffices T / Tstar2 < T / Tstar1 by linarith
  rw [div_lt_div_iff₀ hTs2 hTs1]
  exact mul_lt_mul_of_pos_left h hT

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:239

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file