PointwiseOrbitAverages.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Almost-everywhere convergence of finite orbit averages

For a countable measure-preserving action, finite convex averages of any L2 function have a subsequence converging almost everywhere to an exactly invariant measurable function. These are actual functions, so the convergence can be disintegrated to the conditional measures.

theorem OAI.PolycyclicRecognition.FiniteOrbitAverage.apply_congr_ae line 27

theorem OAI.PolycyclicRecognition.exists_pointwise_orbitAverages line 38

Source documentation

The measurable invariant limit of genuine finite orbit averages.

theorem exists_pointwise_orbitAverages (f : X → ℝ) (hf : MemLp f 2 μ) :
    ∃ (A : ℕ → FiniteOrbitAverage G) (F : X → ℝ),
      Measurable F ∧ (∀ (g : G) x, F (g • x) = F x) ∧
      ∀ᵐ x ∂μ, Tendsto (fun n => (A n).apply f x) atTop (𝓝 (F x)) := by
…

Mentions: OAI.PolycyclicRecognition.FiniteOrbitAverage