Documentation

Lean 4 Proof

theorem spectralGap_convergence {gap₁ gap₂ : ℝ} (h₁ : 0 < gap₁) (hlt : gap₁ < gap₂) :
    1 / gap₂ < 1 / gap₁ := by
  exact div_lt_div_of_pos_left one_pos h₁ hlt

Dependency Graph

Location

thesis/CESProofs/Applications/OpenEconomy.lean:211

Module Section

Open Economy Monetary Transmission

In the same file