feat(BirkhoffSum.Pointwise): maximal inequality

Author: lua-vr

Mathlib/Dynamics/BirkhoffSum/Pointwise.lean

@@ -0,0 +1,316 @@
+/-
+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, Oliver Butterley
+-/
+module
+
+public import Mathlib.Dynamics.BirkhoffSum.Average
+public import Mathlib.MeasureTheory.MeasurableSpace.Invariants
+public import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
+public import Mathlib.Algebra.Order.Group.PartialSups
+public import Mathlib.Algebra.Order.Ring.Star
+public import Mathlib.Data.Real.StarOrdered
+public import Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving
+public import Mathlib.MeasureTheory.Integral.DominatedConvergence
+public import Mathlib.Topology.Algebra.Module.WeakDual
+
+/-!
+# Pointwise Ergodic Theorem
+
+The Pointwise Ergodic Theorem, also known as Birkhoff's Ergodic Theorem, establishes the convergence
+of time averages for dynamical systems.
+
+Let `(α, μ)` be a probability space and `f: α → α` be a measure-preserving transformation. The
+result states that, for any integrable function `φ  ∈ L¹(μ)`, the time averages
+`(1/n)∑_{k=0}^{n-1} φ(f^k x)` converge almost everywhere as `n → ∞` to a limit function `φ*`.
+Moreover the limit function `φ*` is essentially `f`-invariant and integrable with `∫φ* dμ = ∫φ dμ`.
+If the system is ergodic, then `φ*` equals the constant `∫f dμ` almost everywhere.
+
+The limit function `φ*` is equal to the conditional expectation of `φ` with respect to the σ-algebra
+of `f`-invariant sets. This is used explicitly during this proof and also in the main statement.
+
+## Main statements
+
+* `ae_tendsTo_birkhoffAverage_condExp`: time average coincides with conditional expectation
+
+-/
+
+variable {α : Type*}
+
+open MeasureTheory Measure MeasurableSpace Filter Topology
+
+section BirkhoffMax
+
+/-- The maximum of `birkhoffSum f g i` for `i` ranging from `0` to `n`. -/
+def birkhoffMax (f : α → α) (g : α → ℝ) : ℕ →o (α → ℝ) := partialSups (birkhoffSum f g)
+
+lemma birkhoffMax_nonneg {f : α → α} {g n} :
+    0 ≤ birkhoffMax f g n := by
+  apply (le_partialSups_of_le _ n.zero_le).trans'
+  rfl
+
+lemma birkhoffMax_succ {f : α → α} {g n} :
+    birkhoffMax f g (n + 1) = 0 ⊔ (g + birkhoffMax f g n ∘ f) := by
+  have : birkhoffSum f g ∘ Nat.succ = fun k ↦ g + birkhoffSum f g k ∘ f := by
+    funext
+    exact birkhoffSum_succ' ..
+  erw [partialSups_succ', this, partialSups_const_add, birkhoffSum_zero']
+  funext
+  simp [birkhoffMax, partialSups]
+
+example (p : Prop) (h : False ∨ p) : p := h.elim (·.elim) id
+
+lemma birkhoffMax_succ' {f : α → α} {g n x} (hpos : 0 < birkhoffMax f g (n + 1) x) :
+    birkhoffMax f g (n + 1) x = g x + birkhoffMax f g n (f x) := by
+  erw [birkhoffMax_succ, lt_sup_iff] at hpos
+  cases hpos with
+  | inl h => absurd h; exact lt_irrefl 0
+  | inr h =>
+    erw [birkhoffMax_succ, Pi.sup_apply, sup_of_le_right h.le] 
+    rfl
+
+lemma birkhoffMax_comp_le_succ {f : α → α} {g n} :
+    birkhoffMax f g n ≤ birkhoffMax f g (n + 1) := by
+  gcongr
+  exact n.le_succ
+
+lemma birkhoffMax_le_birkhoffMax {f : α → α} {g n x} (hpos : 0 < birkhoffMax f g n x) :
+    birkhoffMax f g n x ≤ g x + birkhoffMax f g n (f x) := by
+  match n with
+  | 0 => absurd hpos; exact lt_irrefl 0
+  | n + 1 => 
+    apply le_of_eq_of_le (birkhoffMax_succ' hpos)
+    apply add_le_add_right
+    exact birkhoffMax_comp_le_succ (f x)
+
+lemma birkhoffMax_pos_of_mem_support {f : α → α} {g : α → ℝ} {n x}
+    (hx : x ∈ (birkhoffMax f g n).support) : 0 < birkhoffMax f g n x := by
+  apply lt_or_gt_of_ne at hx
+  cases hx with
+  | inl h =>
+    absurd h; exact (birkhoffMax_nonneg x).not_gt
+  | inr h => exact h
+
+-- TODO: move elsewhere
+@[measurability]
+lemma birkhoffSum_measurable [MeasurableSpace α] {f : α → α} (hf : Measurable f) {g : α → ℝ}
+    (hg : Measurable g) {n} : Measurable (birkhoffSum f g n) := by
+  apply Finset.measurable_sum
+  measurability
+
+@[measurability]
+lemma birkhoffMax_measurable [MeasurableSpace α] {f : α → α} (hf : Measurable f) {g : α → ℝ}
+    (hg : Measurable g) {n} : Measurable (birkhoffMax f g n) := by
+  unfold birkhoffMax
+  induction n <;> measurability
+
+section MeasurePreserving
+
+variable {f : α → α} [MeasurableSpace α] (μ : Measure α := by volume_tac) {g : α → ℝ} {n}
+  (hf : MeasurePreserving f μ μ) (hg : Integrable g μ)
+
+include hf
+
+@[measurability]
+lemma birkhoffSum_aestronglyMeasurable (hg : AEStronglyMeasurable g μ) :
+    AEStronglyMeasurable (birkhoffSum f g n) μ := by
+  apply Finset.aestronglyMeasurable_fun_sum
+  exact fun i _ => hg.comp_measurePreserving (hf.iterate i)
+
+@[measurability]
+lemma birkhoffMax_aestronglyMeasurable (hg : AEStronglyMeasurable g μ) :
+    AEStronglyMeasurable (birkhoffMax f g n) μ := by
+  unfold birkhoffMax
+  induction n <;> measurability
+
+include hg
+
+-- TODO: move elsewhere
+lemma birkhoffSum_integrable : Integrable (birkhoffSum f g n) μ :=
+  integrable_finset_sum _ fun _ _ ↦ (hf.iterate _).integrable_comp_of_integrable hg
+
+lemma birkhoffMax_integrable : Integrable (birkhoffMax f g n) μ := by
+  unfold birkhoffMax
+  induction n with
+  | zero => exact integrable_zero ..
+  | succ n hn => simpa using Integrable.sup hn (birkhoffSum_integrable μ hf hg)
+
+lemma birkhoffMax_integral_le :
+    ∫ x, birkhoffMax f g n x ∂μ ≤
+    ∫ x in (birkhoffMax f g n).support, g x ∂μ +
+    ∫ x in (birkhoffMax f g n).support, birkhoffMax f g n (f x) ∂μ := by
+  have := hf.integrable_comp_of_integrable (birkhoffMax_integrable μ hf hg (n := n))
+  rw [←integral_add hg.restrict, ←setIntegral_support]
+  · apply setIntegral_mono_on₀
+    · exact (birkhoffMax_integrable μ hf hg).restrict
+    · exact .add hg.restrict this.restrict
+    · exact AEStronglyMeasurable.nullMeasurableSet_support (by measurability)
+    · intro x hx
+      exact birkhoffMax_le_birkhoffMax (birkhoffMax_pos_of_mem_support hx)
+  · exact this.restrict
+
+lemma setIntegral_nonneg_on_birkhoffMax_support :
+    0 ≤ ∫ x in (birkhoffMax f g n).support, g x ∂μ := by
+  have hg₁ : AEStronglyMeasurable (birkhoffMax f g n) μ := by measurability
+  have hg₂ : Integrable (birkhoffMax f g n) μ := birkhoffMax_integrable μ hf hg
+  have hg₃ : Integrable (birkhoffMax f g n ∘ f) μ := hf.integrable_comp_of_integrable hg₂
+  calc
+    0 ≤ ∫ x in (birkhoffMax f g n).supportᶜ, birkhoffMax f g n (f x) ∂μ := by
+      exact integral_nonneg (fun x  => birkhoffMax_nonneg (f x))
+    _ = ∫ x, birkhoffMax f g n (f x) ∂μ -
+        ∫ x in (birkhoffMax f g n).support, birkhoffMax f g n (f x) ∂μ := by
+      exact setIntegral_compl₀ hg₁.nullMeasurableSet_support hg₃
+    _ = ∫ x, birkhoffMax f g n x ∂μ -
+        ∫ x in (birkhoffMax f g n).support, birkhoffMax f g n (f x) ∂μ := by
+      rw [←integral_map hf.aemeasurable (hf.map_eq.symm ▸ hg₁), hf.map_eq]
+    _ ≤ ∫ x in (birkhoffMax f g n).support, g x ∂μ := by
+      grw [birkhoffMax_integral_le μ hf hg]
+      grind
+
+end MeasurePreserving
+
+end BirkhoffMax
+
+section PR -- todo: separate PR
+
+variable {ι α : Type*} [Preorder ι] [LocallyFiniteOrderBot ι] [LinearOrder α]
+
+theorem partialSups_exists (f : ι → α) (i : ι) :
+    ∃ j ≤ i, partialSups f i = f j := by
+  obtain ⟨j, hj⟩ : ∃ j ∈ Finset.Iic i, ∀ k ∈ Finset.Iic i, f k ≤ f j :=
+    Finset.exists_max_image _ _ ⟨i, Finset.mem_Iic.mpr le_rfl⟩
+  simp_all only [Finset.mem_Iic, partialSups, OrderHom.coe_mk]
+  use j, hj.1
+  apply le_antisymm
+  · exact Finset.sup'_le _ _ fun k hk => hj.2 k (Finset.mem_Iic.1 hk)
+  · exact Finset.le_sup' _ (Finset.mem_Iic.2 hj.1 )
+
+end PR
+
+section BirkhoffSup
+
+def birkhoffSupSet (f : α → α) (g : α → ℝ) : Set α :=
+  {x | ∃ n : ℕ, 0 < birkhoffSum f g n x}
+
+lemma birkhoffSupSet_eq_iSup_birkhoffMax_support {f : α → α} {g : α → ℝ} :
+    birkhoffSupSet f g = ⋃ n : ℕ, (birkhoffMax f g n).support := by
+  ext x
+  simp only [birkhoffSupSet, Set.mem_setOf_eq, Set.mem_iUnion, Function.mem_support]
+  constructor
+  · refine fun ⟨n, hn⟩ => ⟨n, ?_⟩
+    apply ne_of_gt
+    apply hn.trans_le
+    exact le_partialSups (birkhoffSum f g) _ _
+  · rintro ⟨n, hn⟩
+    apply lt_or_gt_of_ne at hn
+    cases hn with
+    | inl h => absurd h; exact not_lt_of_ge (birkhoffMax_nonneg x)
+    | inr h =>
+      rw [birkhoffMax, Pi.partialSups_apply] at h
+      rcases partialSups_exists (birkhoffSum f g · x) n with ⟨m, _, hm₂⟩
+      exact ⟨m, hm₂ ▸ h⟩
+
+def birkhoffAverageSupSet (f : α → α) (g : α → ℝ) (a : ℝ) : Set α :=
+  {x | ∃ n : ℕ, a < birkhoffAverage ℝ f g n x}
+
+theorem birkhoffAverage_iff_birkhoffSum {f : α → α} {x n g} {a : ℝ} (hn : 0 < n) :
+    a < birkhoffAverage ℝ f g n x ↔ 0 < birkhoffSum f (g - fun _ ↦ a) n x := by
+  nth_rw 2 [←smul_lt_smul_iff_of_pos_left (a := (↑n : ℝ)⁻¹) (by norm_num [hn])]
+  rw [smul_zero, ←birkhoffAverage, birkhoffAverage_sub]
+  simp only [Pi.sub_apply, sub_pos]
+  nth_rw 2 [birkhoffAverage_of_comp_eq rfl hn.ne']
+
+theorem birkhoffAverageSupSet_eq_birkhoffSupSet {f : α → α} {g a} (ha : 0 < a) :
+    birkhoffAverageSupSet f g a = birkhoffSupSet f (g - fun _ ↦ a) := by
+  unfold birkhoffAverageSupSet birkhoffSupSet
+  have {n x} : a < birkhoffAverage ℝ f g n x ↔ 0 < birkhoffSum f (g - fun _ ↦ a) n x := by
+    cases n with
+    | zero =>
+      refine ⟨fun h => ?_, fun h => ?_⟩
+      · exfalso; rw [birkhoffAverage_zero] at h; exact lt_asymm ha h
+      · exfalso; rw [birkhoffSum_zero] at h; exact lt_irrefl 0 h
+    | succ n => exact birkhoffAverage_iff_birkhoffSum (by norm_num)
+  conv =>
+    enter [1, 1, x, 1, n]
+    rw [this]
+
+section MeasurePreserving
+
+variable {f : α → α} [MeasurableSpace α] (μ : Measure α := by volume_tac) {n}
+  (hf : MeasurePreserving f μ μ)
+
+include hf
+
+section Real
+
+variable {g : α → ℝ} (hg : Integrable g μ)
+
+include hg
+
+lemma tendsto_setIntegral_on_birkhoffMax_support_birkhoffSupSet :
+    Tendsto (fun n ↦ ∫ x in (birkhoffMax f g n).support, g x ∂μ) atTop
+            (𝓝 <| ∫ x in birkhoffSupSet f g, g x ∂ μ) := by
+  rw [birkhoffSupSet_eq_iSup_birkhoffMax_support]
+  apply tendsto_setIntegral_of_monotone₀ _ _ hg.integrableOn
+  · intros
+    exact AEStronglyMeasurable.nullMeasurableSet_support (by measurability)
+  · intro i j hij x
+    have : 0 ≤ birkhoffMax f g i x := birkhoffMax_nonneg x
+    have := (birkhoffMax f g).mono hij x
+    grind [Function.mem_support]
+
+/-- The *Maximal Ergodic Theorem*
+
+The integral of `g` over the set where the supremum of the Birkhoff sums
+is positive is non-negative. -/
+theorem setIntegral_nonneg_on_birkhoffSupSet :
+    0 ≤ ∫ x in birkhoffSupSet f g, g x ∂μ := by
+  apply ge_of_tendsto' (tendsto_setIntegral_on_birkhoffMax_support_birkhoffSupSet μ hf hg)
+  intro n
+  exact setIntegral_nonneg_on_birkhoffMax_support μ hf hg
+
+variable [IsFiniteMeasure μ]
+
+theorem meas_birkhoffAverageSupSet_mul_le_integral (a : ℝ) (ha : 0 < a) :
+    μ.real (birkhoffAverageSupSet f g a) • a ≤ ∫ x in birkhoffAverageSupSet f g a, g x ∂μ := by
+  have p₁ := Integrable.sub hg (integrable_const a)
+  calc
+    _ = ∫ x in birkhoffSupSet f (g - fun _ ↦ a), a ∂μ := by
+      rw [setIntegral_const, birkhoffAverageSupSet_eq_birkhoffSupSet ha]
+    _ ≤ ∫ x in birkhoffSupSet f (g - fun _ ↦ a), a ∂μ +
+        ∫ x in birkhoffSupSet f (g - fun _ ↦ a), g x - a ∂μ := by
+      exact le_add_of_nonneg_right (setIntegral_nonneg_on_birkhoffSupSet μ hf p₁)
+    _ = ∫ x in birkhoffAverageSupSet f g a, g x ∂μ := by
+      rw [← integral_add, birkhoffAverageSupSet_eq_birkhoffSupSet ha]
+      · rcongr; grind
+      · exact (integrable_const a).restrict
+      · exact p₁.restrict
+
+end Real
+
+section NormedAddCommGroup
+
+variable {E : Type*} [NormedAddCommGroup E] {g : α → E} (hg : Integrable g μ) [IsFiniteMeasure μ]
+
+include hg
+
+theorem meas_birkhoffAverageSupSet_mul_le_norm (a : ℝ) (ha : 0 < a) :
+    μ.real (birkhoffAverageSupSet f (fun x ↦ ‖g x‖) a) • a ≤ ∫ x, ‖g x‖ ∂μ :=
+  calc
+    _ ≤ ∫ x in birkhoffAverageSupSet f (fun x ↦ ‖g x‖) a, ‖g x‖ ∂μ := by
+      exact meas_birkhoffAverageSupSet_mul_le_integral μ hf hg.norm a ha
+    _ ≤ ∫ x, ‖g x‖ ∂μ := setIntegral_le_integral hg.norm (ae_of_all _ (norm_nonneg <| g ·))
+
+end NormedAddCommGroup
+
+end MeasurePreserving
+
+end BirkhoffSup
+
+noncomputable section BirkhoffAverage
+
+variable {f : α → α} [MeasurableSpace α] (μ : Measure α := by volume_tac) {g : α → ℝ} {n}
+  (hf : MeasurePreserving f μ μ) (hg : Integrable g μ)
+
+end BirkhoffAverage