Documentation

Lean 4 Proof

theorem reform_scaling_beta {sigma_prev delta beta_n lambda : ℝ}
    (hl : lambda ≠ 0) (hb : beta_n ≠ 0) :
    welfareContribution sigma_prev delta (lambda * beta_n) =
    (1 / lambda) * welfareContribution sigma_prev delta beta_n := by
  simp only [welfareContribution]
  field_simp

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:49

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file