Documentation

Lean 4 Proof

theorem friction_monotone (e : SettlementEconomy) {lambda_1 lambda_2 : ℝ}
    (_h1 : 0 < lambda_1) (_h2 : 0 < lambda_2) (hle : lambda_1 ≤ lambda_2) :
    settlementR0Friction e lambda_1 ≤ settlementR0Friction e lambda_2 := by
  simp only [settlementR0Friction]
  apply div_le_div_of_nonneg_right _ (le_of_lt (mul_pos e.h_self_phi e.h_self_S))
  apply mul_le_mul_of_nonneg_left
  · exact mul_le_mul_of_nonneg_right hle (le_of_lt e.h_cross_S_phi)
  · exact le_of_lt e.h_cross_phi_S

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:161

Module Section

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

In the same file