Documentation

Lean 4 Proof

theorem composite_mp_decreasing_S {FG QE FR₀ S₁ S₂ S_crit α_FR w_FG w_QE w_FR : ℝ}
    (hw : 0 ≤ w_FR) (hFR₀ : 0 ≤ FR₀) (hα : 0 < α_FR) (hSc : 0 < S_crit)
    (hS₁ : 0 ≤ S₁) (hS₂ : 0 ≤ S₂) (hS : S₁ ≤ S₂) :
    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 (fr_decreasing hFR₀ hα hSc hS₁ hS₂ hS) hw]

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:517

Module Section

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

In the same file