Documentation

Lean 4 Proof

theorem commitmentGain_positive {sigma_prev delta beta_old beta_new : ℝ}
    (hs : 0 < sigma_prev) (hdelta : delta ≠ 0)
    (hb1 : 0 < beta_old) (hb2 : 0 < beta_new) (h12 : beta_old < beta_new) :
    0 < commitmentGain sigma_prev delta beta_old beta_new := by
  simp only [commitmentGain]
  linarith [upstream_reform_beta hs hdelta hb1 hb2 h12]

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/TimeInconsistency.lean:76

Module Section

Time Inconsistency Resolution via Upstream Reform (Gap 11)

In the same file