Documentation

Lean 4 Proof

theorem reform_scaling_sigma {sigma_prev delta beta_n lambda : ℝ} :
    welfareContribution (lambda * sigma_prev) delta beta_n =
    lambda * welfareContribution sigma_prev delta beta_n := by
  simp only [welfareContribution]
  rw [mul_assoc, mul_div_assoc]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:38

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file