Effective Welfare Contribution

def proved Hierarchy

Documentation

Lean 4 Proof

def effectiveWelfareContribution (sigma_prev delta beta_n margin : ℝ) : ℝ :=
  sigma_prev * delta ^ 2 / (beta_n * margin)

Dependency Graph

Used by

eff_welfare_nonneg eff_welfare_decreasing_margin policy_dichotomy variance_targeting_improves variance_upstream_complement variance_target_bounds_welfare eff_welfare_at_full_margin

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:149

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file

reform_scaling_sigma reform_scaling_beta reform_substitutability institutionalMargin institutionalMargin_nonneg institutionalMargin_at_zero institutionalMargin_at_critical institutionalAdjustmentTime adjustment_timescale_connection adjustmentTimescale_connection institutionalAdjustmentTime_pos inst_adjustment_decreasing_margin eff_welfare_at_full_margin eff_welfare_decreasing_margin eff_welfare_nonneg fragility_at_critical margin_monotone_in_Tstar margin_strict_in_Tstar