generalize oscillation

Author: lua-vr

Mathlib/Analysis/Oscillation.lean

@@ -1,21 +1,24 @@
 /-
 Copyright (c) 2024 James Sundstrom. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: James Sundstrom
+Authors: James Sundstrom, Lua Viana Reis
 -/
 module
 
 public import Mathlib.Data.ENNReal.Real
 public import Mathlib.Order.WellFoundedSet
 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
 
 /-!
 # Oscillation
 
-In this file we define the oscillation of a function `f: E → F` at a point `x` of `E`. (`E` is
-required to be a TopologicalSpace and `F` a PseudoEMetricSpace.) The oscillation of `f` at `x` is
-defined to be the infimum of `diam f '' N` for all neighborhoods `N` of `x`. We also define
-`oscillationWithin f D x`, which is the oscillation at `x` of `f` restricted to `D`.
+In this file we define the oscillation of a function `f: E → F` along a filter `l` of `E`. (`F` is
+required to be a PseudoEMetricSpace.) The oscillation of `f` at `l` is
+defined to be the infimum of `diam f '' N` for all sets `N` in `l`. We also define
+`oscillationWithin f D l`, which is the oscillation at `l` of `f` restricted to `D`.
 
 We also prove some simple facts about oscillation, most notably that the oscillation of `f`
 at `x` is 0 if and only if `f` is continuous at `x`, with versions for both `oscillation` and
@@ -28,35 +31,39 @@ oscillation, oscillationWithin
 
 @[expose] public section
 
-open Topology Metric Set ENNReal
+open Topology Metric Set ENNReal Filter
 
 universe u v
 
 variable {E : Type u} {F : Type v} [PseudoEMetricSpace F]
 
+/-- The oscillation of `f : E → F` along `l`. -/
+noncomputable def oscillation (f : E → F) (l : Filter E) : ENNReal :=
+  ⨅ S ∈ l.map f, ediam S
+
 /-- The oscillation of `f : E → F` at `x`. -/
-noncomputable def oscillation [TopologicalSpace E] (f : E → F) (x : E) : ENNReal :=
-  ⨅ S ∈ (𝓝 x).map f, ediam S
+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 oscillationWithin [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) :
+noncomputable def oscillationWithinAt [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) :
     ENNReal :=
-  ⨅ S ∈ (𝓝[D] x).map f, ediam S
+  oscillation f (𝓝[D] x)
 
 /-- The oscillation of `f` at `x` within a neighborhood `D` of `x` is equal to `oscillation f x` -/
-theorem oscillationWithin_nhds_eq_oscillation [TopologicalSpace E] (f : E → F) (D : Set E) (x : E)
-    (hD : D ∈ 𝓝 x) : oscillationWithin f D x = oscillation f x := by
-  rw [oscillation, oscillationWithin, nhdsWithin_eq_nhds.2 hD]
+theorem oscillationWithinAt_nhds_eq_oscillationAt [TopologicalSpace E] (f : E → F) (D : Set E)
+    (x : E) (hD : D ∈ 𝓝 x) : oscillationWithinAt f D x = oscillationAt f x := by
+  rw [oscillationAt, oscillationWithinAt, nhdsWithin_eq_nhds.2 hD]
 
 /-- The oscillation of `f` at `x` within `univ` is equal to `oscillation f x` -/
-theorem oscillationWithin_univ_eq_oscillation [TopologicalSpace E] (f : E → F) (x : E) :
-    oscillationWithin f univ x = oscillation f x :=
-  oscillationWithin_nhds_eq_oscillation f univ x Filter.univ_mem
+theorem oscillationWithinAt_univ_eq_oscillationAt [TopologicalSpace E] (f : E → F) (x : E) :
+    oscillationWithinAt f univ x = oscillationAt f x :=
+  oscillationWithinAt_nhds_eq_oscillationAt f univ x Filter.univ_mem
 
 namespace ContinuousWithinAt
 
-theorem oscillationWithin_eq_zero [TopologicalSpace E] {f : E → F} {D : Set E}
-    {x : E} (hf : ContinuousWithinAt f D x) : oscillationWithin f D x = 0 := by
+theorem oscillationWithinAt_eq_zero [TopologicalSpace E] {f : E → F} {D : Set E}
+    {x : E} (hf : ContinuousWithinAt f D x) : oscillationWithinAt f D x = 0 := by
   rw [← nonpos_iff_eq_zero]
   refine _root_.le_of_forall_pos_le_add fun ε hε ↦ ?_
   rw [zero_add]
