Convergence of uniform limit

Stream: Is there code for X?

[Vincent Beffara]

Is this somewhere in Mathlib (probably in much higher generality)?

import Mathlib
open Topology Filter

example {F : ℕ → ℝ → ℝ} {f : ℝ → ℝ}
    (h1 : TendstoUniformly F f atTop)
    (h2 : ∀ n, Tendsto (F n) atTop (𝓝 0)) :
    Tendsto f atTop (𝓝 0) :=
  sorry

It tastes a bit like docs#TendstoUniformly.continuous but I couldn't find it.

[Anatole Dedecker]

The closest I can find is docs#TendstoUniformlyOnFilter.tendsto_at

[Vincent Beffara]

Here is what I ended up with:

import Mathlib

open Topology Filter Uniformity

variable {ι α β : Type*} [UniformSpace β] {l : Filter ι} [NeBot l] {p : Filter α} {b : β}

example {F : ι → α → β} {f : α → β} {L : ι → β} {ℓ : β}
    (h1 : TendstoUniformlyOnFilter F f l p)
    (h2 : ∀ᶠ i in l, Tendsto (F i) p (𝓝 (L i)))
    (h3 : Tendsto L l (𝓝 ℓ)) :
    Tendsto f p (𝓝 ℓ) := by

  -- Rewrite the convergence in terms of uniformities
  rw [Uniform.tendsto_nhds_left]
  intro s hs
  change ∀ᶠ x in p, (f x, ℓ) ∈ s

  -- Cut the uniformity in three parts
  obtain ⟨t, ht, hts⟩ := comp3_mem_uniformity hs

  -- First part : make `L i` `t`-close to `ℓ`
  have l1 : ∀ᶠ i in l, (L i, ℓ) ∈ t := by
    rw [Uniform.tendsto_nhds_left] at h3
    exact h3 ht

  -- Second part : make `F i` `t`-close to `L i`
  have l2 : ∀ᶠ i in l, ∀ᶠ x in p, (F i x, L i) ∈ t := by
    filter_upwards [h2] with i h2
    rw [Uniform.tendsto_nhds_left] at h2
    exact h2 ht

  -- Third part : make `F i x` close to `f x`
  have l3 : ∀ᶠ i in l, ∀ᶠ x in p, (f x, F i x) ∈ t := by
    obtain ⟨p1, r1, p2, r2, h1⟩ := eventually_prod_iff.mp (h1 t ht)
    filter_upwards [r1] with i r1
    filter_upwards [r2] with x r2
    exact h1 r1 r2

  -- Combine the three parts
  obtain ⟨i, l4, l5, l6⟩ := (l1.and (l2.and l3)).exists
  filter_upwards [l5, l6] with x l5 l6
  exact hts ⟨F i x, l6, L i, l5, l4⟩

It can probably be golfed down to a one-liner, but it was fun to do :-)

[Vincent Beffara]

Any hint about making this nicer?