pointwise birkhoff theorem

Author: lua-vr

Mathlib/Data/EReal/Basic.lean

@@ -694,6 +694,14 @@ theorem coe_ennreal_mul : ∀ x y : ℝ≥0∞, ((x * y : ℝ≥0∞) : EReal) =
 theorem coe_ennreal_nsmul (n : ℕ) (x : ℝ≥0∞) : (↑(n • x) : EReal) = n • (x : EReal) :=
   map_nsmul (⟨⟨(↑), coe_ennreal_zero⟩, coe_ennreal_add⟩ : ℝ≥0∞ →+ EReal) _ _
 
+@[simp, norm_cast]
+theorem coe_ennreal_iSup {ι : Sort*} [hι : Nonempty ι] (f : ι → ℝ≥0∞) :
+    ((⨆ i, f i : ℝ≥0∞) : EReal) = ⨆ i, (f i : EReal) := by
+  refine le_antisymm ?_ (iSup_le fun i ↦ mod_cast le_iSup f i)
+  refine le_iSup_iff.mpr fun b hb ↦ ?_
+  lift b to ℝ≥0∞ using hι.elim fun i ↦ (EReal.coe_ennreal_nonneg _).trans (hb i)
+  exact mod_cast iSup_le fun i ↦ mod_cast hb i
+
 /-! ### toENNReal -/
 
 /-- `x.toENNReal` returns `x` if it is nonnegative, `0` otherwise. -/

Mathlib/Dynamics/BirkhoffSum/Average.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Dynamics.BirkhoffSum.Basic
 public import Mathlib.Algebra.Module.Basic
+public import Mathlib.Analysis.Normed.Group.Defs
 
 /-!
 # Birkhoff average

Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean

@@ -98,6 +98,27 @@ theorem tendsto_birkhoffAverage_apply_sub_birkhoffAverage' {g : α → E}
     Tendsto (fun n ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0) :=
   tendsto_birkhoffAverage_apply_sub_birkhoffAverage _ <| h.subset <| range_comp_subset_range _ _
 
+section TriangleInequality
+
+variable {f : α → α} {g : α → E} {n : ℕ} {x : α}
+
+@[bound]
+lemma norm_birkhoffSum_le :
+    ‖birkhoffSum f g n x‖ ≤ birkhoffSum f (‖g ·‖) n x :=
+  norm_sum_le _ _
+
+@[bound]
+lemma norm_birkhoffAverage_le {R : Type*} [RCLike R] [NormedSpace R E] :
+    ‖birkhoffAverage R f g n x‖ ≤ birkhoffAverage ℝ f (‖g ·‖) n x := by
+  by_cases! h : n = 0
+  · simp [birkhoffAverage, h]
+  apply Nat.zero_lt_of_ne_zero at h
+  simp only [birkhoffAverage, norm_smul, norm_inv, RCLike.norm_natCast, smul_eq_mul]
+  gcongr
+  exact norm_birkhoffSum_le
+
+end TriangleInequality
+
 end
 
 variable (𝕜 : Type*) {X E : Type*}

