Skip to content

Commit bd6c047

Browse files
lua-vrlua-vr
committed
generalize oscillation
1 parent 8bfad47 commit bd6c047

2 files changed

Lines changed: 206 additions & 41 deletions

File tree

‎Mathlib/Analysis/BoxIntegral/Basic.lean‎

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

‎Mathlib/Analysis/Oscillation.lean‎

Lines changed: 202 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,24 @@
11
/-
22
Copyright (c) 2024 James Sundstrom. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: James Sundstrom
4+
Authors: James Sundstrom, Lua Viana Reis
55
-/
66
module
77

88
public import Mathlib.Data.ENNReal.Real
99
public import Mathlib.Order.WellFoundedSet
1010
public import Mathlib.Topology.EMetricSpace.Diam
11+
public import Mathlib.Topology.EMetricSpace.Lipschitz
12+
public import Mathlib.Topology.UniformSpace.Cauchy
13+
public import Mathlib.Analysis.Normed.Group.Uniform
1114

1215
/-!
1316
# Oscillation
1417
15-
In this file we define the oscillation of a function `f: E → F` at a point `x` of `E`. (`E` is
16-
required to be a TopologicalSpace and `F` a PseudoEMetricSpace.) The oscillation of `f` at `x` is
17-
defined to be the infimum of `diam f '' N` for all neighborhoods `N` of `x`. We also define
18-
`oscillationWithin f D x`, which is the oscillation at `x` of `f` restricted to `D`.
18+
In this file we define the oscillation of a function `f: E → F` along a filter `l` of `E`. (`F` is
19+
required to be a PseudoEMetricSpace.) The oscillation of `f` at `l` is
20+
defined to be the infimum of `diam f '' N` for all sets `N` in `l`. We also define
21+
`oscillationWithin f D l`, which is the oscillation at `l` of `f` restricted to `D`.
1922
2023
We also prove some simple facts about oscillation, most notably that the oscillation of `f`
2124
at `x` is 0 if and only if `f` is continuous at `x`, with versions for both `oscillation` and
@@ -28,35 +31,42 @@ oscillation, oscillationWithin
2831

2932
@[expose] public section
3033

31-
open Topology Metric Set ENNReal
34+
open Topology Metric Set ENNReal Filter
3235

3336
universe u v
3437

3538
variable {E : Type u} {F : Type v} [PseudoEMetricSpace F]
3639

40+
/-- The oscillation of `f : E → F` along `l`. -/
41+
noncomputable def oscillation (f : E → F) (l : Filter E) : ENNReal :=
42+
⨅ S ∈ l.map f, ediam S
43+
44+
theorem oscillation_le_ediam_range {f : E → F} {l} : oscillation f l ≤ ediam (range f) :=
45+
iInf_le_of_le (range f) (by simp)
46+
3747
/-- The oscillation of `f : E → F` at `x`. -/
38-
noncomputable def oscillation [TopologicalSpace E] (f : E → F) (x : E) : ENNReal :=
39-
⨅ S ∈ (𝓝 x).map f, ediam S
48+
noncomputable abbrev oscillationAt [TopologicalSpace E] (f : E → F) (x : E) : ENNReal :=
49+
oscillation f (𝓝 x)
4050

4151
/-- The oscillation of `f : E → F` within `D` at `x`. -/
42-
noncomputable def oscillationWithin [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) :
52+
noncomputable abbrev oscillationWithinAt [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) :
4353
ENNReal :=
44-
⨅ S ∈ (𝓝[D] x).map f, ediam S
54+
oscillation f (𝓝[D] x)
4555

4656
/-- The oscillation of `f` at `x` within a neighborhood `D` of `x` is equal to `oscillation f x` -/
47-
theorem oscillationWithin_nhds_eq_oscillation [TopologicalSpace E] (f : E → F) (D : Set E) (x : E)
48-
(hD : D ∈ 𝓝 x) : oscillationWithin f D x = oscillation f x := by
49-
rw [oscillation, oscillationWithin, nhdsWithin_eq_nhds.2 hD]
57+
theorem oscillationWithinAt_nhds_eq_oscillationAt [TopologicalSpace E] (f : E → F) (D : Set E)
58+
(x : E) (hD : D ∈ 𝓝 x) : oscillationWithinAt f D x = oscillationAt f x := by
59+
rw [oscillationAt, oscillationWithinAt, nhdsWithin_eq_nhds.2 hD]
5060

