Documentation

Lean 4 Proof

theorem discretion_robust_to_drift {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:150

Module Section

Time Inconsistency Resolution via Upstream Reform (Gap 11)

In the same file