Hypercyclic operators

DefinitionHypercyclic operator#✓fully proved

A bounded operator T is hypercyclic if some vector has a dense orbit under iteration of T.

def IsHypercyclic (T : E →L[𝕜] E) : Prop :=
  ∃ x, Dense (Set.range fun n => (T ^ n) x)

Used by 2

Used byHypercyclicity criterion · Rolewicz's theorem

TheoremHypercyclicity criterion#✓fully proved

The hypercyclicity criterion: along a sequence n_k → ∞, suppose T^(n_k) x → 0 on the dense set X₀, S k y → 0 on the dense set Y₀, and T^(n_k) (S k y) → y on Y₀. Then T is hypercyclic. The Baire proof combines all three eventual estimates and uses cofinality to meet each rational ball after every prescribed time threshold. This includes the full-iterate, exact-inverse special case by taking n_k = id and converting the exact identities to constant convergence.

theorem isHypercyclic_of_criterion [BaireSpace E] [Nonempty E] (T : E →L[𝕜] E)
    (n_k : ℕ → ℕ) (hn_k : Tendsto n_k atTop atTop)
    (D X₀ Y₀ : Set E) (hDcount : D.Countable) (hDdense : Dense D)
    (hX₀ : Dense X₀) (hY₀ : Dense Y₀) (S : ℕ → E → E)
    (hT : ∀ x ∈ X₀, Tendsto (fun k => (T ^ n_k k) x) atTop (𝓝 0))
    (hS : ∀ y ∈ Y₀, Tendsto (fun k => S k y) atTop (𝓝 0))
    (hTS : ∀ y ∈ Y₀, Tendsto (fun k => (T ^ n_k k) (S k y)) atTop (𝓝 y)) :
    IsHypercyclic T

Uses 1 · Used by 1

Statement usesHypercyclic operator

Used byRolewicz's theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.