BoundedGenericSet.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform generic sets for bounded observables

The maximal estimate is applied to the small L1 residual of a single finite orbit average. The complementary part is an explicit bounded coboundary. Consequently one fixed set controls every sufficiently large averaging length, including lengths chosen from a nearby pair.

lemma OAI.DukePrimeDegree.measurable_orbit_average line 23
lemma OAI.DukePrimeDegree.integrable_orbit_average line 29
lemma OAI.DukePrimeDegree.abs_orbit_average_le_of_abs_sum_le line 36

theorem OAI.DukePrimeDegree.exists_uniform_average_set_from_residual line 49

Source documentation

Quantitative good set from one finite-average residual.

theorem exists_uniform_average_set_from_residual
    (μ : Measure X) [IsFiniteMeasure μ]
    (T : X → X) (hT : MeasurePreserving T μ μ)
    (f : X → ℝ) (hfm : Measurable f) (hfi : Integrable f μ)
    (C : ℝ) (hC0 : 0 ≤ C) (hC : ∀ x, |f x| ≤ C)
    (c η : ℝ) (hη : 0 < η) (M : ℕ) (hM : M ≠ 0) :
    ∃ G : Set X, MeasurableSet G ∧
      μ Gᶜ ≤ ENNReal.ofReal
        ((∫ x, |birkhoffAverage ℝ T f M x - c| ∂μ) / η) ∧
      ∀ x ∈ G, ∀ N : ℕ, N ≠ 0 →
        |birkhoffAverage ℝ T f N x - c| ≤ (N : ℝ)⁻¹ * (2 * (M * C)) + η := by
…

theorem OAI.DukePrimeDegree.exists_uniform_generic_set_of_L1_convergence line 92

Source documentation

L1 convergence of bounded orbit averages yields a single measurable set of arbitrarily large measure with uniform eventual convergence. The convergence premise is stated separately so it can be supplied by an ergodic real flow after smoothing over one unit of time.

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