Documentation

Lean 4 Proof

theorem fr_zero_above_critical {FR₀ S S_crit α_FR : ℝ}
    (hS_crit : 0 < S_crit) (hα : α_FR ≠ 0) (hS : S_crit ≤ S) :
    financialRepression FR₀ S S_crit α_FR = 0 := by
  unfold financialRepression
  have h1 : 1 ≤ S / S_crit := le_div_iff₀ hS_crit |>.mpr (by linarith)
  simp [min_eq_left h1, Real.zero_rpow hα, mul_zero]

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:365

Module Section

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

In the same file