Documentation

Lean 4 Proof

theorem policy_bias_positive {c phi_prev sigma_old sigma_new sigma_prev delta
    beta_old beta_new : ℝ}
    (hs_old : sigma_old ≠ 0) (hs_new : sigma_new ≠ 0)
    (hs_prev : 0 < sigma_prev) (hdelta : delta ≠ 0)
    (hb1 : 0 < beta_old) (hb2 : 0 < beta_new) (h12 : beta_old < beta_new) :
    0 < policyBias c phi_prev sigma_old sigma_new sigma_prev delta beta_old beta_new := by
  simp only [policyBias]
  have hd := discretionary_gain_zero hs_old hs_new
    (c := c) (phi_prev := phi_prev) (delta := delta)
  have hc := commitment_gain_positive hs_prev hdelta hb1 hb2 h12
    (sigma_prev := sigma_prev)
  linarith

Dependency Graph

Location

thesis/CESProofs/Applications/TimeInconsistency.lean:91

Module Section

Time Inconsistency Resolution via Upstream Reform (Gap 11)

In the same file