InvariantMeanGenericSet.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform generic sets with a nonconstant invariant mean

The ambient measure need not be ergodic for the chosen root flow. The uniform average is therefore compared with its actual invariant mean q(x). This keeps ambient stabilizer invariance available for the fiber-correction argument, without replacing q by the global integral.

def OAI.DukePrimeDegree.constantMeanOrbitSet line 22
lemma OAI.DukePrimeDegree.measurableSet_constantMeanOrbitSet line 25
lemma OAI.DukePrimeDegree.ae_mem_constantMeanOrbitSet line 30
lemma OAI.DukePrimeDegree.birkhoffAverage_eq_mean_on_orbitSet line 43

theorem OAI.DukePrimeDegree.exists_uniform_invariant_mean_set_from_residual line 57

Source documentation

One bounded coboundary plus the maximal inequality controls the nonconstant invariant mean on a full-measure orbit set.

theorem exists_uniform_invariant_mean_set_from_residual
    (μ : Measure Y) [IsFiniteMeasure μ]
    (T : Y → Y) (hT : MeasurePreserving T μ μ)
    (f : Y → ℝ) (hfm : Measurable f) (hfi : Integrable f μ)
    (C : ℝ) (hC0 : 0 ≤ C) (hC : ∀ x, |f x| ≤ C)
    (q : Y → ℝ) (hqm : Measurable q) (hqi : Integrable q μ)
    (hqinvariant : (fun x => q (T x)) =ᵐ[μ] q)
    (η : ℝ) (hη : 0 < η) (M : ℕ) (hM : M ≠ 0) :
    ∃ G : Set Y, MeasurableSet G ∧
      μ Gᶜ ≤ ENNReal.ofReal
        ((∫ x, |birkhoffAverage ℝ T f M x - q x| ∂μ) / η) ∧
      ∀ x ∈ G, ∀ N : ℕ, N ≠ 0 →
…

theorem OAI.DukePrimeDegree.exists_uniform_invariant_mean_set line 107

Source documentation

Fixed good sets for a nonergodic transformation. Their limiting observable is the invariant mean supplied by the mean-ergodic theorem.

theorem exists_uniform_invariant_mean_set
    (μ : Measure Y) [IsFiniteMeasure μ]
    (T : Y → Y) (hT : MeasurePreserving T μ μ)
    (f : Y → ℝ) (hfm : Measurable f) (hfi : Integrable f μ)
    (C : ℝ) (hC0 : 0 ≤ C) (hC : ∀ x, |f x| ≤ C)
    (q : Y → ℝ) (hqm : Measurable q) (hqi : Integrable q μ)
    (hqinvariant : (fun x => q (T x)) =ᵐ[μ] q)
    (hmean : Tendsto (fun M => ∫ x, |birkhoffAverage ℝ T f M x - q x| ∂μ)
      atTop (𝓝 0))
    (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ G : Set Y, MeasurableSet G ∧ μ Gᶜ ≤ ENNReal.ofReal δ ∧
      ∃ N₀ : ℕ, ∀ x ∈ G, ∀ N ≥ N₀,
…