Documentation

Lean 4 Proof

theorem threshold_decreasing {delta_S gamma1 gamma2 s : ℝ}
    (hd : 0 < delta_S) (hg1 : 0 < gamma1) (_hg2 : 0 < gamma2)
    (hs : 0 < s) (hg : gamma1 < gamma2) :
    dollarizationThreshold delta_S gamma2 s <
    dollarizationThreshold delta_S gamma1 s := by
  unfold dollarizationThreshold
  apply div_lt_div_of_pos_left hd (mul_pos hg1 hs)
    (mul_lt_mul_of_pos_right hg hs)

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:311

Module Section

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

In the same file