Documentation

Lean 4 Proof

theorem cascade_long_run_zero {lam mu : ℝ} (hlam : 0 < lam) (hmu : 0 < mu) :
    Filter.Tendsto (fun h : ℝ => Real.exp (-mu * h) - Real.exp (-lam * h))
                   Filter.atTop (nhds 0) := by
  have key : ∀ c : ℝ, 0 < c →
      Filter.Tendsto (fun h : ℝ => Real.exp (-c * h)) Filter.atTop (nhds 0) := by
    intro c hc
    have h1 := Real.tendsto_exp_neg_atTop_nhds_zero.comp
      (Filter.Tendsto.const_mul_atTop hc Filter.tendsto_id)
    convert h1 using 1
    funext h; simp [neg_mul, id]
  have hsub := (key mu hmu).sub (key lam hlam)
  simp only [sub_self] at hsub
  exact hsub

Dependency Graph

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:181

Module Section

Proposition 6, Theorem 9, Corollaries 1-2 and 4:

In the same file