Documentation

Lean 4 Proof

theorem stability_contraction {k : ℕ} (hk : 2 ≤ k) {m : ℕ} (hm : 3 ≤ m) (a₀ : ℝ) :
    Filter.Tendsto (fun L => modeAfterL k m L a₀) Filter.atTop (nhds 0) := by
  simp only [modeAfterL]
  have ⟨hpos, hlt⟩ := modeRate_in_unit_interval hk hm
  have h := tendsto_pow_atTop_nhds_zero_of_lt_one hpos.le hlt
  have h2 := h.mul tendsto_const_nhds (b := a₀)
  rwa [zero_mul] at h2

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:182

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file