Documentation

Lean 4 Proof

theorem compositeMP_decreasing_phi {FG₁ FG₂ QE₁ QE₂ FR₀ S S_crit α_FR w_FG w_QE w_FR : ℝ}
    (hwFG : 0 ≤ w_FG) (hwQE : 0 ≤ w_QE)
    (hFG : FG₂ ≤ FG₁) (hQE : QE₂ ≤ QE₁) :
    compositeMP FG₂ QE₂ FR₀ S S_crit α_FR w_FG w_QE w_FR ≤
    compositeMP FG₁ QE₁ FR₀ S S_crit α_FR w_FG w_QE w_FR := by
  unfold compositeMP
  linarith [mul_le_mul_of_nonneg_left hFG hwFG, mul_le_mul_of_nonneg_left hQE hwQE]

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:529

Module Section

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

In the same file