feat(topology/uniform_space/uniform_convergence): tendsto_uniformly_o…

…n_filter (#15871)

Currently, mathlib supports several notions of uniform convergence (e.g., tendsto_uniformly_on). These are "global" versions of a more local notion, which we call tendsto_uniformly_on_filter. Specifically, as revealed by tendsto_prod_top_iff is that uniform convergence means convergence on a product filter. So why can't you have a more general filter than a principal filter?

There's no reason you can't! Indeed, if you replace 𝓟 s with 𝓝 x you get a notion of "local uniform convergence" which is enough to prove, e.g., the derivative operator at a point commutes with the pointwise limit.

src/order/filter/prod.lean

@@ -94,6 +94,10 @@ begin
   simp only [mem_univ, forall_true_left]
 end
 
+lemma eventually_prod_principal_iff {p : α × β → Prop} {s : set β} :
+  (∀ᶠ (x : α × β) in (f ×ᶠ (𝓟 s)), p x) ↔ ∀ᶠ (x : α) in f, ∀ (y : β), y ∈ s → p (x, y) :=
+by { rw [eventually_iff, eventually_iff, mem_prod_principal], simp only [mem_set_of_eq], }
+
 lemma comap_prod (f : α → β × γ) (b : filter β) (c : filter γ) :
   comap f (b ×ᶠ c) = (comap (prod.fst ∘ f) b) ⊓ (comap (prod.snd ∘ f) c) :=
 by erw [comap_inf, filter.comap_comap, filter.comap_comap]
@@ -166,6 +170,26 @@ begin
   apply (ht.and hs).mono (λ x hx, hst hx.1 hx.2),
 end
 
+lemma eventually.diag_of_prod_left {f : filter α} {g : filter γ}
+  {p : (α × α) × γ → Prop} :
+  (∀ᶠ x in (f ×ᶠ f ×ᶠ g), p x) →
+  (∀ᶠ (x : α × γ) in (f ×ᶠ g), p ((x.1, x.1), x.2)) :=
+begin
+  intros h,
+  obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h,
+  refine (ht.diag_of_prod.prod_mk hs).mono (λ x hx, by simp only [hst hx.1 hx.2, prod.mk.eta]),
+end
+
+lemma eventually.diag_of_prod_right {f : filter α} {g : filter γ}
+  {p : α × γ × γ → Prop} :
+  (∀ᶠ x in (f ×ᶠ (g ×ᶠ g)), p x) →
+  (∀ᶠ (x : α × γ) in (f ×ᶠ g), p (x.1, x.2, x.2)) :=
+begin
+  intros h,
+  obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h,
+  refine (ht.prod_mk hs.diag_of_prod).mono (λ x hx, by simp only [hst hx.1 hx.2, prod.mk.eta]),
+end
+
 lemma tendsto_diag : tendsto (λ i, (i, i)) f (f ×ᶠ f) :=
 tendsto_iff_eventually.mpr (λ _ hpr, hpr.diag_of_prod)
 
@@ -181,6 +205,14 @@ by { rw [filter.prod, comap_infi, inf_infi], simp only [filter.prod, eq_self_iff
   f₁ ×ᶠ g₁ ≤ f₂ ×ᶠ g₂ :=
 inf_le_inf (comap_mono hf) (comap_mono hg)
 
+lemma prod_mono_left (g : filter β) {f₁ f₂ : filter α} (hf : f₁ ≤ f₂) :
+  f₁ ×ᶠ g ≤ f₂ ×ᶠ g :=
+filter.prod_mono hf rfl.le
+
+lemma prod_mono_right (f : filter α) {g₁ g₂ : filter β} (hf : g₁ ≤ g₂) :
+  f ×ᶠ g₁ ≤ f ×ᶠ g₂ :=
+filter.prod_mono rfl.le hf
+
 lemma {u v w x} prod_comap_comap_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
   {f₁ : filter α₁} {f₂ : filter α₂} {m₁ : β₁ → α₁} {m₂ : β₂ → α₂} :
   (comap m₁ f₁) ×ᶠ (comap m₂ f₂) = comap (λ p : β₁×β₂, (m₁ p.1, m₂ p.2)) (f₁ ×ᶠ f₂) :=
@@ -193,6 +225,10 @@ by simp only [filter.prod, comap_comap, (∘), inf_comm, prod.fst_swap,
 lemma prod_comm : f ×ᶠ g = map (λ p : β×α, (p.2, p.1)) (g ×ᶠ f) :=
 by { rw [prod_comm', ← map_swap_eq_comap_swap], refl }
 
+lemma eventually_swap_iff {p : (α × β) → Prop} : (∀ᶠ (x : α × β) in (f ×ᶠ g), p x) ↔
+  ∀ᶠ (y : β × α) in (g ×ᶠ f), p y.swap :=
+by { rw [prod_comm, eventually_map], simpa, }
+
 lemma prod_assoc (f : filter α) (g : filter β) (h : filter γ) :
   map (equiv.prod_assoc α β γ) ((f ×ᶠ g) ×ᶠ h) = f ×ᶠ (g ×ᶠ h) :=
 by simp_rw [← comap_equiv_symm, filter.prod, comap_inf, comap_comap, inf_assoc, function.comp,

src/topology/algebra/uniform_group.lean

@@ -330,7 +330,19 @@ uniform_continuous_inv.comp_cauchy_seq h
   by simp [← preimage_smul_inv, preimage]
 
 section uniform_convergence
-variables {ι : Type*} {l : filter ι} {f f' : ι → β → α} {g g' : β → α} {s : set β}
+variables {ι : Type*} {l : filter ι} {l' : filter β} {f f' : ι → β → α} {g g' : β → α} {s : set β}
+
+@[to_additive] lemma tendsto_uniformly_on_filter.mul (hf : tendsto_uniformly_on_filter f g l l')
+  (hf' : tendsto_uniformly_on_filter f' g' l l') :
+  tendsto_uniformly_on_filter (f * f') (g * g') l l' :=
+λ u hu, ((uniform_continuous_mul.comp_tendsto_uniformly_on_filter
+  (hf.prod hf')) u hu).diag_of_prod_left
+
+@[to_additive] lemma tendsto_uniformly_on_filter.div (hf : tendsto_uniformly_on_filter f g l l')
+  (hf' : tendsto_uniformly_on_filter f' g' l l') :
+  tendsto_uniformly_on_filter (f / f') (g / g') l l' :=
+λ u hu, ((uniform_continuous_div.comp_tendsto_uniformly_on_filter
+  (hf.prod hf')) u hu).diag_of_prod_left
 
 @[to_additive] lemma tendsto_uniformly_on.mul (hf : tendsto_uniformly_on f g l s)
   (hf' : tendsto_uniformly_on f' g' l s) : tendsto_uniformly_on (f * f') (g * g') l s :=
@@ -340,6 +352,14 @@ variables {ι : Type*} {l : filter ι} {f f' : ι → β → α} {g g' : β →
   (hf' : tendsto_uniformly_on f' g' l s) : tendsto_uniformly_on (f / f') (g / g') l s :=
 λ u hu, ((uniform_continuous_div.comp_tendsto_uniformly_on (hf.prod hf')) u hu).diag_of_prod
 
+@[to_additive] lemma tendsto_uniformly.mul (hf : tendsto_uniformly f g l)
+  (hf' : tendsto_uniformly f' g' l) : tendsto_uniformly (f * f') (g * g') l :=
+λ u hu, ((uniform_continuous_mul.comp_tendsto_uniformly (hf.prod hf')) u hu).diag_of_prod
+
+@[to_additive] lemma tendsto_uniformly.div (hf : tendsto_uniformly f g l)
+  (hf' : tendsto_uniformly f' g' l) : tendsto_uniformly (f / f') (g / g') l :=
+λ u hu, ((uniform_continuous_div.comp_tendsto_uniformly (hf.prod hf')) u hu).diag_of_prod
+
 @[to_additive] lemma uniform_cauchy_seq_on.mul (hf : uniform_cauchy_seq_on f l s)
   (hf' : uniform_cauchy_seq_on f' l s) : uniform_cauchy_seq_on (f * f') l s :=
 λ u hu, by simpa using ((uniform_continuous_mul.comp_uniform_cauchy_seq_on (hf.prod' hf')) u hu)