feat(topology/uniform_space/uniform_convergence): add tendsto_uniformly_iff_seq_tendsto_uniformly (#13128)

For countably generated filters, uniform convergence is equivalent to uniform convergence of sub-sequences.



Co-authored-by: RemyDegenne <Remydegenne@gmail.com>

Author: kex-y

src/order/filter/at_top_bot.lean

@@ -1329,6 +1329,17 @@ begin
     exact hx_tendsto hx_freq, },
 end
 
+lemma eventually_iff_seq_eventually {ι : Type*} {l : filter ι} {p : ι → Prop}
+  [hl : l.is_countably_generated] :
+  (∀ᶠ n in l, p n) ↔ ∀ (x : ℕ → ι), tendsto x at_top l → ∀ᶠ (n : ℕ) in at_top, p (x n) :=
+begin
+  have : (∀ᶠ n in l, p n) ↔ ¬ ∃ᶠ n in l, ¬(p n),
+  { rw not_frequently, simp_rw not_not, },
+  rw [this, frequently_iff_seq_frequently],
+  push_neg,
+  simp_rw [not_frequently, not_not],
+end
+
 lemma subseq_forall_of_frequently {ι : Type*} {x : ℕ → ι} {p : ι → Prop} {l : filter ι}
   (h_tendsto : tendsto x at_top l) (h : ∃ᶠ n in at_top, p (x n)) :
   ∃ ns : ℕ → ℕ, tendsto (λ n, x (ns n)) at_top l ∧ ∀ n, p (x (ns n)) :=

src/order/filter/bases.lean

@@ -693,6 +693,21 @@ begin
     exact ⟨⟨i, i⟩, ⟨hi, hi⟩, h⟩ },
 end
 
+lemma has_antitone_basis.prod {f : filter α} {g : filter β}
+  {s : ℕ → set α} {t : ℕ → set β} (hf : has_antitone_basis f s) (hg : has_antitone_basis g t) :
+  has_antitone_basis (f ×ᶠ g) (λ n, s n ×ˢ t n) :=
+begin
+  have h : has_basis (f ×ᶠ g) _ _ := has_basis.prod' hf.to_has_basis hg.to_has_basis _,
+  swap,
+  { intros i j,
+    simp only [true_and, forall_true_left],
+    exact ⟨max i j, hf.antitone (le_max_left _ _), hg.antitone (le_max_right _ _)⟩, },
+  refine ⟨h, λ n m hn_le_m, _⟩,
+  intros x hx,
+  rw mem_prod at hx ⊢,
+  exact ⟨hf.antitone hn_le_m hx.1, hg.antitone hn_le_m hx.2⟩,
+end
+
 end two_types
 
 open equiv
@@ -888,4 +903,14 @@ by { rw ← principal_singleton, exact is_countably_generated_principal _, }
 @[instance] lemma is_countably_generated_top : is_countably_generated (⊤ : filter α) :=
 @principal_univ α ▸ is_countably_generated_principal _
 
+instance is_countably_generated.prod {f : filter α} {g : filter β}
+  [hf : f.is_countably_generated] [hg : g.is_countably_generated] :
+  is_countably_generated (f ×ᶠ g) :=
+begin
+  simp_rw is_countably_generated_iff_exists_antitone_basis at hf hg ⊢,
+  rcases hf with ⟨s, hs⟩,
+  rcases hg with ⟨t, ht⟩,
+  refine ⟨_, hs.prod ht⟩,
+end
+
 end filter

src/topology/uniform_space/uniform_convergence.lean

@@ -195,6 +195,55 @@ lemma uniform_continuous₂.tendsto_uniformly [uniform_space α] [uniform_space
 uniform_continuous_on.tendsto_uniformly univ_mem $
   by rwa [univ_prod_univ, uniform_continuous_on_univ]
 
+section seq_tendsto
+
+lemma tendsto_uniformly_on_of_seq_tendsto_uniformly_on {l : filter ι} [l.is_countably_generated]
+  (h : ∀ u : ℕ → ι, tendsto u at_top l → tendsto_uniformly_on (λ n, F (u n)) f at_top s) :
+  tendsto_uniformly_on F f l s :=
+begin
+  rw [tendsto_uniformly_on_iff_tendsto, tendsto_iff_seq_tendsto],
+  intros u hu,
+  rw tendsto_prod_iff' at hu,
+  specialize h (λ n, (u n).fst) hu.1,
+  rw tendsto_uniformly_on_iff_tendsto at h,
+  have : ((λ (q : ι × α), (f q.snd, F q.fst q.snd)) ∘ u)
+    = (λ (q : ℕ × α), (f q.snd, F ((λ (n : ℕ), (u n).fst) q.fst) q.snd)) ∘ (λ n, (n, (u n).snd)),
+  { ext1 n, simp, },
+  rw this,
+  refine tendsto.comp h _,
+  rw tendsto_prod_iff',
+  exact ⟨tendsto_id, hu.2⟩,
+end
+
+lemma tendsto_uniformly_on.seq_tendsto_uniformly_on {l : filter ι}
+  (h : tendsto_uniformly_on F f l s) (u : ℕ → ι) (hu : tendsto u at_top l) :
+  tendsto_uniformly_on (λ n, F (u n)) f at_top s :=
+begin
+  rw tendsto_uniformly_on_iff_tendsto at h ⊢,
+  have : (λ (q : ℕ × α), (f q.snd, F (u q.fst) q.snd))
+    = (λ (q : ι × α), (f q.snd, F q.fst q.snd)) ∘ (λ p : ℕ × α, (u p.fst, p.snd)),
+  { ext1 x, simp, },
+  rw this,
+  refine h.comp _,
+  rw tendsto_prod_iff',
+  exact ⟨hu.comp tendsto_fst, tendsto_snd⟩,
+end
+
+lemma tendsto_uniformly_on_iff_seq_tendsto_uniformly_on {l : filter ι} [l.is_countably_generated] :
+  tendsto_uniformly_on F f l s
+    ↔ ∀ u : ℕ → ι, tendsto u at_top l → tendsto_uniformly_on (λ n, F (u n)) f at_top s :=
+⟨tendsto_uniformly_on.seq_tendsto_uniformly_on, tendsto_uniformly_on_of_seq_tendsto_uniformly_on⟩
+
+lemma tendsto_uniformly_iff_seq_tendsto_uniformly {l : filter ι} [l.is_countably_generated] :
+  tendsto_uniformly F f l
+    ↔ ∀ u : ℕ → ι, tendsto u at_top l → tendsto_uniformly (λ n, F (u n)) f at_top :=
+begin
+  simp_rw ← tendsto_uniformly_on_univ,
+  exact tendsto_uniformly_on_iff_seq_tendsto_uniformly_on,
+end
+
+end seq_tendsto
+
 variable [topological_space α]
 
 /-- A sequence of functions `Fₙ` converges locally uniformly on a set `s` to a limiting function