prod.tendsto_iff

Stream: Is there code for X?

[Rémy Degenne]

I recently needed the following lemma prod.tendsto_iff, and I suspect that it should already exist somewhere. Also, I don't know what is the correct generality for that statement.

import topology.metric_space.basic

open filter
open_locale topological_space

lemma tendsto_zero_max_iff_of_nonneg {ι} {fi : _root_.filter ι} (f g : ι → ℝ)
  (hf : 0 ≤ f) (hg : 0 ≤ g) :
  tendsto (λ n, max (f n) (g n)) fi (𝓝 0)
    ↔ tendsto (λ n, f n) fi (𝓝 0) ∧ tendsto (λ n, g n) fi (𝓝 0) :=
begin
  split; intro h,
  { split; refine squeeze_zero _ _ h,
    exacts [hf, λ _, le_max_left _ _ , hg, λ _, le_max_right _ _], },
  { have h_add : tendsto (λ (n : ι), f n + g n) fi (𝓝 0),
      by { convert h.1.add h.2, rw zero_add, },
    exact squeeze_zero (λ n, le_max_of_le_left (hf n))
      (λ n, max_le_add_of_nonneg (hf n) (hg n)) h_add, },
end

lemma prod.tendsto_iff {ι G G'} [pseudo_metric_space G] [pseudo_metric_space G']
  (seq : ι → G × G') {f : filter ι} (x : G × G') :
  tendsto seq f (𝓝 x)
    ↔ tendsto (λ n, (seq n).fst) f (𝓝 x.fst) ∧ tendsto (λ n, (seq n).snd) f (𝓝 x.snd) :=
begin
  rw [tendsto_iff_dist_tendsto_zero, @tendsto_iff_dist_tendsto_zero _ _ _ (λ (n : ι), (seq n).fst),
    @tendsto_iff_dist_tendsto_zero _ _ _ (λ (n : ι), (seq n).snd)],
  simp_rw [prod.dist_eq],
  rw tendsto_zero_max_iff_of_nonneg,
  exacts [λ _, dist_nonneg, λ _, dist_nonneg],
end

[Patrick Massot]

Amazingly, I managed to find only its twin lemma. What you want is:

import topology.metric_space.basic

open filter
open_locale topological_space filter

/- Move next to `filter.tendsto_prod_iff` -/
lemma filter.tendsto_prod_iff' {ι G G'} {f : filter ι} {g : filter G} {g' : filter G'}
  {s : ι → G × G'} :
  tendsto s f (g ×ᶠ g') ↔ tendsto (λ n, (s n).1) f g ∧ tendsto (λ n, (s n).2) f g' :=
begin
  unfold filter.prod,
  simp only [tendsto_inf, tendsto_comap_iff, iff_self]
end

open filter

lemma prod.tendsto_iff {ι G G'} [topological_space G] [topological_space G']
  (seq : ι → G × G') {f : filter ι} (x : G × G') :
  tendsto seq f (𝓝 x)
    ↔ tendsto (λ n, (seq n).fst) f (𝓝 x.fst) ∧ tendsto (λ n, (seq n).snd) f (𝓝 x.snd) :=
begin
  cases x,
  rw [nhds_prod_eq, tendsto_prod_iff'],
end

[Patrick Massot]

Notice how math is simple when you get abstract enough...

[Rémy Degenne]

Thank you very much ! I was pretty sure that the metric assumption was not needed and that it should be a result about products of filters, but I got lost when browsing the related lemmas and decided to go for a naive proof and ask experts :)

[Patrick Massot]

It's pretty easy to get lost in our filter library. You could have asked before trying to write a metric proof.

[Rémy Degenne]

well I got so lost that I started to doubt everything and wanted to be sure it was true