refactor the file

Author: lua-vr

Mathlib/Data/EReal/Basic.lean

@@ -337,6 +337,10 @@ protected theorem coe_pos {x : ℝ} : (0 : EReal) < x ↔ 0 < x :=
 protected theorem coe_neg' {x : ℝ} : (x : EReal) < 0 ↔ x < 0 :=
   EReal.coe_lt_coe_iff
 
+@[simp, norm_cast]
+theorem coe_max (x y : ℝ) : (↑(max x y) : EReal) = max ↑x ↑y :=
+  rfl
+
 lemma toReal_eq_zero_iff {x : EReal} : x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥ := by
   cases x <;> norm_num
 

Mathlib/Dynamics/BirkhoffSum/Maximal.lean

@@ -12,98 +12,88 @@ import Mathlib.Algebra.Order.Ring.Star
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.RCLike.Lemmas
 import Mathlib.Data.Real.StarOrdered
-import Mathlib.Dynamics.BirkhoffSum.Average
+public import Mathlib.Dynamics.BirkhoffSum.Average
 
 /-!
 # Maximal ergodic theorem.
 
-We define the set `birkhoffAverageSupSet f g a` of points `x` where the supremum of
-`birkhoffAverage ℝ f g n x` for varying `n` is greater than `a`. Then, we show its
-measure multiplied by `a` is bounded above by the integral of `g` on this set. In particular,
-for a positive `g`, this integral is bounded above by the `L1` norm of `g`, so for `g`
-taking values in a `NormedAddCommGroup`, we get an inequality involving the norm.
+We prove the maximal ergodic theorem for a measure-preserving map `f` and an integrable function
+`g`. The maximal ergodic operator `birkhoffAverageSup f g x` is defined as the supremum of the
+Birkhoff averages of `g` over all `n`. Moreover, we show some results about the auxiliary definition
+`birkhoffMax f g n`, defined as the maximum of the Birkhoff sums ranging between `0` and `n`.
 
 ## Main results
 
-* `meas_birkhoffAverageSupSet_smul_const_le_integral`: the measure of `birkhoffAverageSupSet f g a`
-   multiplied by `a` is bounded above by the integral of `g` on the same set.
-* `meas_birkhoffAverageSupSet_smul_const_le_norm`: the measure of `birkhoffAverageSupSet f ‖g‖ a`
-   multiplied by `a` is bounded above by the `L1` norm of `g`.
+* `distribution_birkhoffAverageSup_le_integral`: the cumulative distribution function of
+  `birkhoffAverageSup` at `a` is less than or equal to the integral of `g` on the set where
+  `a < birkhoffAverageSup f g x`.
+* `iSup_distribution_birkhoffAverageSup_le_norm`: the operator `birkhoffAverageSup` satisfies a
+   weak-type inequality.
 -/
 
-variable {α : Type*} {f : α → α}
-
 open MeasureTheory Measure MeasurableSpace Filter Topology
 
-section BirkhoffMax
+variable {α M : Type*} {f : α → α} {g : α → M} {n : ℕ} {x : α}
+
+@[expose]
+public section BirkhoffMax
 
 /-- The maximum of `birkhoffSum f g i` for `i` ranging from `0` to `n`. -/
-def birkhoffMax (f : α → α) (g : α → ℝ) : ℕ →o (α → ℝ) :=
+def birkhoffMax [AddCommMonoid M] [SemilatticeSup M]
+    (f : α → α) (g : α → M) : ℕ →o (α → M) :=
   partialSups (birkhoffSum f g)
 