Mathlib/Dynamics/BirkhoffSum/Pointwise.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2025 Lua Viana Reis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lua Viana Reis
+-/
+module
+
+import Mathlib.Analysis.Oscillation
+import Mathlib.Dynamics.BirkhoffSum.Maximal
+import Mathlib.Dynamics.BirkhoffSum.NormedSpace
+import Mathlib.Analysis.InnerProductSpace.MeanErgodic
+
+open MeasureTheory Measure MeasurableSpace Filter Topology Module
+open scoped NNReal ENNReal
+
+variable {α R M : Type*} {f : α → α} {g : α → M} {n : ℕ} [RCLike R]
+  [MeasurableSpace α] (μ : Measure α) (hf : MeasurePreserving f μ μ)
+  [NormedAddCommGroup M] (hg : Integrable g μ) [IsFiniteMeasure μ] [NormedSpace R M]
+
+variable {μ} (R M) in
+abbrev koopman (p) : End R (Lp M p μ) := Lp.compMeasurePreservingₗ R f hf
+
+variable (R M f) in
+def convergenceSet := {g : Lp M 1 μ | ∀ᵐ x ∂μ, oscillation (birkhoffAverage R f g · x) atTop = 0}
+
+lemma mem_convergenceSet_of_mem_coboundary {g : Lp M 1 μ}
+    (hg : g ∈ End.coboundaries (koopman R M hf 1)) : g ∈ convergenceSet R M f μ := by
+  rcases hg with ⟨h, hh⟩
+  simp at hh
+
+  sorry
+
+lemma ENNReal.forall_pos_of_forall_mul {motive : ℝ≥0∞ → Prop} (k : ℝ≥0∞)
+    (h : ∀ ε > 0, motive (k * ε)) (hk₀ : k ≠ 0 := by positivity) (hk : k ≠ ∞ := by finiteness) :
+    ∀ ε > 0, motive ε := fun ε hε ↦
+  ENNReal.mul_div_cancel (a := k) (b := ε) hk₀ hk ▸ h (ε / k) (ENNReal.div_pos hε.ne_zero hk)
+
+omit [IsFiniteMeasure μ] in
+lemma foo {f : α → ℝ≥0∞} (h : ∀ ε > 0, ∀ᵐ x ∂μ, f x ≤ ε) : ∀ᵐ x ∂μ, f x ≤ 0 := by
+  have H : ∀ᵐ x ∂μ, ∀ n : ℕ, f x ≤ (n : ℝ≥0∞)⁻¹ :=
+    ae_all_iff.mpr fun n ↦ h _ (ENNReal.inv_pos.mpr (by finiteness))
+  filter_upwards [H] with x hx
+  refine le_of_forall_pos_le_add fun ε hε => ?_
+  obtain ⟨n, hn⟩ := ENNReal.exists_inv_nat_lt hε.ne_zero
+  exact (hx n).trans (by simp [hn.le])
+
+include hf in
+theorem closed_convergenceSet : IsClosed (convergenceSet R M f μ) := by
+  refine isClosed_of_closure_subset (fun g hg ↦ ?_)
+  rw [EMetric.mem_closure_iff] at hg
+  simp only [convergenceSet, ← nonpos_iff_eq_zero, Set.mem_setOf_eq]
+  apply foo
+  refine ENNReal.forall_pos_of_forall_mul 2 fun δ hδ ↦ ?_
+  by_cases! hδ' : δ = ∞; · bound
+  apply ae_iff.mpr <| nonpos_iff_eq_zero.mp _
+  push Not
+  have (h : Lp M 1 μ) (hh : h ∈ convergenceSet R M f μ) :
+      ∀ᵐ x ∂μ, 2 * δ < oscillation (birkhoffAverage R f g · x) atTop →
+      δ < birkhoffAverageSup f (‖(⇑g - ⇑h) ·‖) x := by
+    filter_upwards [hh] with x hosc hx
+    have := hx.trans_le <| oscillation_le_add_sub (f₂ := (birkhoffAverage R f h · x)) ..
+    rw [hosc] at this
+    grw [oscillation_le_two_mul_iSup_enorm] at this
+    simp only [Pi.sub_apply, zero_add, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
+      ENNReal.ofNat_ne_top, ENNReal.mul_lt_mul_iff_right] at this
+    change _ < ⨆ n, ‖(birkhoffAverage R f g - _) n x‖ₑ at this
+    rw [← birkhoffAverage_sub] at this
+    simp_rw [← EReal.coe_ennreal_lt_coe_ennreal_iff, EReal.coe_ennreal_iSup] at this
+    exact this.trans_le (iSup_mono fun _ ↦ EReal.coe_le_coe norm_birkhoffAverage_le)
+  refine le_of_forall_gt fun c hc ↦ ?_
+  rcases hg (δ * c) (by positivity) with ⟨h, hh, hh'⟩
+  apply measure_mono_ae (this h hh) |>.trans_lt
+
+  apply iSup_distribution_birkhoffAverageSup_le_norm' μ hf (by fun_prop) δ |>.trans_lt
+  rw [Integrable.toL1_sub g h (by fun_prop) (by fun_prop), ← edist_eq_enorm_sub,
+    Integrable.toL1_coeFn, Integrable.toL1_coeFn]
+  apply ENNReal.mul_lt_mul_right (ENNReal.inv_ne_zero.mpr hδ') (by finiteness) hh' |>.trans_le
+  rw [ENNReal.inv_mul_cancel_left (by positivity) hδ']

Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean

@@ -100,6 +100,7 @@ end AEEqFun
 
 namespace L1
 
+
 @[fun_prop]
 theorem integrable_coeFn (f : α →₁[μ] β) : Integrable f μ := by
   rw [← memLp_one_iff_integrable]

Mathlib/Order/LiminfLimsup.lean

@@ -815,17 +815,17 @@ section ConditionallyCompleteLinearOrder
 variable [ConditionallyCompleteLinearOrder α]
 
 /-- If `Filter.limsup u atTop ≤ x`, then for all `ε > 0`, eventually we have `u b < x + ε`. -/
-theorem eventually_lt_add_pos_of_limsup_le [Preorder β] [AddZeroClass α] [AddLeftStrictMono α]
-    {x ε : α} {u : β → α} (hu_bdd : IsBoundedUnder LE.le atTop u) (hu : Filter.limsup u atTop ≤ x)
-    (hε : 0 < ε) :
-    ∀ᶠ b : β in atTop, u b < x + ε :=
+theorem eventually_lt_add_pos_of_limsup_le [AddZeroClass α] [AddLeftStrictMono α]
+    {x ε : α} {u : β → α} {f : Filter β} (hu_bdd : IsBoundedUnder LE.le f u)
+    (hu : Filter.limsup u f ≤ x) (hε : 0 < ε) :
+    ∀ᶠ b : β in f, u b < x + ε :=
   eventually_lt_of_limsup_lt (lt_of_le_of_lt hu (lt_add_of_pos_right x hε)) hu_bdd
 
 /-- If `x ≤ Filter.liminf u atTop`, then for all `ε < 0`, eventually we have `x + ε < u b`. -/
-theorem eventually_add_neg_lt_of_le_liminf [Preorder β] [AddZeroClass α] [AddLeftStrictMono α]
-    {x ε : α} {u : β → α} (hu_bdd : IsBoundedUnder GE.ge atTop u) (hu : x ≤ Filter.liminf u atTop)
-    (hε : ε < 0) :
-    ∀ᶠ b : β in atTop, x + ε < u b :=
+theorem eventually_add_neg_lt_of_le_liminf [AddZeroClass α] [AddLeftStrictMono α]
+    {x ε : α} {u : β → α} {f : Filter β} (hu_bdd : IsBoundedUnder GE.ge f u)
+    (hu : x ≤ Filter.liminf u f) (hε : ε < 0) :
+    ∀ᶠ b : β in f, x + ε < u b :=
   eventually_lt_of_lt_liminf (lt_of_lt_of_le (add_lt_of_neg_right x hε) hu) hu_bdd
 
 /-- If `Filter.limsup u atTop ≤ x`, then for all `ε > 0`, there exists a positive natural