Documentation

Lean 4 Proof

theorem basin_of_attraction_structure {k : ℕ} (hk : 2 ≤ k) :
    ∀ (m : ℕ), 3 ≤ m → ∀ (a₀ : ℝ),
    Filter.Tendsto (fun L => modeAfterL k m L a₀) Filter.atTop (nhds 0) :=
  fun _m hm a₀ => stability_contraction hk hm a₀

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:138

Module Section

Aggregation-invariant class results from Paper 1, Section 5:

In the same file