Birkhoff cleanup (#47)

* Initial pass in Pisa Signed-off-by: Marcello Seri <marcello.seri@gmail.com> * golf proof of `maxOfSums_Monotone ` * golf * Golf more proofs * Update Birkhoff.lean * Move to partialSup Signed-off-by: Marcello Seri <marcello.seri@gmail.com> * golf * BET: refactored using partialSup Signed-off-by: Marcello Seri <marcello.seri@gmail.com> * Proof of divSet_measurable Signed-off-by: Marcello Seri <marcello.seri@gmail.com> * BET: polish proofs Signed-off-by: Marcello Seri <marcello.seri@gmail.com> * BET: missing measure - fix variables and also the proofs Signed-off-by: Marcello Seri <marcello.seri@gmail.com> * BET: Cleanup Signed-off-by: Marcello Seri <marcello.seri@gmail.com> * Make small fix Signed-off-by: Marcello Seri <marcello.seri@gmail.com> --------- Signed-off-by: Marcello Seri <marcello.seri@gmail.com> Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
mseri · Jun 18, 2024 · d103573 · d103573
1 parent a05cf0a
commit d103573
Showing 1 changed file with 88 additions and 110 deletions.
diff --git a/BET/Birkhoff.lean b/BET/Birkhoff.lean
@@ -24,11 +24,15 @@ This file defines Birkhoff sums, other related notions and proves Birkhoff's erg
 
 -/
 
+/- TODO:
+  - define Birkhoff Average on actions, to be done much later, after mathlibization
+  - update the proof to this more general setting
+-/
+
 section Ergodic_Theory
 
 open BigOperators MeasureTheory
 
-
 /-
 - `T` is a measure preserving map of a probability space `(α, μ)`,
 - `φ : α → ℝ` is integrable.
@@ -39,7 +43,7 @@ The original sigma-algebra is now named m0 because we need to distiguish
 b/w that and the invariant sigma-algebra.
 -/
 variable {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
-variable (T : α → α) (hT : MeasurePreserving T μ)
+variable (T : α → α) (hT : MeasurePreserving T μ μ)
 variable (φ : α → ℝ) (hphi : Integrable φ μ) (hphim : Measurable φ)
 /- For the moment it's convenient to also assume that φ is measurable
 because for Lean Integrable means almost everywhere (strongly) measurable
@@ -57,138 +61,112 @@ This is for two reasons:
 def invSigmaAlg : MeasurableSpace α where
   -- same as `MeasurableSet' s := MeasurableSet s ∧ T ⁻¹' s = s`
   MeasurableSet' := fun s ↦ MeasurableSet s ∧ T ⁻¹' s = s
-  measurableSet_empty := by
-    constructor
-    · exact MeasurableSet.empty
-    · exact rfl
-  measurableSet_compl := by
-    -- intro s
-    -- dsimp only
-    -- intro hinit
-    -- obtain ⟨hinit1, hinit2⟩ := hinit
-    -- the above can be abbreviated as follows
-    intro h ⟨hinit1, hinit2⟩ 
-    constructor
-    · exact MeasurableSet.compl hinit1
-    · exact congrArg compl hinit2 -- this was suggested by Lean
+  measurableSet_empty := ⟨MeasurableSet.empty, rfl⟩
+  measurableSet_compl := fun h ⟨hinit1, hinit2⟩ ↦ ⟨MeasurableSet.compl hinit1, congrArg compl hinit2⟩
+
   measurableSet_iUnion := by
     -- now we explicitly want s, so we need to intro it
     intro s
     dsimp
     intro hinit
     constructor
-    · have hi1st : ∀ i, MeasurableSet (s i) := by
-        intro i
-        exact (hinit i).left
+    · have hi1st : ∀ i, MeasurableSet (s i) := fun i ↦(hinit i).left
       exact MeasurableSet.iUnion hi1st
-    · have hi2nd : ∀ i, T ⁻¹'(s i) = s i := by
-        intro i
-        exact (hinit i).right
+    · have hi2nd : ∀ i, T ⁻¹'(s i) = s i := fun i ↦ (hinit i).right
       rw [Set.preimage_iUnion]
       exact Set.iUnion_congr hi2nd
 
-
 /- it was hard to find out what `m ≤ m0` meant, when `m, m0` are measurable spaces.
 Hovering over the `≤` sign in infoview and following the links explained it:
 instance : LE (MeasurableSpace α) where le m₁ m₂ := ∀ s, MeasurableSet[m₁] s → MeasurableSet[m₂] s
 -/
-lemma leq_InvSigmaAlg_FullAlg : invSigmaAlg T ≤ m0 := by
-  intro s hs -- here the infoview is faulty and doesn't show everything (known Lean problem, Floris says)
-  exact hs.left
-
+/-- The invariant sigma algebra of T is a subalgebra of the measure space -/
+lemma leq_InvSigmaAlg_FullAlg : invSigmaAlg T ≤ m0 := fun _ hs ↦ hs.left
 
 open Finset in
-/-- The max of the first `n + 1` Birkhoff sums, i.e.,
-`maxOfSums T φ x n` corresponds to `max {birkhoffSum T φ 1 x,..., birkhoffSum T φ (n + 1) x}`. -/
-def maxOfSums (x : α) (n : ℕ) :=
-    sup' (range (n + 1)) (nonempty_range_succ) (fun k ↦ birkhoffSum T φ (k + 1) x)
-
-/- Note that maxOfSums T φ x n corresponds to Φ_{n+1} in our notation -/
+/-- The max of the first `n` Birkhoff sums, i.e.,
+`maxOfSums T φ x n` corresponds to
+`max {birkhoffSum T φ 1 x,..., birkhoffSum T φ (n + 1) x}`.
+This is because `birkhoffSum T φ 0 x := 0` is defined to be a sum over the empty set. -/
+def maxOfSums (x : α) : OrderHom ℕ ℝ :=
+  partialSups (fun n ↦ birkhoffSum T φ (n+1) x)
+/- was:
+   def maxOfSums (x : α) (n : ℕ) :=
+     sup' (range (n + 1)) (nonempty_range_succ) (fun k ↦ birkhoffSum T φ (k + 1) x)
+   Note that maxOfSums T φ x n corresponds to Φ_{n+1} in our notates -/
 
 theorem maxOfSums_zero : maxOfSums T φ x 0 = φ x := by
   unfold maxOfSums
-  simp only [zero_add, Finset.range_one, Finset.sup'_singleton, birkhoffSum_one']
+  simp [partialSups_zero, zero_add, birkhoffSum_one']
 
 /-- `maxOfSums` is monotone (one step version). -/
 theorem maxOfSums_succ_le (x : α) (n : ℕ) : (maxOfSums T φ x n) ≤ (maxOfSums T φ x (n + 1)) := by
-  exact Finset.sup'_mono (fun k ↦ birkhoffSum T φ (k + 1) x)
-    (Finset.range_subset.mpr (Nat.le.step Nat.le.refl)) Finset.nonempty_range_succ
+  unfold maxOfSums
+  simp [partialSups_succ, le_sup_left]
 
 /-- `maxOfSums` is monotone (general steps version). -/
 theorem maxOfSums_le_le (x : α) (m n : ℕ) (hmn : m ≤ n) :
     (maxOfSums T φ x m) ≤ (maxOfSums T φ x n) := by
   induction' n with n hi
-  rw [Nat.le_zero.mp hmn]
-  rcases Nat.of_le_succ hmn with hc | hc
-  exact le_trans (hi hc) (maxOfSums_succ_le T φ x n)
-  rw [hc]
+  · rw [Nat.le_zero.mp hmn]
+  · rcases Nat.of_le_succ hmn with hc | hc
+    . exact le_trans (hi hc) (maxOfSums_succ_le T φ x n)
+    . rw [hc]
 
 /-- `maxOfSums` is monotone.
 (Uncertain which is the best phrasing to keep of these options.) -/
-theorem maxOfSums_Monotone (x : α) : Monotone (fun n ↦ maxOfSums T φ x n) := by
-  unfold Monotone
-  intros n m hmn
-  exact maxOfSums_le_le T φ x n m hmn
+theorem maxOfSums_Monotone (x : α) : Monotone (fun n ↦ maxOfSums T φ x n) :=
+  maxOfSums_le_le T φ x
 
 open Filter in
-/-- The set of divergent points `{ x | lim_n Φ_n x = ∞}`. -/
+/-- The set of divergent points `{ x | lim_n Φ_{n+1} x = ∞}`. -/
 def divSet := { x : α | Tendsto (fun n ↦ maxOfSums T φ x n) atTop atTop }
 
-open Finset in
--- Marco is working on this
-lemma maxOfSums_measurable : ∀ n, Measurable (fun x ↦ maxOfSums T φ x n) := by
-  sorry
 
+@[measurability]
+lemma birkhoffSum_measurable :
+    Measurable (birkhoffSum T φ n) := by
+  apply Finset.measurable_sum
+  intro i hi
+  simp only [Finset.mem_range] at hi
+  exact Measurable.comp' hphim (Measurable.iterate hT.measurable _)
+
+@[measurability]
+lemma maxOfSums_measurable :
+  ∀ n : ℕ , Measurable (fun x ↦ maxOfSums T φ x n) := by
+  intro n
+  induction n
+  case zero := by
+    simp only [maxOfSums_zero]
+    exact hphim
+  case succ n hn := by
+    unfold maxOfSums
+    simp only [partialSups_succ]
+    exact Measurable.sup' hn (birkhoffSum_measurable _ hT _ hphim)
 
 /- can probably be stated without the '[m0]' part -/
-lemma divSet_neasurable : MeasurableSet[m0] (divSet T φ) := by sorry
-/-
-For the above lemma we need to use that the set A, defined by all x s.t.
-lim_n φ_n = ∞ is m0-measurable. Since φ is measurable (b/c integrable)
-it all boils down to understanding what Lean means with φ : α → ℝ being
-measurable, that is, wrt to what sigma-algebra in ℝ. Since ℝ is ℝ, Lean
-might assume it's wrt the Lebesgue measurable sets. In this case, we're
-good. Of course we still need to find a lemma in mathlib that says that
-the "counterimage of ∞ is measurable". Note that the lemma can't say
-exactly that becuase φ takes values in ℝ and not in ENNReal (in which
-case we might have had a chance).
-In any case, if we don't find such lemma, I can easily produce it.
--/
-
+/-- `divSet T φ` is a measurable set -/
+lemma divSet_measurable : MeasurableSet[m0] (divSet T φ) := by
+  simp only [divSet]
+  exact measurableSet_tendsto Filter.atTop (maxOfSums_measurable _ hT _ hphim)
 
 /- ∀ `x ∈ A`, `Φ_{n+1}(x) - Φ_{n}(T(x)) = φ(x) - min(0,Φ_{n}(T(x))) ≥ φ(x)` decreases to `φ(x)`. -/
 
 /-- Convenient combination of `birkhoffSum` terms. -/
 theorem birkhoffSum_succ_image (n : ℕ) (x : α) :
       birkhoffSum T φ n (T x) = birkhoffSum T φ (n + 1) x - φ x := by
-    rw [birkhoffSum_add T φ n 1 x]
-    rw [eq_add_of_sub_eq' (birkhoffSum_apply_sub_birkhoffSum T φ n x)]
-    simp
-    exact add_sub (birkhoffSum T φ n x) (φ (T^[n] x)) (φ x)
+    simp [birkhoffSum_add T φ n 1 x, eq_add_of_sub_eq' (birkhoffSum_apply_sub_birkhoffSum T φ n x),
+      birkhoffSum_one', add_sub (birkhoffSum T φ n x) (φ (T^[n] x)) (φ x)]
 
 /- Would expect this to be in `Mathlib/Data/Finset/Lattice`.
 Or perhaps there is already an easier way to extract it from mathlib? -/
 theorem sup'_eq_iff_le {s : Finset β} [SemilatticeSup α] (H : s.Nonempty) (f : β → α) (hs : a ∈ s) :
-    s.sup' H f = f a ↔ ∀ b ∈ s, f b ≤ f a := by
-  constructor
-  · intros h0 b h2
-    rw [← h0]
-    exact Finset.le_sup' f h2
-  · intro h1
-    have hle : s.sup' H f ≤ f a := by
-      simp only [Finset.sup'_le_iff]
-      exact h1
-    exact (LE.le.ge_iff_eq hle).mp (Finset.le_sup' f hs)
+    s.sup' H f = f a ↔ ∀ b ∈ s, f b ≤ f a := ⟨fun h0 b h2 ↦ (h0 ▸ Finset.le_sup' f h2),
+    fun h1 ↦ (LE.le.ge_iff_eq (by simp [Finset.sup'_le_iff]; exact h1)).mp (Finset.le_sup' f hs)⟩
 
 /- convenient because used several times in proving claim 1 -/
 theorem map_range_Nonempty (n : ℕ) : (Finset.map (addLeftEmbedding 1)
-    (Finset.range (n + 1))).Nonempty := by
-  use 1
-  refine Finset.mem_map.mpr ?h.a
-  use 0
-  constructor
-  · simp only [Finset.mem_range, add_pos_iff, zero_lt_one, or_true]
-  · exact rfl
+    (Finset.range (n + 1))).Nonempty := by simp
 
 open Finset in
 /-- modified from mathlib to make f explicit - isn't the version in mathlib inconvenient? -/
@@ -217,8 +195,7 @@ theorem claim1 (n : ℕ) (x : α) :
         (sup' (map (addLeftEmbedding 1) (range (n + 1))) (map_range_Nonempty n)
         fun k ↦ birkhoffSum T φ (k + 1) x) := by
       unfold maxOfSums
-      rw [h1]
-      simp
+      simp_rw [partialSups_eq_sup'_range, h1]
       exact rfl
     have h3 := max_choice (birkhoffSum T φ 1 x)
       (sup' (map (addLeftEmbedding 1) (range (n + 1))) (map_range_Nonempty n)
@@ -235,8 +212,9 @@ theorem claim1 (n : ℕ) (x : α) :
     simp
     refine' h11.mp _
     unfold maxOfSums at hcl
-    simp at hcl
-    exact hcl
+    rw [partialSups_eq_sup'_range] at hcl
+    rw [hcl]
+    simp only [birkhoffSum_one']
   have h1 : birkhoffSum T φ 1 x = φ x := birkhoffSum_one T φ x
   have h2 : ∀ k, birkhoffSum T φ k (T x) = birkhoffSum T φ (k + 1) x - φ x := by
     intro k
@@ -250,6 +228,7 @@ theorem claim1 (n : ℕ) (x : α) :
     exact h35 k (mem_range_succ_iff.mpr hk)
   have h4 : maxOfSums T φ (T x) n ≤ 0 := by
     unfold maxOfSums
+    rw [partialSups_eq_sup'_range]
     simp only [sup'_le_iff, mem_range]
     intros k hk
     rw [Nat.lt_succ] at hk
@@ -269,19 +248,19 @@ theorem claim1 (n : ℕ) (x : α) :
     simp at h7
     simp at h5
     simp_rw [← h7] at h5
-    simp_rw [← h5, add_comm]
+    simp_rw [partialSups_eq_sup'_range, ← h5, add_comm]
   -- in this case the min is zero
   have h8 : 0 ≤ maxOfSums T φ (T x) n := by
     have h9 : φ x ≤ maxOfSums T φ x (n + 1) := by
       unfold maxOfSums
       have h41 : 0 ∈ (range (n + 1 + 1)) := mem_range.mpr (Nat.add_pos_right (n + 1) Nat.le.refl)
       have h10 := le_sup' (fun k ↦ birkhoffSum T φ (k + 1) x) h41
       simp at h10
+      rw [partialSups_eq_sup'_range]
       norm_num
       exact h10
     linarith
-  rw [min_eq_left h8, h1]
-  simp
+  simp [min_eq_left h8, h1]
 
 open Filter in
 /-- Eventual equality - variant with assumption on `T x`. -/
@@ -354,7 +333,7 @@ theorem divSet_inv : T⁻¹' (divSet T φ) = (divSet T φ) := by
   · intro hx
     have h2' : ∀ᶠ n in atTop, maxOfSums T φ (T x) n = maxOfSums T φ x (n + 1) - φ x := by
       -- there should be a slicker way of rearranging the equality in Tendsto ------------------
-      simp
+      simp only [eventually_atTop, ge_iff_le]
       have h2 := diff_evenutally_of_divSet' T φ x hx
       simp at h2
       obtain ⟨k, hk⟩ := h2
@@ -364,18 +343,17 @@ theorem divSet_inv : T⁻¹' (divSet T φ) = (divSet T φ) := by
       exact hk n hn
       ------------------------------------------------------------------------------------------
     -- use the eventual equality
-    have h5 : Tendsto (fun n ↦ maxOfSums T φ x (n + 1) - φ x) atTop atTop := by
-      exact Tendsto.congr' h2' hx
+    have h5 : Tendsto (fun n ↦ maxOfSums T φ x (n + 1) - φ x) atTop atTop := Tendsto.congr' h2' hx
     -- rearrange using properties of `Tendsto`
     have h6 : Tendsto (fun n ↦ maxOfSums T φ x (n + 1)) atTop atTop := by
       have h7 := tendsto_atTop_add_const_right atTop (φ x) h5
-      simp at h7
+      simp only [sub_add_cancel] at h7
       exact h7
     refine' (tendsto_add_atTop_iff_nat 1).mp _
     exact h6
   · intro hx
-    have hx' : Tendsto (fun n ↦ maxOfSums T φ x (n + 1)) atTop atTop := by
-      exact (tendsto_add_atTop_iff_nat 1).mpr hx
+    have hx' : Tendsto (fun n ↦ maxOfSums T φ x (n + 1)) atTop atTop :=
+      (tendsto_add_atTop_iff_nat 1).mpr hx
     -- eventually we have a precise equality between the two maxOfSums
     have h2' : ∀ᶠ n in atTop, maxOfSums T φ x (n + 1) - φ x = maxOfSums T φ (T x) n := by
       -- there should be a slicker way of rearranging the equality in Tendsto ------------------
@@ -392,10 +370,9 @@ theorem divSet_inv : T⁻¹' (divSet T φ) = (divSet T φ) := by
 
 /-- Framed formula: the negative difference of maxOfSums is monotone. -/
 theorem diff_Monotone (x : α) : Monotone (fun n ↦ -(maxOfSums T φ x (n + 1) - maxOfSums T φ (T x) n)) := by
-  unfold Monotone
-  intros n m hnm
-  simp_rw [claim1]
-  simp
+  intro n m hnm
+  simp only [claim1, neg_sub, tsub_le_iff_right, sub_add_cancel, le_min_iff, min_le_iff, le_refl,
+    true_or, true_and]
   by_cases hc : 0 ≤ maxOfSums T φ (T x) m
   · left
     exact hc
@@ -405,14 +382,14 @@ theorem diff_Monotone (x : α) : Monotone (fun n ↦ -(maxOfSums T φ x (n + 1)
 open Filter in
 /-- ✨ Outside the divergent set the limsup of Birkhoff average is non positive. -/
 theorem non_positive_of_notin_divSet (x : α) (hx : x ∉ divSet T φ) :
-    limsup (fun n ↦ (birkhoffAverage R T φ n x)) ≤ 0 := by
+    limsup (fun n ↦ (birkhoffSum T φ n x)) ≤ 0 := by
   /- By `hx` we know that `n ↦ birkhoffSum T φ n x` is bounded. Conclude dividing by `n`. -/
+  have h0 : ∀ n, 0 ≥  birkhoffAverage ℝ T φ n x := by
+    intro n
+    unfold birkhoffAverage
+    sorry
   sorry
 
-/-- `divSet T φ` is a measurable set -/
-theorem divSet_MeasurableSet : MeasurableSet (divSet T φ) := by
-  /- ? -/
-  sorry
 
 open Filter Topology Measure in
 /-- The integral of an observable over the divergent set is nonnegative. -/
@@ -423,7 +400,7 @@ theorem integral_nonneg : 0 ≤ ∫ x in (divSet T φ), φ x ∂μ := by
       intros x hx
       have h00 := maxOfSums_Monotone T φ x hn
       linarith
-    exact setIntegral_nonneg (divSet_MeasurableSet T φ) h01
+    exact setIntegral_nonneg (divSet_measurable T hT φ hphim) h01
   have h1 (n : ℕ) : ∫ x in (divSet T φ), (maxOfSums T φ x (n + 1) - maxOfSums T φ x n) ∂μ =
       ∫ x in (divSet T φ), (maxOfSums T φ x (n + 1) - maxOfSums T φ (T x) n) ∂μ := by
     have h10 : ∫ x in (divSet T φ), (maxOfSums T φ x n) ∂μ =
@@ -474,8 +451,8 @@ theorem integral_nonneg : 0 ≤ ∫ x in (divSet T φ), φ x ∂μ := by
 
 /- If `x ∉ A`, `limsup_n (1/n) ∑_{k=0}^{n-1} φ ∘ T^i ≤ 0`. -/
 
-/- If conditional expectation of `φ` is negative, i.e., `∫_C φ dμ = ∫_C φ|_inv_sigmal_algebra dμ < 0` for all `C` in `inv_sigma_algebra` with `μ(C) > 0`,
-then `μ(A) = 0`. -/
+/- If conditional expectation of `φ` is negative, i.e., `∫_C φ dμ = ∫_C φ|_inv_sigmal_algebra dμ < 0`
+for all `C` in `inv_sigma_algebra` with `μ(C) > 0`, then `μ(A) = 0`. -/
 
 /- Then (assumptions as prior step) `limsup_n (1/n) ∑_{k=0}^{n-1} φ ∘ T^i ≤ 0` a.e. -/
 
@@ -487,7 +464,8 @@ then `μ(A) = 0`. -/
 
 /- Replacing `f` with `-f`  we get the lower bound. -/
 
-/- Birkhoff's theorem: Almost surely, `birkhoffAverage ℝ f g n x` converges to the conditional expectation of `f`. -/
+/- Birkhoff's theorem: Almost surely, `birkhoffAverage ℝ f g n x` converges to the conditional
+expectation of `f`. -/
 
 /- If `T` is ergodic, show that the invariant sigma-algebra is a.e. trivial. -/