complete proof of maximal inequality

Author: lua-vr

Mathlib/Dynamics/BirkhoffSum/Pointwise.lean

@@ -190,7 +190,8 @@ end PR
 
 section BirkhoffSup
 
-def birkhoffSupSet (f : α → α) (g : α → ℝ) : Set α := {x | ∃ n : ℕ, 0 < birkhoffSum f g n x}
+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
@@ -210,12 +211,42 @@ lemma birkhoffSupSet_eq_iSup_birkhoffMax_support {f : α → α} {g : α → ℝ
       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) {g : α → ℝ} {n}
-  (hf : MeasurePreserving f μ μ) (hg : Integrable g μ)
+variable {f : α → α} [MeasurableSpace α] (μ : Measure α := by volume_tac) {n}
+  (hf : MeasurePreserving f μ μ)
 
-include hf hg
+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
@@ -239,25 +270,39 @@ theorem setIntegral_nonneg_on_birkhoffSupSet :
   intro n
   exact setIntegral_nonneg_on_birkhoffMax_support μ hf hg
 
-def birkhoffAverageSupSet (f : α → α) (g : α → ℝ) (a : ℝ) : Set α :=
-  {x | ∃ n : ℕ, a < birkhoffAverage ℝ f g n x}
+variable [IsFiniteMeasure μ]
 
-theorem birkhoffAverageSupSet_eq_birkhoffSupSet {x} {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 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 μ]
 
-theorem setIntegral_nonneg_on_birkhoffSupSet' [IsFiniteMeasure μ] (a : ℝ) :
-    μ.real (birkhoffSupSet f g) • a ≤ ∫ x in birkhoffSupSet f g, g x ∂μ := by
+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 birkhoffSupSet f g, a ∂μ := by rw [setIntegral_const]
-    _ ≤ ∫ x in birkhoffSupSet f g, a ∂μ + ∫ (x : α) in birkhoffSupSet f g, g x ∂μ := by sorry
+    _ ≤ ∫ 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 ·))
 
-theorem setIntegral_nonneg_on_birkhoffSupSet'' (a : ℝ) :
-    a * μ.real (birkhoffSupSet f g) ≤ ‖hg.toL1‖ := by
-  sorry
+end NormedAddCommGroup
 
 end MeasurePreserving
 
@@ -268,7 +313,4 @@ noncomputable section BirkhoffAverage
 variable {f : α → α} [MeasurableSpace α] (μ : Measure α := by volume_tac) {g : α → ℝ} {n}
   (hf : MeasurePreserving f μ μ) (hg : Integrable g μ)
 
-def birkhoffOscillation (f : α → α) (g : α → ℝ) (x : α) : ℝ :=
-  limsup (birkhoffAverage ℝ f g · x) atTop - liminf (birkhoffAverage ℝ f g · x) atTop
-
 end BirkhoffAverage