Topological multiple recurrence

DefinitionMultiply recurrent point#✓fully proved

Let \(X\) be a topological space and \(T \colon X \to X\) a map. A point \(x \in X\) is multiply recurrent for \(T\) if for every integer \(d \ge 1\) there is a strictly increasing sequence of natural numbers \((n_k)\) such that \(T^{j n_k}(x) \to x\) as \(k \to \infty\) for every integer \(j\) with \(1 \le j \le d\), where \(T^{m}\) denotes the \(m\)-th iterate of \(T\).

def IsMultiplyRecurrent {X : Type*} [TopologicalSpace X]
    (T : X → X) (x : X) : Prop :=
  ∀ d : ℕ, 1 ≤ d →
    ∃ n : ℕ → ℕ, StrictMono n ∧
      ∀ j : ℕ, 1 ≤ j → j ≤ d →
        Tendsto (fun k : ℕ => T^[j * n k] x) atTop (𝓝 x)

Used by 1

Used byFurstenberg–Weiss multiple recurrence for a single homeomorphism

TheoremFurstenberg–Weiss multiple recurrence for a single homeomorphism#●ready to prove

Every homeomorphism \(T\) of a nonempty compact metric space \(X\) has a multiply recurrent point: there is a point \(x \in X\) such that for every integer \(d \ge 1\) there is a strictly increasing sequence of natural numbers \((n_k)\) with \(T^{j n_k}(x) \to x\) as \(k \to \infty\) for every integer \(j\) with \(1 \le j \le d\), where \(T^{m}\) denotes the \(m\)-th iterate of \(T\).

public theorem_wanted furstenberg_topological_recurrence {X : Type*} [MetricSpace X]
    [CompactSpace X] [Nonempty X] (T : X ≃ₜ X) :
    ∃ x : X, IsMultiplyRecurrent (T : X → X) x

Sources

• H. Furstenberg and B. Weiss, Topological dynamics and combinatorial number theory, Journal d'Analyse Mathématique 34 (1978), 61-85. Listed as §56 (main theorem) in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem furstenberg_topological of the lean-eval benchmark.

Uses 1

Statement usesMultiply recurrent point

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.