5161
/-- The oscillation of `f` at `x` within `univ` is equal to `oscillation f x` -/
52-
theorem oscillationWithin_univ_eq_oscillation [TopologicalSpace E] (f : E → F) (x : E) :
53-
oscillationWithin f univ x = oscillation f x :=
54-
oscillationWithin_nhds_eq_oscillation f univ x Filter.univ_mem
62+
theorem oscillationWithinAt_univ_eq_oscillationAt [TopologicalSpace E] (f : E → F) (x : E) :
63+
oscillationWithinAt f univ x = oscillationAt f x :=
64+
oscillationWithinAt_nhds_eq_oscillationAt f univ x Filter.univ_mem
5565

5666
namespace ContinuousWithinAt
5767

58-
theorem oscillationWithin_eq_zero [TopologicalSpace E] {f : E → F} {D : Set E}
59-
{x : E} (hf : ContinuousWithinAt f D x) : oscillationWithin f D x = 0 := by
68+
theorem oscillationWithinAt_eq_zero [TopologicalSpace E] {f : E → F} {D : Set E}
69+
{x : E} (hf : ContinuousWithinAt f D x) : oscillationWithinAt f D x = 0 := by
6070
rw [← nonpos_iff_eq_zero]
6171
refine _root_.le_of_forall_pos_le_add fun ε hε ↦ ?_
6272
rw [zero_add]
@@ -69,35 +79,36 @@ end ContinuousWithinAt
6979

7080
namespace ContinuousAt
7181

72-
theorem oscillation_eq_zero [TopologicalSpace E] {f : E → F} {x : E} (hf : ContinuousAt f x) :
73-
oscillation f x = 0 := by
82+
theorem oscillationAt_eq_zero [TopologicalSpace E] {f : E → F} {x : E} (hf : ContinuousAt f x) :
83+
oscillationAt f x = 0 := by
7484
rw [← continuousWithinAt_univ f x] at hf
75-
exact oscillationWithin_univ_eq_oscillation f x ▸ hf.oscillationWithin_eq_zero
85+
exact oscillationWithinAt_univ_eq_oscillationAt f x ▸ hf.oscillationWithinAt_eq_zero
7686

7787
end ContinuousAt
7888

79-
namespace OscillationWithin
89+
namespace OscillationWithinAt
8090

8191
/-- The oscillation within `D` of `f` at `x ∈ D` is 0 if and only if `ContinuousWithinAt f D x`. -/
8292
theorem eq_zero_iff_continuousWithinAt [TopologicalSpace E] (f : E → F) {D : Set E}
83-
{x : E} (xD : x ∈ D) : oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x := by
84-
refine ⟨fun hf ↦ EMetric.tendsto_nhds.mpr (fun ε ε0 ↦ ?_), fun hf ↦ hf.oscillationWithin_eq_zero⟩
85-
simp_rw [← hf, oscillationWithin, iInf_lt_iff] at ε0
93+
{x : E} (xD : x ∈ D) : oscillationWithinAt f D x = 0 ↔ ContinuousWithinAt f D x := by
94+
refine ⟨fun hf ↦ EMetric.tendsto_nhds.mpr (fun ε ε0 ↦ ?_),
95+
fun hf ↦ hf.oscillationWithinAt_eq_zero⟩
96+
simp_rw [← hf, oscillationWithinAt, oscillation, iInf_lt_iff] at ε0
8697
obtain ⟨S, hS, Sε⟩ := ε0
8798
refine Filter.mem_of_superset hS (fun y hy ↦ lt_of_le_of_lt ?_ Sε)
8899
exact edist_le_ediam_of_mem (mem_preimage.1 hy) <| mem_preimage.1 (mem_of_mem_nhdsWithin xD hS)
89100

90-
end OscillationWithin
101+
end OscillationWithinAt
91102

92-
namespace Oscillation
103+
namespace OscillationAt
93104

94105
/-- The oscillation of `f` at `x` is 0 if and only if `f` is continuous at `x`. -/
95106
theorem eq_zero_iff_continuousAt [TopologicalSpace E] (f : E → F) (x : E) :
96-
oscillation f x = 0 ↔ ContinuousAt f x := by
97-
rw [← oscillationWithin_univ_eq_oscillation, ← continuousWithinAt_univ f x]
98-
exact OscillationWithin.eq_zero_iff_continuousWithinAt f (mem_univ x)
107+
oscillationAt f x = 0 ↔ ContinuousAt f x := by
108+
rw [← oscillationWithinAt_univ_eq_oscillationAt, ← continuousWithinAt_univ f x]
109+
exact OscillationWithinAt.eq_zero_iff_continuousWithinAt f (mem_univ x)
99110

