Documentation

Lean 4 Proof

theorem fr_decreasing {FR₀ S₁ S₂ S_crit α_FR : ℝ}
    (hFR₀ : 0 ≤ FR₀) (hα : 0 < α_FR) (hSc : 0 < S_crit)
    (_hS₁ : 0 ≤ S₁) (hS₂ : 0 ≤ S₂) (hS : S₁ ≤ S₂) :
    financialRepression FR₀ S₂ S_crit α_FR ≤ financialRepression FR₀ S₁ S_crit α_FR := by
  unfold financialRepression
  apply mul_le_mul_of_nonneg_left _ hFR₀
  apply rpow_le_rpow (fr_inner_nonneg hS₂ hSc)
  · linarith [min_le_min_left (1 : ℝ) (div_le_div_of_nonneg_right hS (le_of_lt hSc))]
  · exact le_of_lt hα

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:388

Module Section

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

In the same file