Documentation

Lean 4 Proof

theorem eff_welfare_decreasing_margin {sigma_prev delta beta_n m1 m2 : ℝ}
    (hs : 0 < sigma_prev) (hd : delta ≠ 0) (hb : 0 < beta_n)
    (hm1 : 0 < m1) (_hm2 : 0 < m2) (hm : m1 < m2) :
    effectiveWelfareContribution sigma_prev delta beta_n m2 <
    effectiveWelfareContribution sigma_prev delta beta_n m1 := by
  simp only [effectiveWelfareContribution]
  apply div_lt_div_of_pos_left
  · exact mul_pos hs (sq_pos_of_ne_zero hd)
  · exact mul_pos hb hm1
  · exact mul_lt_mul_of_pos_left hm hb

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:170

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file