100-
end Oscillation
111+
end OscillationAt
101112

102113
namespace IsCompact
103114

@@ -106,7 +117,7 @@ variable {f : E → F} {D : Set E} {ε : ENNReal}
106117

107118
/-- If `oscillationWithin f D x < ε` at every `x` in a compact set `K`, then there exists `δ > 0`
108119
such that the oscillation of `f` on `ball x δ ∩ D` is less than `ε` for every `x` in `K`. -/
109-
theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscillationWithin f D x < ε) :
120+
theorem uniform_oscillationWithinAt (comp : IsCompact K) (hK : ∀ x ∈ K, oscillationWithinAt f D x < ε) :
110121
∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε := by
111122
let S := fun r ↦
112123
{x : E | ∃ (a : ℝ), (a > r ∧ ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε)}
@@ -120,8 +131,8 @@ theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscill
120131
rw [← ofReal_add (by linarith) (by linarith), sub_add_cancel]
121132
have S_cover : K ⊆ ⋃ r > 0, S r := by
122133
intro x hx
123-
have : oscillationWithin f D x < ε := hK x hx
124-
simp only [oscillationWithin, Filter.mem_map, iInf_lt_iff] at this
134+
have : oscillationWithinAt f D x < ε := hK x hx
135+
simp only [oscillationWithinAt, oscillation, Filter.mem_map, iInf_lt_iff] at this
125136
obtain ⟨n, hn₁, hn₂⟩ := this
126137
obtain ⟨r, r0, hr⟩ := EMetric.mem_nhdsWithin_iff.1 hn₁
127138
simp only [gt_iff_lt, mem_iUnion, exists_prop]
@@ -154,10 +165,164 @@ theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscill
154165
/-- If `oscillation f x < ε` at every `x` in a compact set `K`, then there exists `δ > 0` such
155166
that the oscillation of `f` on `ball x δ` is less than `ε` for every `x` in `K`. -/
156167
theorem uniform_oscillation {K : Set E} (comp : IsCompact K)
157-
{f : E → F} {ε : ENNReal} (hK : ∀ x ∈ K, oscillation f x < ε) :
168+
{f : E → F} {ε : ENNReal} (hK : ∀ x ∈ K, oscillationAt f x < ε) :
158169
∃ δ > 0, ∀ x ∈ K, ediam (f '' (eball x (ENNReal.ofReal δ))) ≤ ε := by
159-
simp only [← oscillationWithin_univ_eq_oscillation] at hK
160-
convert! ← comp.uniform_oscillationWithin hK
170+
simp only [← oscillationWithinAt_univ_eq_oscillationAt] at hK
171+
convert! ← comp.uniform_oscillationWithinAt hK
161172
exact inter_univ _
162173

