Documentation

Lean 4 Proof

theorem fr_deriv_diverges {FR₀ α_FR S_crit : ℝ}
    (hFR₀ : 0 < FR₀) (hα_pos : 0 < α_FR) (hα_lt : α_FR < 1) (hSc : 0 < S_crit) :
    Tendsto (fun S => frDerivMagnitude FR₀ α_FR S_crit S)
      (nhdsWithin S_crit (Set.Iio S_crit)) atTop := by
  unfold frDerivMagnitude
  have hc : 0 < FR₀ * α_FR / S_crit := div_pos (mul_pos hFR₀ hα_pos) hSc
  apply Filter.Tendsto.const_mul_atTop hc
  have hexp : α_FR - 1 < 0 := by linarith
  exact (tendsto_rpow_neg_nhdsGT_zero hexp).comp
    (tendsto_one_minus_div_nhdsWithin hSc)

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:489

Module Section

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

In the same file