English
If a compact set K is such that oscillationWithin f D x is uniformly below ε for all x ∈ K, then there exists δ>0 so that the diameter of f on ball x(δ) ∩ D is ≤ ε for all x ∈ K.
Русский
Пусть K компактно, и для всех x∈K имеют oscillationWithin f D x < ε. Тогда существует δ>0, такое что на шаре x(δ) ∩ D диаметр образа f не превышает ε для всех x∈K.
LaTeX
$$$\\text{IsCompact } K \\Rightarrow (\\forall x\\in K, \\operatorname{oscillationWithin}(f,D,x)<\\varepsilon) \\Rightarrow \\exists \\delta>0, \\forall x\\in K,\\ \\operatorname{diam}(f''(\\ball{x}{\\delta}\\cap D))\\le \\varepsilon$$$
Lean4
/-- 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 < ε) :
∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ) ∩ D)) ≤ ε :=
by
let S := fun r ↦ {x : E | ∃ (a : ℝ), (a > r ∧ diam (f '' (ball x (ENNReal.ofReal a) ∩ D)) ≤ ε)}
have S_open : ∀ r > 0, IsOpen (S r) :=
by
refine fun r _ ↦ isOpen_iff.mpr fun x ⟨a, ar, ha⟩ ↦ ⟨ENNReal.ofReal ((a - r) / 2), by simp [ar], ?_⟩
refine fun y hy ↦ ⟨a - (a - r) / 2, by linarith, le_trans (diam_mono (image_mono fun z hz ↦ ?_)) ha⟩
refine ⟨lt_of_le_of_lt (edist_triangle z y x) (lt_of_lt_of_eq (ENNReal.add_lt_add hz.1 hy) ?_), hz.2⟩
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
obtain ⟨n, hn₁, hn₂⟩ := this
obtain ⟨r, r0, hr⟩ := mem_nhdsWithin_iff.1 hn₁
simp only [gt_iff_lt, mem_iUnion, exists_prop]
have : ∀ r', (ENNReal.ofReal r') ≤ r → diam (f '' (ball x (ENNReal.ofReal r') ∩ D)) ≤ ε :=
by
intro r' hr'
grw [← hn₂, ← image_subset_iff.2 hr, hr']
by_cases r_top : r = ⊤
· use 1, one_pos, 2, one_lt_two, this 2 (by simp only [r_top, le_top])
· obtain ⟨r', hr'⟩ := exists_between (toReal_pos (ne_of_gt r0) r_top)
use r', hr'.1, r.toReal, hr'.2, this r.toReal ofReal_toReal_le
have S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁ := fun r₁ r₂ hr x ⟨a, ar₂, ha⟩ ↦ ⟨a, lt_of_le_of_lt hr ar₂, ha⟩
obtain ⟨δ, δ0, hδ⟩ : ∃ r > 0, K ⊆ S r :=
by
obtain ⟨T, Tb, Tfin, hT⟩ := comp.elim_finite_subcover_image S_open S_cover
by_cases T_nonempty : T.Nonempty
· use Tfin.isWF.min T_nonempty, Tb (Tfin.isWF.min_mem T_nonempty)
intro x hx
obtain ⟨r, hr⟩ := mem_iUnion.1 (hT hx)
simp only [mem_iUnion, exists_prop] at hr
exact (S_antitone _ r (IsWF.min_le Tfin.isWF T_nonempty hr.1)) hr.2
· rw [not_nonempty_iff_eq_empty] at T_nonempty
use 1, one_pos, subset_trans hT (by simp [T_nonempty])
use δ, δ0
intro x xK
obtain ⟨a, δa, ha⟩ := hδ xK
grw [← ha]
gcongr