-lemma birkhoffMax_nonneg {g n} :
-    0 ≤ birkhoffMax f g n := by
-  apply (le_partialSups_of_le _ n.zero_le).trans'
-  rfl
-
-lemma birkhoffMax_succ {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]
-
-lemma birkhoffMax_succ' {g n x} (hpos : 0 < birkhoffMax f g (n + 1) x) :
+lemma birkhoffMax_nonneg [AddCommMonoid M] [SemilatticeSup M] : 0 ≤ birkhoffMax f g n x :=
+  (birkhoffMax ..).mono n.zero_le x
+
+variable [AddCommGroup M]
+
+variable [SemilatticeSup M] [IsOrderedAddMonoid M] in
+lemma birkhoffMax_succ :
+    birkhoffMax f g (n + 1) x = 0 ⊔ (g x + birkhoffMax f g n (f x)) := by
+  have : birkhoffSum f g ∘ (· + 1) = (g + birkhoffSum f g · ∘ f) :=
+    funext₂ <| fun k x ↦ birkhoffSum_succ' ..
+  rw [birkhoffMax, partialSups_add_one', this, partialSups_const_add]
+  simp [partialSups]
+
+variable [LinearOrder M] [IsOrderedAddMonoid M]
+
+lemma birkhoffMax_succ' (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 {g n} :
-    birkhoffMax f g n ≤ birkhoffMax f g (n + 1) := by
-  gcongr
-  exact n.le_succ
-
-lemma birkhoffMax_le_birkhoffMax {g n x} (hpos : 0 < birkhoffMax f g n x) :
+  rw [birkhoffMax_succ, birkhoffMax, lt_sup_iff] at hpos
+  rcases hpos with h | h
+  · grind
+  · rw [birkhoffMax_succ, birkhoffMax, sup_of_le_right h.le]
+
+lemma birkhoffMax_le_self_add_comp (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)
+  rcases n with _ | n
+  · simp [birkhoffMax] at *
+  · apply le_of_eq_of_le (birkhoffMax_succ' hpos)
     apply add_le_add_right
-    exact birkhoffMax_comp_le_succ (f x)
+    apply birkhoffMax f g |>.mono (by omega)
 
-lemma birkhoffMax_pos_of_mem_support {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
+end BirkhoffMax
+
+variable {g : α → ℝ}
 
 -- TODO: move elsewhere
 @[fun_prop]
-lemma birkhoffSum_measurable [MeasurableSpace α] {f : α → α} (hf : Measurable f) {g : α → ℝ}
-    (hg : Measurable g) {n} : Measurable (birkhoffSum f g n) := by
+public lemma birkhoffSum_measurable [MeasurableSpace α] (hf : Measurable f) (hg : Measurable g) :
+    Measurable (birkhoffSum f g n) := by
   apply Finset.measurable_sum
   measurability
 
--- TODO: move elsewhere
 @[fun_prop]
-lemma birkhoffMax_measurable [MeasurableSpace α] (hf : Measurable f) {g : α → ℝ}
-    (hg : Measurable g) {n} : Measurable (birkhoffMax f g n) := by
+public lemma birkhoffMax_measurable [MeasurableSpace α] (hf : Measurable f) (hg : Measurable g) :
+    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 μ)
+variable [MeasurableSpace α] (μ : Measure α := by volume_tac) (hf : MeasurePreserving f μ μ)
+  (hg : Integrable g μ)
 
 include hf
 
@@ -112,9 +102,8 @@ include hf
 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)
+  exact fun i _ ↦ hg.comp_measurePreserving (hf.iterate i)
 
--- todo: move elsewhere
 @[fun_prop]
 lemma birkhoffMax_aestronglyMeasurable (hg : AEStronglyMeasurable g μ) :
     AEStronglyMeasurable (birkhoffMax f g n) μ := by
@@ -127,7 +116,6 @@ include hg
 lemma birkhoffSum_integrable : Integrable (birkhoffSum f g n) μ :=
   integrable_finsetSum _ fun _ _ ↦ (hf.iterate _).integrable_comp_of_integrable hg
 
--- todo: move elsewhere
 lemma birkhoffMax_integrable : Integrable (birkhoffMax f g n) μ := by
   unfold birkhoffMax
   induction n with
@@ -145,17 +133,19 @@ lemma birkhoffMax_integral_le :
     · 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)
+      rw [Function.mem_support] at hx
+      apply birkhoffMax_le_self_add_comp
+      exact birkhoffMax_nonneg |>.lt_of_ne hx.symm
   · exact this.restrict
 
-lemma setIntegral_nonneg_on_birkhoffMax_support :
+lemma setIntegral_birkhoffMax_support_nonneg :
     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))
+      exact integral_nonneg (fun x ↦ birkhoffMax_nonneg)
     _ = ∫ 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₃
@@ -168,58 +158,56 @@ lemma setIntegral_nonneg_on_birkhoffMax_support :
 
 end MeasurePreserving
 
