Documentation

Lean 4 Proof

theorem phillips_flat_discretion {phi_prev sigma_n c_n : ℝ}
    (hsigma : sigma_n ≠ 0) :
    c_n * (phi_prev / sigma_n) * sigma_n = c_n * phi_prev :=
  damping_cancellation_algebraic hsigma

Dependency Graph

Location

thesis/CESProofs/Applications/TimeInconsistency.lean:178

Module Section

Time Inconsistency Resolution via Upstream Reform (Gap 11)

In the same file