sup metric convergence is uniform convergence

Stream: Is there code for X?

[Jireh Loreaux]

We don't have this, right? Do we want it?

import topology.continuous_function.bounded

open filter metric set bounded_continuous_function
open_locale topological_space bounded_continuous_function

variables {α β ι : Type*} [topological_space α] [metric_space β]

lemma tendsto_dist_iff_tendsto_uniformly {F : ι → (α →ᵇ β)} {f : α →ᵇ β} {l : filter ι} :
  tendsto (λ i, dist f (F i)) l (𝓝 0) ↔ tendsto_uniformly (λ i, F i) f l :=
begin
  refine iff.intro (λ h u hu, _) (λ h, metric.tendsto_nhds.mpr $ λ ε ε_pos,
    (h _ (dist_mem_uniformity $ half_pos ε_pos)).mp (eventually_of_forall $ λ n hn, _)),
  { rcases mem_uniformity_dist.mp hu with ⟨ε, ε_pos, hε⟩,
    refine (tendsto_iff_forall_eventually_mem.mp h (ball 0 ε) (ball_mem_nhds _ ε_pos)).mp
      (eventually_of_forall $ λ n hn x, hε $ lt_of_le_of_lt (dist_coe_le_dist x) _),
    simpa [real.norm_of_nonneg dist_nonneg] using hn },
  { simp only [mem_set_of_eq, dist_zero_right, real.norm_of_nonneg dist_nonneg],
    exact lt_of_le_of_lt ((dist_le (half_pos ε_pos).le).mpr $ λ x, le_of_lt $ hn x)
      (half_lt_self ε_pos), }
end

[Jireh Loreaux]

sorry, I should have rephrased the lhs as tendsto F l (𝓝 f)

[Heather Macbeth]

I think this can be two more restricted lemmas:

lemma tendsto_dist_iff {F : ι → β} {f : β} {l : filter ι} :
  tendsto (λ i, dist f (F i)) l (𝓝 0) ↔ tendsto F l (𝓝 f) :=
sorry

lemma bounded_continuous_function.tendsto_iff_tendsto_uniformly
  {F : ι → (α →ᵇ β)} {f : α →ᵇ β} {l : filter ι} :
  tendsto F l (𝓝 f) ↔ tendsto_uniformly (λ i, F i) f l :=
sorry

[Jireh Loreaux]

I mean, the first one is silly, and we likely already have it, I actually meant to write the second one, I just wasn't thinking when I originally typed it up.

[Heather Macbeth]

Ah, the first one is docs#tendsto_iff_dist_tendsto_zero

[Heather Macbeth]

For the second one, docs#continuous_map.tendsto_iff_tendsto_uniformly ?

[Heather Macbeth]

That's a little different, in fact -- for continuous functions on compact spaces, not for bounded continuous on arbitrary spaces.

[Heather Macbeth]

So yes, I guess it's missing!