Documentation

Lean 4 Proof

theorem basin_is_global {k : ℕ} (hk : 2 ≤ k) {m : ℕ} (hm : 3 ≤ m)
    (a₀ : ℝ) (ε : ℝ) (hε : 0 < ε) :
    ∃ L₀ : ℕ, ∀ L, L₀ ≤ L → |modeAfterL k m L a₀| < ε := by
  have htend := stability_contraction hk hm a₀
  rw [Metric.tendsto_atTop] at htend
  obtain ⟨L₀, hL₀⟩ := htend ε hε
  exact ⟨L₀, fun L hL => by simpa [Real.dist_eq] using hL₀ L hL⟩

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:149

Module Section

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

In the same file