InvariantMeanLimit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual nonergodic invariant mean

The L2 mean ergodic theorem constructs the invariant observable used by the uniform generic-set theorem. Its integral agrees with the original observable; it is not asserted to be constant.

theorem OAI.DukePrimeDegree.exists_measurable_invariant_L1_mean line 21

theorem OAI.DukePrimeDegree.exists_invariant_mean_with_uniform_generic_sets line 87

Source documentation

A bounded observable has fixed uniform generic sets around its actual invariant mean, even for a nonergodic sampling transformation.

theorem exists_invariant_mean_with_uniform_generic_sets
    (μ : Measure Y) [IsProbabilityMeasure μ]
    (T : Y → Y) (hT : MeasurePreserving T μ μ)
    (f : Y → ℝ) (hfm : Measurable f)
    (C : ℝ) (hC0 : 0 ≤ C) (hC : ∀ x, |f x| ≤ C) :
    ∃ q : Y → ℝ, Measurable q ∧ Integrable q μ ∧
      (fun x => q (T x)) =ᵐ[μ] q ∧ (∫ x, q x ∂μ) = ∫ x, f x ∂μ ∧
      ∀ ε δ : ℝ, 0 < ε → 0 < δ →
        ∃ G : Set Y, MeasurableSet G ∧ μ Gᶜ ≤ ENNReal.ofReal δ ∧
          ∃ N₀ : ℕ, ∀ x ∈ G, ∀ N ≥ N₀,
            |birkhoffAverage ℝ T f N x - q x| ≤ ε := by
…