pointwise birkhoff theorem

Author: lua-vr

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -655,11 +655,11 @@ theorem integrable_of_bounded_and_ae_continuousWithinAt [CompleteSpace E] {I : B
      centered at x is ≤ ε₁ -/
   have comp : IsCompact (Box.Icc I \ U) :=
     I.isCompact_Icc.of_isClosed_subset (I.isCompact_Icc.isClosed.sdiff Uopen) Set.diff_subset
-  have : ∀ x ∈ (Box.Icc I \ U), oscillationWithin f (Box.Icc I) x < (ENNReal.ofReal ε₁) := by
+  have : ∀ x ∈ (Box.Icc I \ U), oscillationWithinAt f (Box.Icc I) x < (ENNReal.ofReal ε₁) := by
     intro x hx
-    suffices oscillationWithin f (Box.Icc I) x = 0 by rw [this]; exact ofReal_pos.2 ε₁0
-    simpa [OscillationWithin.eq_zero_iff_continuousWithinAt, D, hx.1] using hx.2 ∘ (fun a ↦ UD a)
-  rcases comp.uniform_oscillationWithin this with ⟨r, r0, hr⟩
+    suffices oscillationWithinAt f (Box.Icc I) x = 0 by rw [this]; exact ofReal_pos.2 ε₁0
+    simpa [OscillationWithinAt.eq_zero_iff_continuousWithinAt, D, hx.1] using hx.2 ∘ (fun a ↦ UD a)
+  rcases comp.uniform_oscillationWithinAt this with ⟨r, r0, hr⟩
   /- We prove the claim for partitions π₁ and π₂ subordinate to r/2, by writing the difference as
      an integralSum over π₁ ⊓ π₂ and considering separately the boxes of π₁ ⊓ π₂ which are/aren't
      fully contained within U. -/

Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

@@ -23,7 +23,18 @@ see `ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection`.
 
 public section
 
-open Filter Finset Function Bornology
+namespace Module.End
+
+variable {R M F : Type*} [Semiring R] [AddCommGroup M] [Module R M]
+  [FunLike F M M] [One F] [LinearMapClass F R M M]
+
+abbrev fixedPoints (f : F) : Submodule R M := LinearMap.eqLocus f 1
+
+abbrev coboundaries (f : F) : Submodule R M := (f - 1 : M →ₗ[R] M).range
+
+end Module.End
+
+open Filter Set Function Bornology Module
 open scoped Topology
 
 variable {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E]
@@ -45,9 +56,9 @@ I chose to do it in order to isolate parts of the proof that do not rely
 on the inner product space structure.
 -/
 theorem LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure [NormedSpace 𝕜 E]
-    (f : E →ₗ[𝕜] E) (hf : LipschitzWith 1 f) (g : E →L[𝕜] LinearMap.eqLocus f 1)
-    (hg_proj : ∀ x : LinearMap.eqLocus f 1, g x = x)
-    (hg_ker : (g.ker : Set E) ⊆ closure (LinearMap.range (f - 1))) (x : E) :
+    (f : E →ₗ[𝕜] E) (hf : LipschitzWith 1 f) (g : E →L[𝕜] End.fixedPoints f)
+    (hg_proj : ∀ x : End.fixedPoints f, g x = x)
+    (hg_ker : g.ker ≤ (End.coboundaries f).topologicalClosure) (x : E) :
     Tendsto (birkhoffAverage 𝕜 f _root_.id · x) atTop (𝓝 (g x)) := by
   /- Any point can be represented as a sum of `y ∈ LinearMap.ker g` and a fixed point `z`. -/
   obtain ⟨y, hy, z, hz, rfl⟩ : ∃ y, g y = 0 ∧ ∃ z, IsFixedPt f z ∧ x = y + z :=
@@ -59,7 +70,7 @@ theorem LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure [NormedSpace 
     simpa [hy, hgz, birkhoffAverage, birkhoffSum, Finset.sum_add_distrib, smul_add]
       using this.add (hz.tendsto_birkhoffAverage 𝕜 _root_.id)
   /- By continuity, it suffices to prove the theorem on a dense subset of `LinearMap.ker g`.
-  By assumption, `LinearMap.range (f - 1)` is dense in the kernel of `g`,
+  By assumption, `f.coboundaries` is dense in the kernel of `g`,
   so it suffices to prove the theorem for `y = f x - x`. -/
   have : IsClosed {x | Tendsto (birkhoffAverage 𝕜 f _root_.id · x) atTop (𝓝 0)} :=
     isClosed_setOf_tendsto_birkhoffAverage 𝕜 hf uniformContinuous_id continuous_const
@@ -78,6 +89,31 @@ variable [InnerProductSpace 𝕜 E] [CompleteSpace E]
 
 local notation "⟪" x ", " y "⟫" => inner 𝕜 x y
 
+open Submodule
+
+/-- The closure of the coboundaries of the form `f x - x` contains the orthogonal complement of the
+fixed points of `f`.
+-/
+theorem eqLocus_orthogonal_le_topologicalClosure_coboundary (f : E →L[𝕜] E) (hf : ‖f‖ ≤ 1) :
+    (End.fixedPoints f)ᗮ ≤ (End.coboundaries f).topologicalClosure := by
+  /- In other words, we need to verify that any vector that is orthogonal to the range of `f - 1`
+  is a fixed point of `f`. -/
+  rw [← Submodule.orthogonal_orthogonal_eq_closure]
+  /- To verify this, we verify `‖f x‖ ≤ ‖x‖` (because `‖f‖ ≤ 1`) and `⟪f x, x⟫ = ‖x‖²`. -/
+  refine Submodule.orthogonal_le fun x hx ↦ eq_of_norm_le_re_inner_eq_norm_sq (𝕜 := 𝕜) ?_ ?_
+  · simpa using f.le_of_opNorm_le hf x
+  · have : ∀ y, ⟪f y, x⟫ = ⟪y, x⟫ := by
+      simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx
+    simp [this]
+
+theorem topologicalClosure_eqLocus_sum_coboundary_eq_top (f : E →L[𝕜] E) (hf : ‖f‖ ≤ 1) :
+    (End.fixedPoints f + End.coboundaries f).topologicalClosure = ⊤ := by
+  have h := sup_orthogonal_of_hasOrthogonalProjection (K := End.fixedPoints f)
+  rw [eq_top_iff] at *
+  grw [eqLocus_orthogonal_le_topologicalClosure_coboundary f hf,
+    ClosureOperator.sup_closure_le _ (LinearMap.eqLocus f 1)] at h
+  assumption
+
 set_option backward.isDefEq.respectTransparency false in
 /-- **Von Neumann Mean Ergodic Theorem** for an operator in a Hilbert space.
 For a contracting continuous linear self-map `f : E →L[𝕜] E` of a Hilbert space, `‖f‖ ≤ 1`,
@@ -89,20 +125,12 @@ converge to the orthogonal projection of `x` to the subspace of fixed points of
 theorem ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection (f : E →L[𝕜] E)
     (hf : ‖f‖ ≤ 1) (x : E) :
     Tendsto (birkhoffAverage 𝕜 f _root_.id · x) atTop
-      (𝓝 <| (LinearMap.eqLocus f 1).orthogonalProjection x) := by
+      (𝓝 <| (End.fixedPoints f).orthogonalProjection x) := by
   /- Due to the previous theorem, it suffices to verify
   that the range of `f - 1` is dense in the orthogonal complement
   to the submodule of fixed points of `f`. -/
-  apply (f : E →ₗ[𝕜] E).tendsto_birkhoffAverage_of_ker_subset_closure (f.lipschitz.weaken hf)
+  apply f.tendsto_birkhoffAverage_of_ker_subset_closure (f.lipschitz.weaken hf)
   · exact (LinearMap.eqLocus f 1).orthogonalProjection_mem_subspace_eq_self
   · clear x
-    /- In other words, we need to verify that any vector that is orthogonal to the range of `f - 1`
-    is a fixed point of `f`. -/
-    rw [Submodule.ker_orthogonalProjection, ← Submodule.topologicalClosure_coe,
-      SetLike.coe_subset_coe, ← Submodule.orthogonal_orthogonal_eq_closure]
-    /- To verify this, we verify `‖f x‖ ≤ ‖x‖` (because `‖f‖ ≤ 1`) and `⟪f x, x⟫ = ‖x‖²`. -/
-    refine Submodule.orthogonal_le fun x hx ↦ eq_of_norm_le_re_inner_eq_norm_sq (𝕜 := 𝕜) ?_ ?_
-    · simpa using f.le_of_opNorm_le hf x
-    · have : ∀ y, ⟪f y, x⟫ = ⟪y, x⟫ := by
-        simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx
-      simp [this]
+    rw [Submodule.ker_orthogonalProjection]
+    exact eqLocus_orthogonal_le_topologicalClosure_coboundary f hf

Mathlib/Analysis/Oscillation.lean

@@ -11,6 +11,7 @@ public import Mathlib.Topology.EMetricSpace.Diam
 public import Mathlib.Topology.EMetricSpace.Lipschitz
 public import Mathlib.Topology.UniformSpace.Cauchy
 public import Mathlib.Analysis.Normed.Group.Uniform
+public import Mathlib.Order.LiminfLimsup
 import Mathlib.Tactic.Scratchpad
 
 /-!
@@ -42,12 +43,15 @@ variable {E : Type u} {F : Type v} [PseudoEMetricSpace F]
 noncomputable def oscillation (f : E → F) (l : Filter E) : ENNReal :=
   ⨅ S ∈ l.map f, ediam S
 
+theorem oscillation_le_ediam_range {f : E → F} {l} : oscillation f l ≤ ediam (range f) :=
+  iInf_le_of_le (range f) (by simp)
+
 /-- The oscillation of `f : E → F` at `x`. -/
 noncomputable abbrev oscillationAt [TopologicalSpace E] (f : E → F) (x : E) : ENNReal :=
   oscillation f (𝓝 x)
 
 /-- The oscillation of `f : E → F` within `D` at `x`. -/
-noncomputable def oscillationWithinAt [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) :
+noncomputable abbrev oscillationWithinAt [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) :
     ENNReal :=
   oscillation f (𝓝[D] x)
 
@@ -209,6 +213,14 @@ lemma mul_biInf {p : ι → Prop} (hp : ∃ i, p i) {a : ℝ≥0∞} {f : ι →
   simp_rw [iInf_subtype, Subtype.exists] at this
   exact this hinfty
 
+@[to_dual iInf₂_eq_of_forall_ge_of_forall_gt_exists_lt]
+theorem iSup₂_eq_of_forall_le_of_forall_lt_exists_gt [CompleteLattice α] {b : α}
+    (h₁ : ∀ i j, f i j ≤ b) (h₂ : ∀ w, w < b → ∃ i j, w < f i j) : ⨆ (i) (j), f i j = b := by
+  have := iSup_eq_of_forall_le_of_forall_lt_exists_gt
+    (f := fun (ij : PSigma κ) ↦ f ij.1 ij.2) (b := b)
+  simp_rw [PSigma.forall, PSigma.exists, iSup_psigma] at this
+  exact this h₁ h₂
+
 end MoveMe
 
 section Cauchy
@@ -263,11 +275,11 @@ theorem LipschitzWith.oscillation_comp₂_le (g : α → β → γ) (f₁ : E 
       ≤ ↑K₁ * oscillation f₁ l + ↑K₂ * oscillation f₂ l := by
   unfold oscillation
   simp_rw [mul_biInf ⟨_, Filter.univ_mem⟩ (coe_ne_top · |>.elim)]
-  change_set _ ≤ (?a + ?b : ℝ≥0∞)
+  change_set _ ≤ ?a + ?b
   by_cases! ha : a = ∞; · simp [ha]
   by_cases! hb : b = ∞; · simp [hb]
-  apply ENNReal.le_of_forall_pos_le_add
-  intro ε hε hfin
+  apply _root_.le_of_forall_pos_le_add
+  intro ε hε
   rcases iInf₂_le_iff_forall_lt (l := a) |>.mp le_rfl (a + ε / 2)
     (lt_add_right ha (by norm_num [hε.ne'])) with ⟨sa, hsa, hsa'⟩
   rcases iInf₂_le_iff_forall_lt (l := b) |>.mp le_rfl (b + ε / 2)
@@ -297,4 +309,20 @@ theorem oscillation_mul_le (f₁ : E → F) (f₂ : E → F) (l : Filter E) :
     (fun _ => (isometry_mul_left _).lipschitz)
     |>.trans_eq (by simp only [coe_one, one_mul])
 
+@[to_additive]
+theorem oscillation_le_add_div (f₁ : E → F) (f₂ : E → F) (l : Filter E) :
+    oscillation f₁ l ≤ oscillation f₂ l + oscillation (f₁ / f₂) l := by
+  nth_rw 1 [show f₁ = f₂ * (f₁ / f₂) by simp]
+  exact oscillation_mul_le ..
+
+@[to_additive oscillation_le_two_mul_iSup_enorm]
+theorem oscillation_le_two_mul_iSup_enorm' (f : E → F) (l : Filter E) :
+    oscillation f l ≤ 2 * iSup (‖f ·‖ₑ) := by
+  apply oscillation_le_ediam_range.trans
+  refine ediam_le fun x hx y hy => ?_
+  rw [edist_eq_enorm_div x y, two_mul]
+  apply enorm_div_le.trans <| add_le_add _ _
+  · exact hx.out.elim fun z hz ↦ hz ▸ le_iSup (‖f ·‖ₑ) ..
+  · exact hy.out.elim fun z hz ↦ hz ▸ le_iSup (‖f ·‖ₑ) ..
+
 end SeminormedAddCommGroup

Mathlib/Data/EReal/Basic.lean

@@ -693,6 +693,14 @@ theorem coe_ennreal_mul : ∀ x y : ℝ≥0∞, ((x * y : ℝ≥0∞) : EReal) =
 theorem coe_ennreal_nsmul (n : ℕ) (x : ℝ≥0∞) : (↑(n • x) : EReal) = n • (x : EReal) :=
   map_nsmul (⟨⟨(↑), coe_ennreal_zero⟩, coe_ennreal_add⟩ : ℝ≥0∞ →+ EReal) _ _
 
+@[simp, norm_cast]
+theorem coe_ennreal_iSup {ι : Sort*} [hι : Nonempty ι] (f : ι → ℝ≥0∞) :
+    ((⨆ i, f i : ℝ≥0∞) : EReal) = ⨆ i, (f i : EReal) := by
+  refine le_antisymm ?_ (iSup_le fun i ↦ mod_cast le_iSup f i)
+  refine le_iSup_iff.mpr fun b hb ↦ ?_
+  lift b to ℝ≥0∞ using hι.elim fun i ↦ (EReal.coe_ennreal_nonneg _).trans (hb i)
+  exact mod_cast iSup_le fun i ↦ mod_cast hb i
+
 /-! ### toENNReal -/
 
 /-- `x.toENNReal` returns `x` if it is nonnegative, `0` otherwise. -/

Mathlib/Dynamics/BirkhoffSum/Average.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Dynamics.BirkhoffSum.Basic
 public import Mathlib.Algebra.Module.Basic
+public import Mathlib.Analysis.Normed.Group.Defs
 
 /-!
 # Birkhoff average

Mathlib/Dynamics/BirkhoffSum/Maximal.lean

@@ -13,8 +13,8 @@ import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.RCLike.Lemmas
 import Mathlib.Data.Real.StarOrdered
 public import Mathlib.Dynamics.BirkhoffSum.Average
-import Mathlib.Dynamics.BirkhoffSum.Measurable
-import Mathlib.Dynamics.BirkhoffSum.Integrable
+public import Mathlib.Dynamics.BirkhoffSum.Measurable
+public import Mathlib.Dynamics.BirkhoffSum.Integrable
 
 /-!
 # Maximal ergodic theorem.
@@ -93,14 +93,14 @@ variable [MeasurableSpace α] (μ : Measure α := by volume_tac) (hf : MeasurePr
 include hf
 
 @[fun_prop]
-lemma birkhoffMax_aestronglyMeasurable (hg : AEStronglyMeasurable g μ) :
+public lemma birkhoffMax_aestronglyMeasurable (hg : AEStronglyMeasurable g μ) :
     AEStronglyMeasurable (birkhoffMax f g n) μ := by
   unfold birkhoffMax
   induction n <;> measurability
 
 include hg
 
-lemma birkhoffMax_integrable : Integrable (birkhoffMax f g n) μ := by
+public lemma birkhoffMax_integrable : Integrable (birkhoffMax f g n) μ := by
   unfold birkhoffMax
   induction n with
   | zero => exact integrable_zero ..
@@ -192,8 +192,7 @@ theorem lt_birkhoffAverageSup_iff_lt_birkhoffSumSup {a : ℝ} (ha : 0 < a) :
 
 section MeasurePreserving
 
-variable {f : α → α} [MeasurableSpace α] (μ : Measure α := by volume_tac)
-  (hf : MeasurePreserving f μ μ)
+variable [MeasurableSpace α] (μ : Measure α) (hf : MeasurePreserving f μ μ)
 
 include hf
 
@@ -243,14 +242,14 @@ end Real
 
 section NormedAddCommGroup
 
-variable {E : Type*} [NormedAddCommGroup E] {g : α → E} (hg : Integrable g μ) [IsFiniteMeasure μ]
+variable [NormedAddCommGroup M] {g : α → M} (hg : Integrable g μ) [IsFiniteMeasure μ]
 
 include hg
 
 /-- 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 ↦ ?_
+    ∀ a : ℝ, a * μ.real {x | a < birkhoffAverageSup f (‖g ·‖) x} ≤ ∫ x, ‖g x‖ ∂μ := by
+  intro a
   by_cases! ha : 0 < a; swap
   · apply mul_nonpos_of_nonpos_of_nonneg ha measureReal_nonneg |>.trans
     exact integral_nonneg (fun _ ↦ norm_nonneg _)
@@ -260,6 +259,11 @@ public theorem iSup_distribution_birkhoffAverageSup_le_norm :
     _ ≤ ∫ x, ‖g x‖ ∂μ := by
       exact setIntegral_le_integral hg.norm (ae_of_all _ (norm_nonneg <| g ·))
 
+/-- Maximal ergodic theorem: the operator `birkhoffAverageSup` satisfies a weak-type inequality. -/
+public theorem iSup_distribution_birkhoffAverageSup_le_norm' :
+    ∀ a : ENNReal, μ {x | a < birkhoffAverageSup f (‖g ·‖) x} ≤ a⁻¹ * ‖hg.toL1‖ₑ := by
+  sorry
+
 end NormedAddCommGroup
 
 end MeasurePreserving

Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean

@@ -98,6 +98,27 @@ theorem tendsto_birkhoffAverage_apply_sub_birkhoffAverage' {g : α → E}
     Tendsto (fun n ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0) :=
   tendsto_birkhoffAverage_apply_sub_birkhoffAverage _ <| h.subset <| range_comp_subset_range _ _
 
+section TriangleInequality
+
+variable {f : α → α} {g : α → E} {n : ℕ} {x : α}
+
+@[bound]
+lemma norm_birkhoffSum_le :
+    ‖birkhoffSum f g n x‖ ≤ birkhoffSum f (‖g ·‖) n x :=
+  norm_sum_le _ _
+
+@[bound]
+lemma norm_birkhoffAverage_le {R : Type*} [RCLike R] [NormedSpace R E] :
+    ‖birkhoffAverage R f g n x‖ ≤ birkhoffAverage ℝ f (‖g ·‖) n x := by
+  by_cases! h : n = 0
+  · simp [birkhoffAverage, h]
+  apply Nat.zero_lt_of_ne_zero at h
+  simp only [birkhoffAverage, norm_smul, norm_inv, RCLike.norm_natCast, smul_eq_mul]
+  gcongr
+  exact norm_birkhoffSum_le
+
+end TriangleInequality
+
 end
 
 variable (𝕜 : Type*) {X E : Type*}

Mathlib/Dynamics/BirkhoffSum/Pointwise.lean

@@ -0,0 +1,78 @@
+/-
+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
+-/
+module
+
+import Mathlib.Analysis.Oscillation
+import Mathlib.Dynamics.BirkhoffSum.Maximal
+import Mathlib.Tactic.Scratchpad
+import Mathlib.Dynamics.BirkhoffSum.NormedSpace
+import Mathlib.Analysis.InnerProductSpace.MeanErgodic
+
+open MeasureTheory Measure MeasurableSpace Filter Topology Module
+open scoped NNReal ENNReal
+
+variable {α R M : Type*} {f : α → α} {g : α → M} {n : ℕ} [RCLike R]
+  [MeasurableSpace α] (μ : Measure α) (hf : MeasurePreserving f μ μ)
+  [NormedAddCommGroup M] (hg : Integrable g μ) [IsFiniteMeasure μ] [NormedSpace R M]
+
+variable {μ} (R M) in
+abbrev koopman (p) : End R (Lp M p μ) := Lp.compMeasurePreservingₗ R f hf
+
+variable (R M f) in
+def convergenceSet := {g : Lp M 1 μ | ∀ᵐ x ∂μ, oscillation (birkhoffAverage R f g · x) atTop = 0}
+
+lemma mem_convergenceSet_of_mem_coboundary {g : Lp M 1 μ}
+    (hg : g ∈ End.coboundaries (koopman R M hf 1)) : g ∈ convergenceSet R M f μ := by
+  rcases hg with ⟨h, hh⟩
+  simp at hh
+
+  sorry
+
+lemma ENNReal.forall_pos_of_forall_mul {motive : ℝ≥0∞ → Prop} (k : ℝ≥0∞)
+    (h : ∀ ε > 0, motive (k * ε)) (hk₀ : k ≠ 0 := by positivity) (hk : k ≠ ∞ := by finiteness) :
+    ∀ ε > 0, motive ε := fun ε hε ↦
+  ENNReal.mul_div_cancel (a := k) (b := ε) hk₀ hk ▸ h (ε / k) (ENNReal.div_pos hε.ne_zero hk)
+
+omit [IsFiniteMeasure μ] in
+lemma foo {f : α → ℝ≥0∞} (h : ∀ ε > 0, ∀ᵐ x ∂μ, f x ≤ ε) : ∀ᵐ x ∂μ, f x ≤ 0 := by
+  have H : ∀ᵐ x ∂μ, ∀ n : ℕ, f x ≤ (n : ℝ≥0∞)⁻¹ :=
+    ae_all_iff.mpr fun n ↦ h _ (ENNReal.inv_pos.mpr (by finiteness))
+  filter_upwards [H] with x hx
+  refine le_of_forall_pos_le_add fun ε hε => ?_
+  obtain ⟨n, hn⟩ := ENNReal.exists_inv_nat_lt hε.ne_zero
+  exact (hx n).trans (by simp [hn.le])
+
+include hf in
+theorem closed_convergenceSet : IsClosed (convergenceSet R M f μ) := by
+  refine isClosed_of_closure_subset (fun g hg ↦ ?_)
+  rw [EMetric.mem_closure_iff] at hg
+  simp only [convergenceSet, ← nonpos_iff_eq_zero, Set.mem_setOf_eq]
+  apply foo
+  refine ENNReal.forall_pos_of_forall_mul 2 fun δ hδ ↦ ?_
+  by_cases! hδ' : δ = ∞; · bound
+  apply ae_iff.mpr <| nonpos_iff_eq_zero.mp _
+  push Not
+  have (h : Lp M 1 μ) (hh : h ∈ convergenceSet R M f μ) :
+      ∀ᵐ x ∂μ, 2 * δ < oscillation (birkhoffAverage R f g · x) atTop →
+      δ < birkhoffAverageSup f (‖(⇑g - ⇑h) ·‖) x := by
+    filter_upwards [hh] with x hosc hx
+    have := hx.trans_le <| oscillation_le_add_sub (f₂ := (birkhoffAverage R f h · x)) ..
+    rw [hosc] at this
+    grw [oscillation_le_two_mul_iSup_enorm] at this
+    simp only [Pi.sub_apply, zero_add, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
+      ENNReal.ofNat_ne_top, ENNReal.mul_lt_mul_iff_right] at this
+    change _ < ⨆ n, ‖(birkhoffAverage R f g - _) n x‖ₑ at this
+    rw [← birkhoffAverage_sub] at this
+    simp_rw [← EReal.coe_ennreal_lt_coe_ennreal_iff, EReal.coe_ennreal_iSup] at this
+    exact this.trans_le (iSup_mono fun _ ↦ EReal.coe_le_coe norm_birkhoffAverage_le)
+  refine le_of_forall_gt fun c hc ↦ ?_
+  rcases hg (δ * c) (by positivity) with ⟨h, hh, hh'⟩
+  apply measure_mono_ae (this h hh) |>.trans_lt
+  apply iSup_distribution_birkhoffAverageSup_le_norm' μ hf (by fun_prop) δ |>.trans_lt
+  rw [Integrable.toL1_sub g h (by fun_prop) (by fun_prop), ← edist_eq_enorm_sub,
+    Integrable.toL1_coeFn, Integrable.toL1_coeFn]
+  apply ENNReal.mul_lt_mul_right (ENNReal.inv_ne_zero.mpr hδ') (by finiteness) hh' |>.trans_le
+  rw [ENNReal.inv_mul_cancel_left (by positivity) hδ']

Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean

@@ -101,6 +101,7 @@ end AEEqFun
 namespace L1
 
 
+@[fun_prop]
 theorem integrable_coeFn (f : α →₁[μ] β) : Integrable f μ := by
   rw [← memLp_one_iff_integrable]
   exact Lp.memLp f