uniform_continuous_on

Stream: maths

[Patrick Massot]

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]

@Sebastien Gouezel and @Yury G. Kudryashov

[Yury G. Kudryashov]

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]

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]

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

[Patrick Massot]

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.