Documentation

Lean 4 Proof

theorem iterate_tendsto_zero {μ x₀ : ℝ} (hμ : |μ| < 1) :
    Tendsto (fun n => μ ^ n * x₀) atTop (nhds 0) := by
  have h1 : Tendsto (fun n => μ ^ n) atTop (nhds 0) := by
    apply squeeze_zero_norm (fun n => ?_)
      (tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg μ) hμ)
    simp
  rw [show (0 : ℝ) = 0 * x₀ from (zero_mul _).symm]
  exact h1.mul_const x₀

Dependency Graph

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:77

Module Section

Discrete-Time Stability of CES Tâtonnement (Edge of Stability)

In the same file