OrbitConcentration.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Concentration from compactly controlled returns

If nearby returns of an ergodic action lie in a fixed compact set of translations in a larger group, the whole measure lies on one orbit of that group. This is the topological-measure argument in the reverse implication of EKL (2006), Proposition 4.3.

theorem OAI.DukePrimeDegree.ae_on_single_orbit_of_compact_returns line 27

Source documentation

Strong returns with compact translation parameters force a single orbit, once the ergodic component has a support point in the return set.

theorem ae_on_single_orbit_of_compact_returns
    (μ : Measure Y) [ErgodicSMul H Y μ]
    (φ : H →* C) (hφ : ∀ h : H, ∀ y : Y, (φ h) • y = h • y)
    (K : Set Y) (hK : MeasurableSet K)
    (z : Y) (hz : z ∈ (μ.restrict K).support)
    (V : Set Y) (hV : IsOpen V) (hzV : z ∈ V)
    (L : Set C) (hL : IsCompact L)
    (hret : ∀ u ∈ K ∩ V, ∀ h : H, h • u ∈ K ∩ V →
      ∃ c ∈ L, c • u = h • u) :
    ∀ᵐ y ∂μ, ∃ c : C, c • z = y := by
…