Documentation

Lean 4 Proof

lemma fr_below_critical {FR₀ S S_crit α_FR : ℝ}
    (hSc : 0 < S_crit) (_hS_nn : 0 ≤ S) (hS : S < S_crit) :
    financialRepression FR₀ S S_crit α_FR = FR₀ * (1 - S / S_crit) ^ α_FR := by
  unfold financialRepression
  congr 1
  have : S / S_crit < 1 := by rwa [div_lt_one hSc]
  simp [min_eq_right (le_of_lt this)]

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:375

Module Section

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

In the same file