Documentation

Lean 4 Proof

theorem mp_effectiveness_decreasing {phi1 phi2 f1 f2 : ℝ}
    (_hphi1 : 0 ≤ phi1) (_hphi2 : phi2 ≤ 1)
    (hphi : phi1 < phi2) (hf_pos : 0 < f1) (hf : f2 ≤ f1) :
    (1 - phi2) * f2 ≤ (1 - phi1) * f1 := by
  have h1 : 1 - phi2 ≤ 1 - phi1 := by linarith
  calc (1 - phi2) * f2
      ≤ (1 - phi2) * f1 := by nlinarith
    _ ≤ (1 - phi1) * f1 := by nlinarith

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:262

Module Section

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

In the same file