Documentation

Lean 4 Proof

private lemma tendsto_one_minus_div_nhdsWithin {S_crit : ℝ} (hSc : 0 < S_crit) :
    Tendsto (fun S : ℝ => 1 - S / S_crit) (nhdsWithin S_crit (Set.Iio S_crit))
      (nhdsWithin 0 (Set.Ioi 0)) := by
  apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
  · have : Tendsto (fun S : ℝ => 1 - S / S_crit) (nhds S_crit) (nhds 0) := by
      have h1 : (fun S : ℝ => 1 - S / S_crit) = (fun S => 1 - S * S_crit⁻¹) := by
        ext; simp [div_eq_mul_inv]
      rw [h1]
      have h2 : 1 - S_crit * S_crit⁻¹ = 0 := by
        rw [mul_inv_cancel₀ (ne_of_gt hSc)]; ring
      rw [← h2]
      exact (tendsto_const_nhds.sub (tendsto_id.mul_const _))
    exact this.mono_left nhdsWithin_le_nhds
  · apply eventually_nhdsWithin_of_forall
    intro S hS
    simp only [Set.mem_Ioi]
    linarith [div_lt_one hSc |>.mpr hS]

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:459

Module Section

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

In the same file