Discretionary Gain

Documentation

Lean 4 Proof

def discretionaryGain (c phi_prev sigma_old sigma_new delta : ℝ) : ℝ :=
  c * (phi_prev / sigma_new) * sigma_new * delta ^ 2 -
  c * (phi_prev / sigma_old) * sigma_old * delta ^ 2

Dependency Graph

Used by

discretionary_gain_zero discretion_robust_to_drift discretion_zero_cost_of_appearing commitment_dominates_discretion policyBias

Location

thesis/CESProofs/Applications/TimeInconsistency.lean:36

Module Section

Time Inconsistency Resolution via Upstream Reform (Gap 11)

In the same file

commitmentGain policyBias discretionary_gain_zero commitmentGain_positive commitment_gain_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