OrbitSupport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Ergodic orbits accumulate on the support of a restricted measure

For a countable ergodic group action, almost every orbit meets every positive-measure set. Applying this to a countable topological basis shows that the orbit's visits to a measurable set accumulate on the support of the restricted measure. This is the orbit-density step of EKL (2006), Proposition 4.3.

theorem OAI.DukePrimeDegree.ae_orbit_meets_of_measure_ne_zero line 26

Source documentation

The saturation of a positive-measure set is conull in an ergodic action.

theorem ae_orbit_meets_of_measure_ne_zero
    (μ : Measure Y) [ErgodicSMul H Y μ]
    (S : Set Y) (hS : MeasurableSet S) (hpos : μ S ≠ 0) :
    ∀ᵐ y ∂μ, ∃ h : H, h • y ∈ S := by
…

theorem OAI.DukePrimeDegree.ae_restricted_support_subset_orbit_closure line 54

Source documentation

Almost every orbit's visits to K accumulate on the entire support of the restricted measure; no closedness assumption on K is needed.

theorem ae_restricted_support_subset_orbit_closure
    (μ : Measure Y) [ErgodicSMul H Y μ] (K : Set Y) (hK : MeasurableSet K) :
    ∀ᵐ y ∂μ, (μ.restrict K).support ⊆
      closure {z : Y | z ∈ K ∧ ∃ h : H, h • y = z} := by
…