@@ -69,35 +76,36 @@ end ContinuousWithinAt
 
 namespace ContinuousAt
 
-theorem oscillation_eq_zero [TopologicalSpace E] {f : E → F} {x : E} (hf : ContinuousAt f x) :
-    oscillation f x = 0 := by
+theorem oscillationAt_eq_zero [TopologicalSpace E] {f : E → F} {x : E} (hf : ContinuousAt f x) :
+    oscillationAt f x = 0 := by
   rw [← continuousWithinAt_univ f x] at hf
-  exact oscillationWithin_univ_eq_oscillation f x ▸ hf.oscillationWithin_eq_zero
+  exact oscillationWithinAt_univ_eq_oscillationAt f x ▸ hf.oscillationWithinAt_eq_zero
 
 end ContinuousAt
 
-namespace OscillationWithin
+namespace OscillationWithinAt
 
 /-- The oscillation within `D` of `f` at `x ∈ D` is 0 if and only if `ContinuousWithinAt f D x`. -/
 theorem eq_zero_iff_continuousWithinAt [TopologicalSpace E] (f : E → F) {D : Set E}
-    {x : E} (xD : x ∈ D) : oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x := by
-  refine ⟨fun hf ↦ EMetric.tendsto_nhds.mpr (fun ε ε0 ↦ ?_), fun hf ↦ hf.oscillationWithin_eq_zero⟩
-  simp_rw [← hf, oscillationWithin, iInf_lt_iff] at ε0
+    {x : E} (xD : x ∈ D) : oscillationWithinAt f D x = 0 ↔ ContinuousWithinAt f D x := by
+  refine ⟨fun hf ↦ EMetric.tendsto_nhds.mpr (fun ε ε0 ↦ ?_),
+    fun hf ↦ hf.oscillationWithinAt_eq_zero⟩
+  simp_rw [← hf, oscillationWithinAt, oscillation, iInf_lt_iff] at ε0
   obtain ⟨S, hS, Sε⟩ := ε0
   refine Filter.mem_of_superset hS (fun y hy ↦ lt_of_le_of_lt ?_ Sε)
   exact edist_le_ediam_of_mem (mem_preimage.1 hy) <| mem_preimage.1 (mem_of_mem_nhdsWithin xD hS)
 
-end OscillationWithin
+end OscillationWithinAt
 
-namespace Oscillation
+namespace OscillationAt
 
 /-- The oscillation of `f` at `x` is 0 if and only if `f` is continuous at `x`. -/
 theorem eq_zero_iff_continuousAt [TopologicalSpace E] (f : E → F) (x : E) :
-    oscillation f x = 0 ↔ ContinuousAt f x := by
-  rw [← oscillationWithin_univ_eq_oscillation, ← continuousWithinAt_univ f x]
-  exact OscillationWithin.eq_zero_iff_continuousWithinAt f (mem_univ x)
+    oscillationAt f x = 0 ↔ ContinuousAt f x := by
+  rw [← oscillationWithinAt_univ_eq_oscillationAt, ← continuousWithinAt_univ f x]
+  exact OscillationWithinAt.eq_zero_iff_continuousWithinAt f (mem_univ x)
 
-end Oscillation
+end OscillationAt
 
 namespace IsCompact
 
@@ -106,7 +114,7 @@ variable {f : E → F} {D : Set E} {ε : ENNReal}
 
 /-- If `oscillationWithin f D x < ε` at every `x` in a compact set `K`, then there exists `δ > 0`
 such that the oscillation of `f` on `ball x δ ∩ D` is less than `ε` for every `x` in `K`. -/
-theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscillationWithin f D x < ε) :
+theorem uniform_oscillationWithinAt (comp : IsCompact K) (hK : ∀ x ∈ K, oscillationWithinAt f D x < ε) :
     ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε := by
   let S := fun r ↦
     {x : E | ∃ (a : ℝ), (a > r ∧ ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε)}
@@ -120,8 +128,8 @@ theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscill
     rw [← ofReal_add (by linarith) (by linarith), sub_add_cancel]
   have S_cover : K ⊆ ⋃ r > 0, S r := by
     intro x hx