-end BirkhoffMax
+noncomputable section BirkhoffSup
+
+def birkhoffSumSup (f : α → α) (g : α → ℝ) (x : α) : EReal :=
+  ⨆ n, ↑(birkhoffSum f g n x)
+
+lemma birkhoffSumSup_eq_iSup_birkhoffMax :
+    birkhoffSumSup f g x = ⨆ n, ↑(birkhoffMax f g n x) := by
+  simp [birkhoffMax, Pi.partialSups_apply, ←map_partialSups' EReal.coe_max, birkhoffSumSup]
 
-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 (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 exists_partialSups_eq (birkhoffSum f g · x) n with ⟨m, _, hm₂⟩
-      exact ⟨m, hm₂ ▸ h⟩
-
-/-- The set of `x` for which `birkhoffAverage ℝ f g n x` greater than some `a`
-for at least one value of `n`. -/
-public 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) :
+@[expose]
+public def birkhoffAverageSup (f : α → α) (g : α → ℝ) (x : α) : EReal :=
+  ⨆ n, ↑(birkhoffAverage ℝ f g n x)
+
+end BirkhoffSup
+
+lemma setOf_birkhoffSumSup_pos_eq_iUnion_birkhoffMax_support :
+    {x | 0 < birkhoffSumSup f g x} = ⋃ n : ℕ, (birkhoffMax f g n).support := by
+  simp_rw [birkhoffSumSup_eq_iSup_birkhoffMax, lt_iSup_iff, Set.setOf_exists, EReal.coe_pos,
+    birkhoffMax_nonneg.lt_iff_ne, Function.support, ne_comm]
+
+theorem lt_birkhoffAverage_iff_lt_birkhoffSum {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 positivity)]
   rw [smul_zero, ←birkhoffAverage, birkhoffAverage_sub]
   simp only [Pi.sub_apply, sub_pos]
   nth_rw 2 [birkhoffAverage_of_comp_eq _ rfl (by positivity)]
 
-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
-    rcases n
-    · 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
-    · exact birkhoffAverage_iff_birkhoffSum (by positivity)
-  simp_rw [this]
+theorem lt_birkhoffAverageSup_iff_lt_birkhoffSumSup {a : ℝ} (ha : 0 < a) :
+    a < birkhoffAverageSup f g x ↔ 0 < birkhoffSumSup f (g - fun _ ↦ a) x := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · have ⟨n, hn⟩ := lt_iSup_iff.mp h
+    apply lt_iSup_iff.mpr (.intro n _)
+    norm_cast at *
+    rwa [←lt_birkhoffAverage_iff_lt_birkhoffSum]
+    by_contra!
+    apply Nat.eq_zero_of_le_zero at this
+    simp only [this, birkhoffAverage_zero'] at hn
+    exact lt_asymm hn ha
+  · have ⟨n, hn⟩ := lt_iSup_iff.mp h
+    apply lt_iSup_iff.mpr (.intro n _)
+    norm_cast at *
+    rwa [lt_birkhoffAverage_iff_lt_birkhoffSum]
+    by_contra!
+    apply Nat.eq_zero_of_le_zero at this
+    simp only [this, birkhoffSum_zero'] at hn
+    exact lt_irrefl 0 hn
 
 section MeasurePreserving
 
-variable {f : α → α} [MeasurableSpace α] (μ : Measure α := by volume_tac) {n}
+variable {f : α → α} [MeasurableSpace α] (μ : Measure α := by volume_tac)
   (hf : MeasurePreserving f μ μ)
 
 include hf
@@ -230,42 +218,40 @@ variable {g : α → ℝ} (hg : Integrable g μ)
 
 include hg
 
-lemma tendsto_setIntegral_on_birkhoffMax_support_birkhoffSupSet :
+lemma tendsto_setIntegral_birkhoffMax_support :
     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]
+    (𝓝 <| ∫ x in {x | 0 < birkhoffSumSup f g x}, g x ∂ μ) := by
+  rw [setOf_birkhoffSumSup_pos_eq_iUnion_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]
-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)
+    grind [birkhoffMax_nonneg, (birkhoffMax f g).mono hij x, Function.mem_support]
+
+theorem setIntegral_birkhoffSumSup_nonneg :
+    0 ≤ ∫ x in {x | 0 < birkhoffSumSup f g x}, g x ∂μ := by
+  apply ge_of_tendsto' (tendsto_setIntegral_birkhoffMax_support μ hf hg)
   intro n
