Documentation

Lean 4 Proof

theorem safety_zone_shrinking {c_0 phi1 phi2 : ℝ}
    (hc : 0 < c_0) (hphi : phi1 < phi2) :
    (1 - phi2) * c_0 < (1 - phi1) * c_0 := by
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:275

Module Section

Paper 7: Settlement Feedback and Monetary Policy in a Mesh Economy

In the same file