Documentation

Lean 4 Proof

theorem threshold_ratio_invariant {delta gamma s1 s2 : ℝ}
    (_hg : 0 < gamma) (hs1 : 0 < s1) (hs2 : 0 < s2)
    (hdelta : 0 < delta) :
    dollarizationThreshold delta gamma s1 /
    dollarizationThreshold delta gamma s2 = s2 / s1 := by
  unfold dollarizationThreshold
  have hd : delta ≠ 0 := ne_of_gt hdelta
  field_simp

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:322

Module Section

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

In the same file