-    have : oscillationWithin f D x < ε := hK x hx
-    simp only [oscillationWithin, Filter.mem_map, iInf_lt_iff] at this
+    have : oscillationWithinAt f D x < ε := hK x hx
+    simp only [oscillationWithinAt, oscillation, Filter.mem_map, iInf_lt_iff] at this
     obtain ⟨n, hn₁, hn₂⟩ := this
     obtain ⟨r, r0, hr⟩ := EMetric.mem_nhdsWithin_iff.1 hn₁
     simp only [gt_iff_lt, mem_iUnion, exists_prop]
@@ -154,10 +162,140 @@ theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscill
 /-- If `oscillation f x < ε` at every `x` in a compact set `K`, then there exists `δ > 0` such
 that the oscillation of `f` on `ball x δ` is less than `ε` for every `x` in `K`. -/
 theorem uniform_oscillation {K : Set E} (comp : IsCompact K)
-    {f : E → F} {ε : ENNReal} (hK : ∀ x ∈ K, oscillation f x < ε) :
+    {f : E → F} {ε : ENNReal} (hK : ∀ x ∈ K, oscillationAt f x < ε) :
     ∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ))) ≤ ε := by
-  simp only [← oscillationWithin_univ_eq_oscillation] at hK
-  convert! ← comp.uniform_oscillationWithin hK
+  simp only [← oscillationWithinAt_univ_eq_oscillationAt] at hK
+  convert! ← comp.uniform_oscillationWithinAt hK
   exact inter_univ _
 
 end IsCompact
