Documentation

Lean 4 Proof

theorem discretionary_gain_zero {c phi_prev sigma_old sigma_new delta : ℝ}
    (hs1 : sigma_old ≠ 0) (hs2 : sigma_new ≠ 0) :
    discretionaryGain c phi_prev sigma_old sigma_new delta = 0 := by
  simp only [discretionaryGain]
  have h1 := welfare_independent_of_own_sigma (phi_prev := phi_prev) (c := c)
    (delta := delta) hs2 hs1
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/TimeInconsistency.lean:61

Module Section

Time Inconsistency Resolution via Upstream Reform (Gap 11)

In the same file