Sequence limit

Stream: Is there code for X?

[María Inés de Frutos Fernández]

Do we have this limit computed anywhere?

import topology.metric_space.basic
import analysis.special_functions.pow

open_locale filter topological_space

example {C : ℝ} (hC0 : 0 < C) : filter.tendsto (λ n : ℕ, C ^ (1 / (n : ℝ))) filter.at_top (𝓝 1) :=
sorry

[Yaël Dillies]

Is it not simply 1 / (n : ℝ) tending to 0 once you've pulled the C ^ out of the tendsto via continuity?

[Jason KY.]

I guess you can prove it with sequential continuity:

example {C : ℝ} (hC0 : 0 < C) :
  filter.tendsto (λ n : ℕ, C ^ (1 / (n : ℝ))) filter.at_top (𝓝 1) :=
begin
  rw (by rw real.rpow_zero : 𝓝 1 = 𝓝 (C ^ (0 : ℝ))),
  exact (continuous_iff_continuous_at.2
    (λ x, real.continuous_at_const_rpow hC0.ne.symm)).to_sequentially_continuous _
    (tendsto_const_div_at_top_nhds_0_nat 1),
end

[María Inés de Frutos Fernández]

I should have asked this in new members; I don't know how to move it there now. I ended up with this proof:

import topology.metric_space.basic
import analysis.special_functions.pow

open_locale filter topological_space

example {C : ℝ} (hC : 0 < C) : filter.tendsto (λ n : ℕ, C ^ (1 / (n : ℝ))) filter.at_top (𝓝 1) :=
begin
  apply filter.tendsto.comp _ (tendsto_const_div_at_top_nhds_0_nat 1),
  rw ← real.rpow_zero C,
  apply continuous_at.tendsto (real.continuous_at_const_rpow (ne_of_gt hC)),
end