HopfMeanBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Mean bounds from eventual orbit excursions

A conull union of positive finite excursions has nonnegative mean by the finite Hopf inequality. This avoids assuming integrability of an unbounded information function before truncating it.

theorem OAI.DukePrimeDegree.integral_nonneg_of_ae_positive_birkhoffSum line 21

Source documentation

Positive partial sums somewhere along almost every orbit force a nonnegative integral.

theorem integral_nonneg_of_ae_positive_birkhoffSum
    {Y : Type*} [MeasurableSpace Y] {μ : Measure Y}
    {T : Y → Y} {f : Y → ℝ} (hT : MeasurePreserving T μ μ)
    (hf : Integrable f μ) (hfm : Measurable f)
    (hexc : ∀ᵐ x ∂μ, ∃ n : ℕ, 0 < birkhoffSum T f n x) :
    0 ≤ ∫ x, f x ∂μ := by
…

theorem OAI.DukePrimeDegree.integral_le_of_ae_birkhoffSum_lt line 48

Source documentation

A bounded observable whose orbit average is eventually below c has mean at most c.

theorem integral_le_of_ae_birkhoffSum_lt
    {Y : Type*} [MeasurableSpace Y] {μ : Measure Y} [IsProbabilityMeasure μ]
    {T : Y → Y} {g : Y → ℝ} (hT : MeasurePreserving T μ μ)
    (hg : Integrable g μ) (hgm : Measurable g) (c : ℝ)
    (hexc : ∀ᵐ x ∂μ, ∃ n : ℕ, birkhoffSum T g n x < c * n) :
    (∫ x, g x ∂μ) ≤ c := by
…