Documentation

Lean 4 Proof

theorem discretion_zero_cost_of_appearing {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 :=
  discretionary_gain_zero hs1 hs2

Dependency Graph

Location

thesis/CESProofs/Applications/TimeInconsistency.lean:111

Module Section

Time Inconsistency Resolution via Upstream Reform (Gap 11)

In the same file