## Stream: maths

### Topic: uniform_continuous_on

#### Patrick Massot (Jun 17 2020 at 10:27):

I notice that we don't have uniform_continuous_on. Should we? I'm still hunting down stupid holes from https://leanprover-community.github.io/undergrad_todo.html and I wrote:

import topology.instances.real

open_locale topological_space
open_locale filter

open set filter

variables {α β γ δ : Type*}

lemma filter.tendsto.prod_map {f : α → γ} {g : β → δ} {a : filter α} {b : filter β}
{c : filter γ} {d : filter δ} (hf : tendsto f a c) (hg : tendsto g b d) :
tendsto (λ x : α × β, (f x.1, g x.2)) (a ×ᶠ b) (c ×ᶠ d) :=
begin
rw [tendsto, ← prod_map_map_eq],
exact filter.prod_mono hf hg,
end

variables [topological_space α] [topological_space β] [topological_space γ]
[topological_space δ]

lemma continuous_within_at.prod_map {f : α → γ} {g : β → δ} {s : set α} {t : set β}
{x : α} {y : β} (hx : x ∈ s) (hy : y ∈ t)
(hf : continuous_within_at f s x) (hg : continuous_within_at g t y) :
continuous_within_at (λ (x : α × β), (f x.fst, g x.snd)) (s.prod t) (x, y) :=
begin
unfold continuous_within_at at *,
rw [nhds_within_prod_eq, nhds_prod_eq],
exact hf.prod_map hg,
end

lemma continuous_on.prod_map {f : α → γ} {g : β → δ} {s : set α} {t : set β}
(hf : continuous_on f s) (hg : continuous_on g t) :
continuous_on (λ x : α × β, (f x.1, g x.2)) (set.prod s t) :=
λ ⟨x, y⟩ ⟨hx, hy⟩, continuous_within_at.prod_map hx hy (hf x hx) (hg y hy)

lemma is_closed_le_on [preorder α] [order_closed_topology α] {f g : β → α} {s : set β}
(hf : continuous_on f s) (hg : continuous_on g s) (hs : is_closed s) :
is_closed {b | b ∈ s ∧ f b ≤ g b} :=
(hf.prod hg).preimage_closed_of_closed hs order_closed_topology.is_closed_le'

lemma compact.uniform_continuous_on {X : Type*} [metric_space X]
{s : set X} (hs : compact s) {f : X → ℝ} (hf : continuous_on f s) :
∀ ε > 0, ∃ δ > 0, ∀ x y ∈ s, dist x y < δ → dist (f x) (f y) < ε :=
begin
classical,
by_cases hs' : s.nonempty,
{ intros ε ε_pos,
let φ : X × X → ℝ := λ p, dist (f p.1) (f p.2),
have φ_cont : continuous_on φ (set.prod s s) :=
continuous_dist.comp_continuous_on (hf.prod_map hf),
set K := { p : X × X | p ∈ set.prod s s ∧ ε ≤ φ p },
have : is_closed K :=
is_closed_le_on continuous_const.continuous_on φ_cont (closed_of_compact _ \$ hs.prod hs),
have K_cpct : compact K :=
compact_of_is_closed_subset (hs.prod hs) this (λ p hp, hp.1),
by_cases hK : K.nonempty,
{ rcases K_cpct.exists_forall_le hK continuous_dist.continuous_on with ⟨⟨x₀, y₀⟩, xy₀_in, H⟩,
use dist x₀ y₀,
split,
{ change _ < _,
rw dist_pos,
intro h,
have ineq := xy₀_in.2,
dsimp [φ] at ineq,
rw [h, dist_self] at ineq,
linarith },
{ intros x y x_in y_in hxy,
replace H : ∀ (a b : X), a ∈ s → b ∈ s → ε ≤ φ (a, b) → dist x₀ y₀ ≤ dist a b,
by simpa using H,
by_contra h,
push_neg at h,
linarith [H x y x_in y_in h] } },
{ use [1, zero_lt_one],
intros x y x_in y_in hxy,
rw not_nonempty_iff_eq_empty at hK,
have : (x, y) ∉ K, by simp [hK],
have : x ∈ s → y ∈ s → φ (x, y) < ε, by simpa [K],
exact this x_in y_in }, },
{ rw not_nonempty_iff_eq_empty at hs',
intros ε ε_pos,
use [1, zero_lt_one],
intros x y x_in,
exfalso,
rwa hs' at x_in },
end


Note that the preliminary lemmas are also surprising holes, did I miss stuff?

#### Patrick Massot (Jun 17 2020 at 10:28):

@Sebastien Gouezel and @Yury G. Kudryashov

#### Yury G. Kudryashov (Jun 17 2020 at 13:03):

is_closed_le_on exists as is_closed.is_closed_le. Feel free to add an alias and/or replace the proof with yours. It would be nice to have a definition of uniform_continuous_on in a uniform_space related both to uniform_continuous and tendsto_uniformly_on. Do you need a metric_space in this lemma?

#### Patrick Massot (Jun 17 2020 at 13:24):

Thanks. It's strange that I missed is_closed.is_closed_le since I was clearly searching in the correct file. Trying to think about a version of Heine-Cantor in uniform spaces was also on my TODO list.

#### Yury G. Kudryashov (Jun 17 2020 at 14:33):

AFAIR, one can start with "tendsto implies tendsto_uniformly", then get uniform continuity as a particular case.

#### Patrick Massot (Jun 17 2020 at 14:58):

I don't know why I wasted time this morning. Bourbaki does this Heine theorem in uniform spaces from the beginning. I'll redo things properly.

Last updated: May 11 2021 at 16:22 UTC