Documentation

Lean 4 Proof

theorem hump_long_run_zero {lam : ℝ} (hlam : 0 < lam) (a : ℝ) :
    Filter.Tendsto (fun h : ℝ => a * h * Real.exp (-lam * h))
                   Filter.atTop (nhds 0) := by
  rcases eq_or_ne a 0 with rfl | ha
  · simp
  · -- Normalize: exp(-lam*h) = exp(-(lam*h)) for compatibility with composition
    have hrw : (fun h : ℝ => a * h * Real.exp (-lam * h)) =
               (fun h => a * h * Real.exp (-(lam * h))) := by
      funext h; congr 1; ring
    rw [hrw]
    -- Build: lam*h * exp(-(lam*h)) → 0 via h ↦ lam*h substitution
    have h1 := (Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero 1).comp
      (Filter.Tendsto.const_mul_atTop hlam Filter.tendsto_id)
    have h2 : Filter.Tendsto (fun h : ℝ => lam * h * Real.exp (-(lam * h)))
        Filter.atTop (nhds 0) := by
      convert h1 using 1; funext h; simp [Function.comp, id]
    -- Scale: a * h * exp(-(lam*h)) = (a/lam) * (lam * h * exp(-(lam*h)))
    have h3 := h2.const_mul (a / lam)
    simp only [mul_zero] at h3
    convert h3 using 1
    funext h
    field_simp [hlam.ne']

Dependency Graph

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:201

Module Section

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

In the same file