Documentation

Lean 4 Proof

theorem eff_welfare_nonneg {sigma_prev delta beta_n margin : ℝ}
    (hs : 0 ≤ sigma_prev) (hb : 0 < beta_n) (hm : 0 < margin) :
    0 ≤ effectiveWelfareContribution sigma_prev delta beta_n margin := by
  simp only [effectiveWelfareContribution]
  apply div_nonneg
  · exact mul_nonneg hs (sq_nonneg _)
  · exact le_of_lt (mul_pos hb hm)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:182

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file