generalize oscillation

Author: lua-vr

Mathlib/Analysis/Oscillation.lean

@@ -1,21 +1,22 @@
 /-
 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.UniformSpace.Cauchy
 
 /-!
 # 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 +29,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 +74,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 +112,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 +126,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 +160,76 @@ 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
+
+end MoveMe
+
+section Cauchy
+
+variable {f : E → F}
+
+theorem EMetric.cauchy_iff_iInf_ediam_eq_zero (l : Filter F) [NeBot l] :
+    Cauchy l ↔ 0 = ⨅ s ∈ l, ediam s := by
+  rw [EMetric.cauchy_iff, eq_comm, ←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) ↔ 0 = oscillation f l :=
+  EMetric.cauchy_iff_iInf_ediam_eq_zero _
+
+end Cauchy