pointwise birkhoff theorem

Author: lua-vr

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,6 +43,9 @@ 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)
@@ -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
@@ -266,8 +278,8 @@ theorem LipschitzWith.oscillation_comp₂_le (g : α → β → γ) (f₁ : E 
   change_set _ ≤ (?a + ?b : ℝ≥0∞)
   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/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 α := by volume_tac) (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 _)

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 [NormedSpace ℝ E] :
+    ‖birkhoffAverage ℝ 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,104 @@
+/-
+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
+
+open MeasureTheory Measure MeasurableSpace Filter Topology
+
+variable {α M : Type*} {f : α → α} {g : α → M} {n : ℕ}
+
+variable [MeasurableSpace α] (μ : Measure α) (hf : MeasurePreserving f μ μ)
+
+variable [NormedAddCommGroup M] (hg : Integrable g μ) [IsFiniteMeasure μ] [NormedSpace ℝ M]
+
+variable (M f) in
+def convergenceSet :=
+  {g : Lp M 1 μ | ∀ᵐ x ∂μ, oscillation (birkhoffAverage ℝ f g · x) atTop = 0}
+
+open scoped NNReal ENNReal
+
+theorem ENNReal.forall_pos_of_forall_nat_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])
+
+theorem EReal.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 ↦ ?_
+  have h0 : 0 ≤ b := hι.elim fun i ↦ (EReal.coe_ennreal_nonneg _).trans (hb i)
+  obtain ⟨c, rfl⟩ : ∃ c : ℝ≥0∞, (c : EReal) = b := ⟨b.toENNReal, EReal.coe_toENNReal h0⟩
+  exact mod_cast iSup_le fun i ↦ mod_cast hb i
+
+include hf in
+theorem closed_convergenceSet : IsClosed (convergenceSet 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_nat_mul 2 fun δ hδ ↦ ?_
+  apply ae_iff.mpr <| nonpos_iff_eq_zero.mp _
+  push Not
+  have (h : Lp M 1 μ) (hh : h ∈ convergenceSet M f μ) :
+      ∀ᵐ x ∂μ, 2 * δ < oscillation (birkhoffAverage ℝ 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 ℝ f h · x)) ..
+    rw [hosc] at this
+    grw [oscillation_le_two_mul_iSup_enorm] at this
+    simp [ENNReal.mul_lt_mul_iff_right] at this
+    change _ < ⨆ n, ‖(birkhoffAverage ℝ f g - _) n x‖ₑ at this
+    rw [← birkhoffAverage_sub] at this
+    simp_rw [←ofReal_norm, ←EReal.coe_ennreal_lt_coe_ennreal_iff] at this
+    simp_rw [EReal.coe_ennreal_iSup, EReal.coe_ennreal_ofReal, max_eq_left (norm_nonneg _)] at this
+    exact this.trans_le (iSup_mono fun _ ↦ EReal.coe_le_coe norm_birkhoffAverage_le)
+  refine le_of_forall_gt fun c hc ↦ ?_
+
+  apply measure_mono_ae (this _)
+
+
+  done
+
+/-   simp only [convergenceSet, ← nonpos_iff_eq_zero, Set.mem_setOf_eq]
+  apply foo
+  refine ENNReal.forall_pos_of_forall_nat_mul 2 fun δ hδ ↦ ?_
+  rcases hg δ hδ with ⟨h, hh, hh'⟩
+  filter_upwards [hh] with x hx
+  apply le_of_forall_pos_le_add
+  refine ENNReal.forall_pos_of_forall_nat_mul 2 fun ε hε ↦ ?_
+  apply oscillation_le_add_sub (f₂ := (birkhoffAverage ℝ f h · x)) .. |>.trans
+  change _ + oscillation ((birkhoffAverage ℝ f g - birkhoffAverage ℝ f h) · x) _ ≤ _
+  rw [←birkhoffAverage_sub, hx, zero_add, ←mul_add]
+  apply oscillation_le_two_mul_norm_max _ _ |>.trans
+  gcongr
+  simp_rw [←ofReal_norm]
+  apply (iSup_mono fun _ ↦ ENNReal.ofReal_le_ofReal norm_birkhoffAverage_le).trans
+  apply EReal.coe_ennreal_le_coe_ennreal_iff.mp
+  simp only [Pi.sub_apply, EReal.coe_ennreal_iSup, EReal.coe_ennreal_ofReal, EReal.coe_max,
+    EReal.coe_zero, EReal.coe_ennreal_add, iSup_le_iff, sup_le_iff]
+  push ∀ _, _
+  rw [← iSup_le_iff, ← birkhoffAverageSup]
+
+
+  push_cast
+  simp
+  -- apply iSup_le_iff.mpr
+  -- intro i
+  done
+ -/

Mathlib/Order/LiminfLimsup.lean

@@ -815,17 +815,17 @@ section ConditionallyCompleteLinearOrder
 variable [ConditionallyCompleteLinearOrder α]
 
 /-- If `Filter.limsup u atTop ≤ x`, then for all `ε > 0`, eventually we have `u b < x + ε`. -/
