Documentation

Lean 4 Proof

theorem fr_continuous {FR₀ S_crit α_FR : ℝ}
    (_hSc : 0 < S_crit) (hα : 0 < α_FR) :
    Continuous (fun S => financialRepression FR₀ S S_crit α_FR) := by
  unfold financialRepression
  apply Continuous.mul continuous_const
  apply Continuous.rpow _ continuous_const (fun x => Or.inr hα)
  exact continuous_const.sub (continuous_min_div S_crit)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:417

Module Section

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

In the same file