Zulip Chat Archive

Stream: maths

Topic: uniform_continuous_on


view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jun 17 2020 at 10:28):

@Sebastien Gouezel and @Yury G. Kudryashov

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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