-theorem eventually_lt_add_pos_of_limsup_le [Preorder β] [AddZeroClass α] [AddLeftStrictMono α]
-    {x ε : α} {u : β → α} (hu_bdd : IsBoundedUnder LE.le atTop u) (hu : Filter.limsup u atTop ≤ x)
-    (hε : 0 < ε) :
-    ∀ᶠ b : β in atTop, u b < x + ε :=
+theorem eventually_lt_add_pos_of_limsup_le [AddZeroClass α] [AddLeftStrictMono α]
+    {x ε : α} {u : β → α} {f : Filter β} (hu_bdd : IsBoundedUnder LE.le f u)
+    (hu : Filter.limsup u f ≤ x) (hε : 0 < ε) :
+    ∀ᶠ b : β in f, u b < x + ε :=
   eventually_lt_of_limsup_lt (lt_of_le_of_lt hu (lt_add_of_pos_right x hε)) hu_bdd
 
 /-- If `x ≤ Filter.liminf u atTop`, then for all `ε < 0`, eventually we have `x + ε < u b`. -/
-theorem eventually_add_neg_lt_of_le_liminf [Preorder β] [AddZeroClass α] [AddLeftStrictMono α]
-    {x ε : α} {u : β → α} (hu_bdd : IsBoundedUnder GE.ge atTop u) (hu : x ≤ Filter.liminf u atTop)
-    (hε : ε < 0) :
-    ∀ᶠ b : β in atTop, x + ε < u b :=
+theorem eventually_add_neg_lt_of_le_liminf [AddZeroClass α] [AddLeftStrictMono α]
+    {x ε : α} {u : β → α} {f : Filter β} (hu_bdd : IsBoundedUnder GE.ge f u)
+    (hu : x ≤ Filter.liminf u f) (hε : ε < 0) :
+    ∀ᶠ b : β in f, x + ε < u b :=
   eventually_lt_of_lt_liminf (lt_of_lt_of_le (add_lt_of_neg_right x hε) hu) hu_bdd
 
 /-- If `Filter.limsup u atTop ≤ x`, then for all `ε > 0`, there exists a positive natural

Mathlib/Tactic/Scratchpad.lean

@@ -1,6 +1,8 @@
 module
 
 public import Mathlib.Tactic.Set
+public import Lean.Meta.Tactic.TryThis
+public import Lean.Meta.Tactic.ExposeNames
 
 set_option trace.debug true
 set_option pp.rawOnError true
@@ -42,3 +44,60 @@ example : (fun x => x + 1) 0 = 1 + 0 := by
   change_set ?a + 1 = ?b
 
   rfl
+
+
+open Lean Elab Meta Tactic
+open Lean.Meta.Tactic.TryThis
+
+namespace MakeHave
+
+private meta partial def leadingIndent (source : String) (pos : String.Pos.Raw) : String :=
+  let rec go (i : String.Pos.Raw) : String.Pos.Raw :=
+    if i.atEnd source then
+      i
+    else
+      let c := i.get source
+      if c == ' ' || c == '\t' then
+        go (i.next source)
+      else
+        i
+  String.Pos.Raw.extract source pos (go pos)
+
+private meta def insertHaveSuggestion (ref : Syntax) : TacticM Unit := do
+  let some refRange := ref.getRange?
+    | return
+  let target ← instantiateMVars (← getMainTarget)
+  let targetFmt ← withOptions (pp.mvars.set · false) <| withExposedNames <|
+    PrettyPrinter.ppExpr target
+  let targetText := targetFmt.pretty 100000
+  let fileMap ← getFileMap
+  let lineStart := fileMap.lineStart (fileMap.toPosition refRange.start).line
+  let indent := leadingIndent fileMap.source lineStart
+  let newText := s!"{indent}have : {targetText} := sorry\n"
+  let insertionRange : Syntax.Range := ⟨lineStart, lineStart⟩
+  let title := "Insert `have` for current goal"
+  let suggestion : Suggestion := {
+    suggestion := .string newText
+    toCodeActionTitle? := some fun _ => title
+  }
+  addSuggestion ref suggestion (origSpan? := some (Syntax.ofRange insertionRange))
+    (header := "Code action:")
+
+/--
+Emit a code action inserting `have : <current goal> := sorry` before the current tactic line.
+
+This is intended for use as a `simp` discharger, for example:
+`simp (disch:=make_have)`. For `simp` discharger goals, the tactic records the
+code action and admits the generated side condition so that `simp` can finish.
+The inserted `have` can then discharge later runs via `simp (disch:=assumption)`.
+-/
+elab "make_have" : tactic => do
+  let goal ← getMainGoal
+  insertHaveSuggestion (← getRef)
+  if (← goal.getTag) == `simp.discharger then
+    admitGoal goal (synthetic := false)
+
+example (x y : Int) : x / x + y / y = 2 := by
+  simp (disch := first | assumption | make_have)
+
+end MakeHave