Documentation

Lean 4 Proof

theorem composite_mp_continuous_S {FR₀ S_crit α_FR w_FG w_QE w_FR FG QE : ℝ}
    (hSc : 0 < S_crit) (hα : 0 < α_FR) :
    Continuous (fun S => compositeMP FG QE FR₀ S S_crit α_FR w_FG w_QE w_FR) := by
  unfold compositeMP
  exact continuous_const.add (continuous_const.mul (fr_continuous hSc hα))

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:543

Module Section

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

In the same file