-  exact setIntegral_nonneg_on_birkhoffMax_support μ hf hg
+  exact setIntegral_birkhoffMax_support_nonneg μ hf hg
 
 variable [IsFiniteMeasure μ]
 
-/-- The measure of the set where the supremum of the Birkhoff averages of `g` is greater than `a`,
-multiplied by `a`, is bounded above by the integral of `g` on this set. -/
-public theorem meas_birkhoffAverageSupSet_smul_const_le_integral (a : ℝ) (ha : 0 < a) :
-    a * μ.real (birkhoffAverageSupSet f g a) ≤ ∫ x in birkhoffAverageSupSet f g a, g x ∂μ := by
+/-- The cumulative distribution function of `birkhoffAverageSup` at `a` is less than or equal to the
+integral of `g` on the set where `a < birkhoffAverageSup f g x`. -/
+public theorem distribution_birkhoffAverageSup_le_integral (a : ℝ) (ha : 0 < a) :
+    a * μ.real {x | a < birkhoffAverageSup f g x}
+    ≤ ∫ x in {x | a < birkhoffAverageSup f g x}, g x ∂μ := by
   have p₁ := Integrable.sub hg (integrable_const a)
   calc
-    _ = ∫ x in birkhoffSupSet f (g - fun _ ↦ a), a ∂μ := by
-      simp [birkhoffAverageSupSet_eq_birkhoffSupSet ha]
+    _ = ∫ x in {x | 0 < birkhoffSumSup f (g - fun _ ↦ a) x}, a ∂μ := by
+      simp [lt_birkhoffAverageSup_iff_lt_birkhoffSumSup ha]
       ring
-    _ ≤ ∫ 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
-        ring
-      · exact (integrable_const a).restrict
+    _ ≤ ∫ x in {x | 0 < birkhoffSumSup f (g - fun _ ↦ a) x}, a ∂μ +
+        ∫ x in {x | 0 < birkhoffSumSup f (g - fun _ ↦ a) x}, g x - a ∂μ := by
+      exact le_add_of_nonneg_right (setIntegral_birkhoffSumSup_nonneg μ hf p₁)
+    _ = ∫ x in {x | a < birkhoffAverageSup f g x}, g x ∂μ := by
+      rw [←integral_add (integrable_const a).restrict]
+      · simp [lt_birkhoffAverageSup_iff_lt_birkhoffSumSup ha]
       · exact p₁.restrict
 
 end Real
@@ -276,16 +262,16 @@ variable {E : Type*} [NormedAddCommGroup E] {g : α → E} (hg : Integrable g μ
 
 include hg
 
-/-- Maximal ergodic theorem: the maximal ergodic operator satisfies a weak-type inequality. -/
-public theorem meas_birkhoffAverageSupSet_smul_const_le_norm :
-    ⨆ a, a * μ.real (birkhoffAverageSupSet f (fun x ↦ ‖g x‖) a) ≤ ∫ x, ‖g x‖ ∂μ := by
+/-- Maximal ergodic theorem: the operator `birkhoffAverageSup` satisfies a weak-type inequality. -/
+public theorem iSup_distribution_birkhoffAverageSup_le_norm :
+    ⨆ a : ℝ, a * μ.real {x | a < birkhoffAverageSup f (‖g ·‖) x} ≤ ∫ x, ‖g x‖ ∂μ := by
   refine ciSup_le fun a ↦ ?_
   by_cases! ha : 0 < a; swap
   · apply mul_nonpos_of_nonpos_of_nonneg ha measureReal_nonneg |>.trans
     exact integral_nonneg (fun _ ↦ norm_nonneg _)
   calc
-    _ ≤ ∫ x in birkhoffAverageSupSet f (fun x ↦ ‖g x‖) a, ‖g x‖ ∂μ := by
-      exact meas_birkhoffAverageSupSet_smul_const_le_integral μ hf hg.norm a ha
+    _ ≤ ∫ x in {x | a < birkhoffAverageSup f (‖g ·‖) x}, ‖g x‖ ∂μ := by
+      exact distribution_birkhoffAverageSup_le_integral μ hf hg.norm a ha
     _ ≤ ∫ x, ‖g x‖ ∂μ := by
       exact setIntegral_le_integral hg.norm (ae_of_all _ (norm_nonneg <| g ·))