Documentation

Lean 4 Proof

theorem eff_welfare_at_full_margin {sigma_prev delta beta_n : ℝ} :
    effectiveWelfareContribution sigma_prev delta beta_n 1 =
    welfareContribution sigma_prev delta beta_n := by
  simp only [effectiveWelfareContribution, welfareContribution, mul_one]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:155

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file