using tendsto

Stream: Is there code for X?

[Moritz Firsching]

I'm trying to use tendsto and need some very basic lemmas and I'm wondering how to get them most easily:

import tactic
import analysis.special_functions.log
import order.filter

import data.fintype.basic
import data.finset.sum
import data.real.basic

open real
open filter
open nat

open_locale filter topological_space

-- Is there some more direct way of proving this or
-- even this lemma somewhere in mathlib?
lemma unique_limit (a : (ℕ → ℝ)) (A B: ℝ)
(hA: tendsto (λ (k : ℕ), a k) at_top (𝓝 (A)))
(hB: tendsto (λ (k : ℕ), a k) at_top (𝓝 (B))) :
A = B :=
begin
  have h := tendsto.sub hA hB,
  simp only [sub_self] at h,
  have hAB: (0 : ℝ) = A - B :=
  begin
    -- how to use tendsto_const_iff here?
    sorry,
  end,
  exact eq_of_sub_eq_zero (symm hAB),
end

lemma sub_seq_tendsto {an : ℕ → ℝ} {A : ℝ}
 (h: tendsto (λ (n : ℕ), an n) at_top (𝓝 (A))):
 tendsto (λ (n : ℕ), an (2*n)) at_top (𝓝 (A)) :=
begin
  sorry,
end

Any advice on how to solve the sorrys above?

[Kalle Kytölä]

I think docs#tendsto_nhds_unique should help (hopefully very directly) with the first one.

[Moritz Firsching]

Kalle Kytölä said:

I think docs#tendsto_nhds_unique should help (hopefully very directly) with the first one.

perfect, thanks:

lemma unique_limit (a : (ℕ → ℝ)) (A B: ℝ)
(hA: tendsto (λ (k : ℕ), a k) at_top (𝓝 (A)))
(hB: tendsto (λ (k : ℕ), a k) at_top (𝓝 (B))) :
A = B :=
begin
  exact tendsto_nhds_unique hA hB,
end

[Kalle Kytölä]

And docs#filter.tendsto.comp with the second one, if you first prove that $\lim_{n \to \infty} 2 n = \infty$ (something like tendsto (λ (n : ℕ), 2*n) at_top at_top).

[Floris van Doorn]

You can use docs#filter.tendsto.mul_at_top for that

[Patrick Massot]

You don't need all those parentheses. You can write

lemma unique_limit (a : ℕ → ℝ) (A B: ℝ)
(hA: tendsto a at_top (𝓝 A))
(hB: tendsto a at_top (𝓝 B)) :
A = B :=
tendsto_nhds_unique hA hB

[Moritz Firsching]

Thanks I will write less parentheses...

For the second one, I can't quite get it to work yet:

lemma sub_seq_tendsto {an : ℕ → ℝ} {A : ℝ}
 (h: tendsto an at_top (𝓝 A)):
 tendsto (λ (n : ℕ), an 2*n) at_top (𝓝 A) :=
begin
  have htop: tendsto (λ (n : ℕ), 2*n) at_top at_top :=
  begin
    have h2: tendsto (λ (n : ℕ), 2) at_top (𝓝 2)
      := tendsto_const_nhds,
    rw tendsto.mul_at_top two_pos h2 tendsto_id,
  end,
  exact tendsto.comp h htop,
end

The rw, that should solve the proof of htop complains:

type mismatch at application
  tendsto.mul_at_top two_pos
term
  two_pos
has type
  0 < 2
but is expected to have type
  0 < ?m_3