diff --git a/BET/Birkhoff.lean b/BET/Birkhoff.lean index 977f79b..7676f1b 100644 --- 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,7 +248,7 @@ 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 @@ -277,11 +256,11 @@ theorem claim1 (n : ℕ) (x : α) : 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. -/