163174
end IsCompact
175+
176+
section MoveMe
177+
178+
variable {ι : Sort*} {κ : ι → Sort*} {α : Type*} {f : (i : ι) → κ i → α}
179+
180+
@[to_dual iInf₂_le_iff]
181+
theorem le_iSup₂_iff [CompleteSemilatticeSup α] {a : α} :
182+
a ≤ ⨆ (i) (j), f i j ↔ ∀ b, (∀ i j, f i j ≤ b) → a ≤ b := by
183+
simp [iSup, le_sSup_iff, upperBounds]
184+
185+
@[to_dual iInf₂_lt_iff]
186+
theorem lt_iSup₂_iff [CompleteLinearOrder α] {a : α} :
187+
a < ⨆ (i) (j), f i j ↔ ∃ i j, a < f i j := by
188+
have := lt_iSup_iff (f := fun (ij : PSigma κ) ↦ f ij.1 ij.2) (a := a)
189+
simp_rw [PSigma.exists, iSup_psigma] at this
190+
exact this
191+
192+
@[to_dual iInf₂_le_iff_forall_lt]
193+
theorem le_iSup₂_iff_forall_lt [CompleteLinearOrder α] {l : α} :
194+
l ≤ ⨆ (i) (j), f i j ↔ ∀ b < l, ∃ i j, b < f i j := by
195+
have := le_iSup_iff_forall_lt (f := fun (ij : PSigma κ) ↦ f ij.1 ij.2) (l := l)
196+
simp_rw [PSigma.exists, iSup_psigma] at this
197+
exact this
198+
199+
@[to_dual lt_iInf₂_iff]
200+
theorem iSup₂_lt_iff [CompleteLattice α] {l : α} :
201+
⨆ (i) (j), f i j < l ↔ ∃ b < l, ∀ i j, f i j ≤ b := by
202+
have := iSup_lt_iff (f := fun (ij : PSigma κ) ↦ f ij.1 ij.2) (l := l)
203+
simp_rw [PSigma.forall, iSup_psigma] at this
204+
exact this
205+
206+
lemma mul_biInf {p : ι → Prop} (hp : ∃ i, p i) {a : ℝ≥0∞} {f : ι → ℝ≥0∞}
207+
(hinfty : a = ∞ → ⨅ (i) (_ : p i), f i = 0 → ∃ i, ∃ (_ : p i), f i = 0) :
208+
a * ⨅ (i) (_ : p i), f i = ⨅ (i) (_ : p i), a * f i := by
209+
haveI : Nonempty {i // p i} := nonempty_subtype.mpr hp
210+
have := mul_iInf (ι := {i // p i}) (a := a) (f := (f ·))
211+
simp_rw [iInf_subtype, Subtype.exists] at this
212+
exact this hinfty
213+
214+
@[to_dual iInf₂_eq_of_forall_ge_of_forall_gt_exists_lt]
215+
theorem iSup₂_eq_of_forall_le_of_forall_lt_exists_gt [CompleteLattice α] {b : α}
216+
(h₁ : ∀ i j, f i j ≤ b) (h₂ : ∀ w, w < b → ∃ i j, w < f i j) : ⨆ (i) (j), f i j = b := by
217+
have := iSup_eq_of_forall_le_of_forall_lt_exists_gt
218+
(f := fun (ij : PSigma κ) ↦ f ij.1 ij.2) (b := b)
219+
simp_rw [PSigma.forall, PSigma.exists, iSup_psigma] at this
220+
exact this h₁ h₂
221+
222+
end MoveMe
223+
224+
section Cauchy
225+
226+
variable {f : E → F}
227+
228+
theorem EMetric.cauchy_iff_iInf_ediam_eq_zero (l : Filter F) [NeBot l] :
229+
Cauchy l ↔ ⨅ s ∈ l, ediam s = 0 := by
230+
rw [EMetric.cauchy_iff, ←nonpos_iff_eq_zero, iInf₂_le_iff_forall_lt]
231+
constructor
232+
· intro h ε hε
233+
rcases exists_between hε with ⟨η, hη⟩
234+
rcases h.right η hη.1 with ⟨s, hs₁, hs₂⟩
235+
use s, hs₁
236+
apply iSup₂_lt_iff.mpr
237+
use η, hη.2
238+
intro i hi
239+
apply iSup₂_le_iff.mpr
240+
intro j hj
241+
exact hs₂ i hi j hj |>.le
242+
· intro h
243+
use NeBot.ne'
244+
intro ε hε
245+
rcases h ε hε with ⟨s, hs₁, hs₂⟩
246+
use s, hs₁
247+
intro i hi j hj
248+
rcases iSup₂_lt_iff.mp hs₂ with ⟨l, hl, hs₃⟩
249+
specialize hs₃ i hi
250+
exact iSup₂_le_iff.mp hs₃ j hj |>.trans_lt hl
251+
252+
theorem cauchy_iff_oscillation_eq_zero (l : Filter E) [NeBot l] :
253+
Cauchy (l.map f) ↔ oscillation f l = 0 :=
254+
EMetric.cauchy_iff_iInf_ediam_eq_zero _
255+
256+
/-- A function `f` whose domain is a complete `EMetric` space converges to a point along a filter if
257+
and only if its oscillation along `l` is equal to zero. -/
258+
theorem EMetric.tendsTo_nhds_iff_oscillation_eq_zero [CompleteSpace F] (l : Filter E) [NeBot l] :
259+
(∃ x, Tendsto f l (𝓝 x)) ↔ oscillation f l = 0 := by
260+
rw [←cauchy_map_iff_exists_tendsto]
261+
exact cauchy_iff_oscillation_eq_zero _
262+
263+
end Cauchy
264+
265+
section Lipschitz
266+
267+
variable {α β γ : Type*} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ]
268+
269+
theorem LipschitzWith.oscillation_comp₂_le (g : α → β → γ) (f₁ : E → α) (f₂ : E → β)
270+
{K₁ K₂ : NNReal} (l : Filter E)
271+
(hf₁ : ∀ b, LipschitzWith K₁ (g · b)) (hf₂ : ∀ a, LipschitzWith K₂ (g a ·)) :
272+
oscillation (fun a ↦ g (f₁ a) (f₂ a)) l
273+
≤ ↑K₁ * oscillation f₁ l + ↑K₂ * oscillation f₂ l := by
274+
unfold oscillation
275+
simp_rw [mul_biInf ⟨_, Filter.univ_mem⟩ (coe_ne_top · |>.elim)]
276+
-- this would be more convenient with a `setm` tactic
277+
set a := ⨅ i ∈ map f₁ l, ↑K₁ * ediam i
278+
set b := ⨅ i ∈ map f₂ l, ↑K₂ * ediam i
279+
by_cases! ha : a = ∞; · simp [ha]
280+
by_cases! hb : b = ∞; · simp [hb]
281+
apply _root_.le_of_forall_pos_le_add
282+
intro ε hε
283+
rcases iInf₂_le_iff_forall_lt (l := a) |>.mp le_rfl (a + ε / 2)
284+
(lt_add_right ha (by norm_num [hε.ne'])) with ⟨sa, hsa, hsa'⟩
285+
rcases iInf₂_le_iff_forall_lt (l := b) |>.mp le_rfl (b + ε / 2)
286+
(lt_add_right hb (by norm_num [hε.ne'])) with ⟨sb, hsb, hsb'⟩
287+
rw [show a + b + ε = a + ε / 2 + (b + ε / 2) by
288+
ring_nf
289+
rw [ENNReal.div_mul_cancel (by positivity) (by finiteness)]]
290+
apply ENNReal.add_lt_add hsa' hsb' |>.trans_le' _ |>.le
291+
apply iInf₂_le_of_le (image2 g sa sb) _ _
292+
· rw [mem_map] at ⊢ hsa hsb
293+
exact l.mem_of_superset (l.inter_mem hsa hsb) fun a ⟨h₁, h₂⟩ ↦ ⟨f₁ a, h₁, f₂ a, h₂, rfl⟩
294+
· exact LipschitzOnWith.ediam_image2_le _ _ _
295+
(fun s _ ↦ hf₁ s |>.lipschitzOnWith)
296+
(fun s _ ↦ hf₂ s |>.lipschitzOnWith)
297+
298+
end Lipschitz
299+
300+
section SeminormedAddCommGroup
301+
302+
variable {F : Type*} [SeminormedCommGroup F]
303+
304+
@[to_additive]
305+
theorem oscillation_mul_le (f₁ : E → F) (f₂ : E → F) (l : Filter E) :
306+
oscillation (f₁ * f₂) l ≤ oscillation f₁ l + oscillation f₂ l :=
307+
LipschitzWith.oscillation_comp₂_le (· * ·) f₁ f₂ l
308+
(fun _ => (isometry_mul_right _).lipschitz)
309+
(fun _ => (isometry_mul_left _).lipschitz)
310+
|>.trans_eq (by simp only [coe_one, one_mul])
311+
312+
@[to_additive]
313+
theorem oscillation_le_add_div (f₁ : E → F) (f₂ : E → F) (l : Filter E) :
314+
oscillation f₁ l ≤ oscillation f₂ l + oscillation (f₁ / f₂) l := by
315+
nth_rw 1 [show f₁ = f₂ * (f₁ / f₂) by simp]
316+
exact oscillation_mul_le ..
317+
318+
@[to_additive oscillation_le_two_mul_iSup_enorm]
319+
theorem oscillation_le_two_mul_iSup_enorm' (f : E → F) (l : Filter E) :
320+
oscillation f l ≤ 2 * iSup (‖f ·‖ₑ) := by
321+
apply oscillation_le_ediam_range.trans
322+
refine ediam_le fun x hx y hy => ?_
323+
rw [edist_eq_enorm_div x y, two_mul]
324+
apply enorm_div_le.trans <| add_le_add _ _
325+
· exact hx.out.elim fun z hz ↦ hz ▸ le_iSup (‖f ·‖ₑ) ..
326+
· exact hy.out.elim fun z hz ↦ hz ▸ le_iSup (‖f ·‖ₑ) ..
327+
328+
end SeminormedAddCommGroup

0 commit comments

Comments
 (0)