Documentation

Lean 4 Proof

theorem fr_nonneg {FR₀ S S_crit α_FR : ℝ}
    (hFR₀ : 0 ≤ FR₀) (hS : 0 ≤ S) (hSc : 0 < S_crit) :
    0 ≤ financialRepression FR₀ S S_crit α_FR := by
  unfold financialRepression
  exact mul_nonneg hFR₀ (rpow_nonneg (fr_inner_nonneg hS hSc) _)

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:354

Module Section

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

In the same file