StrongReturnExclusion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Excluding positive-measure sets of strong neutral returns

Ergodic decomposition, the compact-return orbit-concentration argument, and the arithmetic centralizer-orbit obstruction together exclude a measurable positive-measure set with uniform strong neutral returns. This is the consequence of EKL (2006), Proposition 4.3 and Theorem 5.1, needed for the low-entropy alternative on the arithmetic quotient.

theorem OAI.DukePrimeDegree.strong_neutral_return_set_null line 25

theorem OAI.DukePrimeDegree.strong_neutral_return_set_null_of_ae line 89

Source documentation

An almost-everywhere version, so that recurrence null sets may be removed without changing the mass of the return set.

theorem strong_neutral_return_set_null_of_ae
    (d : ℕ) (hd : 2 < d + 1) {i j : Fin (d + 1)} (hij : i ≠ j)
    (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (K : Set (X (d + 1))) (hK : MeasurableSet K)
    (r : ℝ) (hr : 0 < r)
    (hstrong : ∀ᵐ x ∂μ, x ∈ K →
      ∀ (ell : Fin (d + 1) → ℝ) (hell : ∑ a, ell a = 0), ell i = ell j →
      rightAction x (diagonalOneParameter ell hell 1) ∈ K →
      ∀ g ∈ matrixBall (d + 1) r,
        rightAction x g = rightAction x (diagonalOneParameter ell hell 1) →
          g ∈ rootPairCentralizer hij) : μ K = 0 := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.rootPairCentralizer