Documentation

Lean 4 Proof

theorem iterate_norm_tendsto_top {μ x₀ : ℝ} (hμ : 1 < |μ|) (hx : x₀ ≠ 0) :
    Tendsto (fun n => |μ ^ n * x₀|) atTop atTop := by
  simp only [abs_mul, abs_pow]
  exact (tendsto_pow_atTop_atTop_of_one_lt hμ).atTop_mul_const (abs_pos.mpr hx)

Dependency Graph

Location

thesis/CESProofs/Dynamics/DiscreteStability.lean:87

Module Section

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

In the same file