+
+section MoveMe
+
+variable {ι : Sort*} {κ : ι → Sort*} {α : Type*} {f : (i : ι) → κ i → α}
+
+@[to_dual iInf₂_le_iff]
+theorem le_iSup₂_iff [CompleteSemilatticeSup α] {a : α} :
+    a ≤ ⨆ (i) (j), f i j ↔ ∀ b, (∀ i j, f i j ≤ b) → a ≤ b := by
+  simp [iSup, le_sSup_iff, upperBounds]
+
+@[to_dual iInf₂_lt_iff]
+theorem lt_iSup₂_iff [CompleteLinearOrder α] {a : α} :
+    a < ⨆ (i) (j), f i j ↔ ∃ i j, a < f i j := by
+  have := lt_iSup_iff (f := fun (ij : PSigma κ) ↦ f ij.1 ij.2) (a := a)
+  simp_rw [PSigma.exists, iSup_psigma] at this
+  exact this
+
+@[to_dual iInf₂_le_iff_forall_lt]
+theorem le_iSup₂_iff_forall_lt [CompleteLinearOrder α] {l : α} :
+    l ≤ ⨆ (i) (j), f i j ↔ ∀ b < l, ∃ i j, b < f i j := by
+  have := le_iSup_iff_forall_lt (f := fun (ij : PSigma κ) ↦ f ij.1 ij.2) (l := l)
+  simp_rw [PSigma.exists, iSup_psigma] at this
+  exact this
+
+@[to_dual lt_iInf₂_iff]
+theorem iSup₂_lt_iff [CompleteLattice α] {l : α} :
+    ⨆ (i) (j), f i j < l ↔ ∃ b < l, ∀ i j, f i j ≤ b := by
+  have := iSup_lt_iff (f := fun (ij : PSigma κ) ↦ f ij.1 ij.2) (l := l)
+  simp_rw [PSigma.forall, iSup_psigma] at this
+  exact this
+
+lemma mul_biInf {p : ι → Prop} (hp : ∃ i, p i) {a : ℝ≥0∞} {f : ι → ℝ≥0∞}
+    (hinfty : a = ∞ → ⨅ (i) (_ : p i), f i = 0 → ∃ i, ∃ (_ : p i), f i = 0) :
+    a * ⨅ (i) (_ : p i), f i = ⨅ (i) (_ : p i), a * f i := by
+  haveI : Nonempty {i // p i} := nonempty_subtype.mpr hp
+  have := mul_iInf (ι := {i // p i}) (a := a) (f := (f ·))
+  simp_rw [iInf_subtype, Subtype.exists] at this
+  exact this hinfty
+
+end MoveMe
+
+section Cauchy
+
+variable {f : E → F}
+
+theorem EMetric.cauchy_iff_iInf_ediam_eq_zero (l : Filter F) [NeBot l] :
+    Cauchy l ↔ ⨅ s ∈ l, ediam s = 0 := by
+  rw [EMetric.cauchy_iff, ←nonpos_iff_eq_zero, iInf₂_le_iff_forall_lt]
+  constructor
+  · intro h ε hε
+    rcases exists_between hε with ⟨η, hη⟩
+    rcases h.right η hη.1 with ⟨s, hs₁, hs₂⟩
+    use s, hs₁
+    apply iSup₂_lt_iff.mpr
+    use η, hη.2
+    intro i hi
+    apply iSup₂_le_iff.mpr
+    intro j hj
+    exact hs₂ i hi j hj |>.le
+  · intro h
+    use NeBot.ne'
+    intro ε hε
+    rcases h ε hε with ⟨s, hs₁, hs₂⟩
+    use s, hs₁
+    intro i hi j hj
+    rcases iSup₂_lt_iff.mp hs₂ with ⟨l, hl, hs₃⟩
+    specialize hs₃ i hi
+    exact iSup₂_le_iff.mp hs₃ j hj |>.trans_lt hl
+
+theorem cauchy_iff_oscillation_eq_zero (l : Filter E) [NeBot l] :
+    Cauchy (l.map f) ↔ oscillation f l = 0 :=
+  EMetric.cauchy_iff_iInf_ediam_eq_zero _
+
+/-- A function `f` whose domain is a complete `EMetric` space converges to a point along a filter if
+and only if its oscillation along `l` is equal to zero. -/
+theorem EMetric.tendsTo_nhds_iff_oscillation_eq_zero [CompleteSpace F] (l : Filter E) [NeBot l] :
+    (∃ x, Tendsto f l (𝓝 x)) ↔ oscillation f l = 0 := by
+  rw [←cauchy_map_iff_exists_tendsto]
+  exact cauchy_iff_oscillation_eq_zero _
+
+end Cauchy
+
+section Lipschitz
+
+variable {α β γ : Type*} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ]
+
+theorem LipschitzWith.oscillation_comp₂_le (g : α → β → γ) (f₁ : E → α) (f₂ : E → β)
+    {K₁ K₂ : NNReal} (l : Filter E)
+    (hf₁ : ∀ b, LipschitzWith K₁ (g · b)) (hf₂ : ∀ a, LipschitzWith K₂ (g a ·)) :
+    oscillation (fun a ↦ g (f₁ a) (f₂ a)) l
+      ≤ ↑K₁ * oscillation f₁ l + ↑K₂ * oscillation f₂ l := by
+  unfold oscillation
+  simp_rw [mul_biInf ⟨_, Filter.univ_mem⟩ (coe_ne_top · |>.elim)]
+  -- this would be more convenient with a `setm` tactic
+  set a := ⨅ i ∈ map f₁ l, ↑K₁ * ediam i
+  set b := ⨅ i ∈ map f₂ l, ↑K₂ * ediam i
+  by_cases! ha : a = ∞; · simp [ha]
+  by_cases! hb : b = ∞; · simp [hb]
+  apply ENNReal.le_of_forall_pos_le_add
+  intro ε hε hfin
+  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)
+    (lt_add_right hb (by norm_num [hε.ne'])) with ⟨sb, hsb, hsb'⟩
+  rw [show a + b + ε = a + ε / 2 + (b + ε / 2) by
+    ring_nf
+    rw [ENNReal.div_mul_cancel (by positivity) (by finiteness)]]
+  apply ENNReal.add_lt_add hsa' hsb' |>.trans_le' _ |>.le
+  apply iInf₂_le_of_le (image2 g sa sb) _ _
+  · rw [mem_map] at ⊢ hsa hsb
+    exact l.mem_of_superset (l.inter_mem hsa hsb) fun a ⟨h₁, h₂⟩ ↦ ⟨f₁ a, h₁, f₂ a, h₂, rfl⟩
+  · exact LipschitzOnWith.ediam_image2_le _ _ _
+      (fun s _ ↦ hf₁ s |>.lipschitzOnWith)
+      (fun s _ ↦ hf₂ s |>.lipschitzOnWith)
+
+end Lipschitz
+
+section SeminormedAddCommGroup
+
+variable {F : Type*} [SeminormedCommGroup F]
+
+@[to_additive]
+theorem oscillation_mul_le (f₁ : E → F) (f₂ : E → F) (l : Filter E) :
+    oscillation (f₁ * f₂) l ≤ oscillation f₁ l + oscillation f₂ l :=
+  LipschitzWith.oscillation_comp₂_le (· * ·) f₁ f₂ l
+    (fun _ => (isometry_mul_right _).lipschitz)
+    (fun _ => (isometry_mul_left _).lipschitz)
+    |>.trans_eq (by simp only [coe_one, one_mul])
+
+end SeminormedAddCommGroup