Documentation

Lean 4 Proof

theorem institutional_amplification {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T Tstar1 Tstar2 : ℝ} (hTs1 : 0 < Tstar1) (hTs2 : 0 < Tstar2)
    (h : Tstar1 ≤ Tstar2) (hT : 0 ≤ T) :
    effectiveCurvatureKeff J ρ T Tstar1 ≤ effectiveCurvatureKeff J ρ T Tstar2 := by
  simp only [effectiveCurvatureKeff]
  apply mul_le_mul_of_nonneg_left _ (le_of_lt (curvatureK_pos hJ hρ))
  -- max 0 (1 - T/T*₁) ≤ max 0 (1 - T/T*₂)
  apply max_le_max_left 0
  suffices T / Tstar2 ≤ T / Tstar1 by linarith
  rw [div_le_div_iff₀ hTs2 hTs1]
  exact mul_le_mul_of_nonneg_left h hT

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/MonetaryPolicy.lean:137

Module Section

Monetary Policy and the Liquidity Trap

In the same file