Commitment Gain

Documentation

Lean 4 Proof

def commitmentGain (sigma_prev delta beta_old beta_new : ℝ) : ℝ :=
  welfareContribution sigma_prev delta beta_old -
  welfareContribution sigma_prev delta beta_new

Dependency Graph

Used by

commitment_robust_to_drift commitment_dominates_discretion commitmentGain_positive policyBias commitment_gain_positive

Location

thesis/CESProofs/Applications/TimeInconsistency.lean:43

Module Section

Time Inconsistency Resolution via Upstream Reform (Gap 11)

In the same file

discretionaryGain policyBias discretionary_gain_zero commitment_gain_positive commitmentGain_positive policyBias_positive policy_bias_positive discretion_zero_cost_of_appearing commitment_resolves_inconsistency rho_drift_shifts_Tstar discretion_robust_to_drift commitment_robust_to_drift phillips_flat_discretion commitment_dominates_discretion