Documentation

Lean 4 Proof

theorem cbdc_acceleration (e : SettlementEconomy) {lambda_B : ℝ}
    (_hlambda_pos : 0 < lambda_B) (hlambda_lt : lambda_B < 1) :
    settlementR0Friction e lambda_B < settlementR0 e := by
  rw [settlementR0Friction_eq]
  exact mul_lt_of_lt_one_left (settlementR0_pos e) hlambda_lt

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:153

Module Section

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

In the same file