Limits of c^(1/n) and (n+c)^(1/n)

Stream: Is there code for X?

[Michael Stoll]

I need the facts that $\lim_{n \to \infty} c^{1/n} = 1$ (for $c \in \mathbb{R}_{>0}$) and $\lim_{n \to \infty} (n + c)^{1/n} = 1$ (for $c \in \mathbb{R}$) ,
but can't seem to find something along these lines in Mathlib:

@loogle Filter.Tendsto (fun _ : ℕ ↦ Real.rpow _ _) Filter.atTop _

[loogle]

:shrug: nothing found

[Michael Stoll]

OK; found docs#tendsto_rpow_div (which is for a real variable). I wonder why

@loogle Filter.Tendsto, Real.rpow

[loogle]

:shrug: nothing found

[Michael Stoll]

doesn't find anything...

[Michael Stoll]

docs#tendsto_rpow_div_mul_add should be usable for the second one.

[Michael Stoll]

@loogle Filter.Tendsto (fun x : ℝ ↦ ?c ^ (1/ x)) Filter.atTop

[loogle]

:search: tendsto_rpow_div

[Michael Stoll]

Is there no version with a constant ?c?

[Michael Stoll]

I guess it can be deduced via docs#Filter.Tendsto.rpow, but I would have expected this to be there.

[Michael Stoll]

Michael Stoll said:

I wonder why ... doesn't find anything...

I guess this is because it's syntactically HPow.hpow and not Real.rpow.
Loogling is an art :shrug:

[Yakov Pechersky]

There's also docs#tendsto_zpow_atTop_zero wrong variable

[Jireh Loreaux]

@loogle Filter.Tendsto, "rpow"

[loogle]

:search: tendsto_rpow_atTop, tendsto_exp_div_rpow_atTop, and 28 more

[Jireh Loreaux]

I couldn't find it in this list, so I doubt we have it.

[Jireh Loreaux]

But you should be able to prove it relatively easily from docs#Real.continuousAt_const_rpow

[Yakov Pechersky]

import Mathlib

open Filter Topology

lemma Filter.Tendsto.const_rpow_inv_atTop {c : ℝ} (hc0 : c ≠ 0) :
    Tendsto (fun k : ℝ ↦ c ^ (k⁻¹)) atTop (𝓝 1) := by
  simpa using (tendsto_const_nhds (x := c)).rpow tendsto_inv_atTop_zero (Or.inl hc0)

lemma Filter.Tendsto.const_npow_inv_atTop {c : ℝ} (hc0 : c ≠ 0) :
    Tendsto (fun k : ℕ ↦ c ^ ((k : ℝ)⁻¹)) atTop (𝓝 1) :=
  (const_rpow_inv_atTop hc0).comp tendsto_natCast_atTop_atTop

[Michael Stoll]

Here is my use case.

import Mathlib

open Filter Topology

example : Tendsto (fun n : ℕ ↦ (4 * ((n : ℝ) + 1)) ^ (1 / n : ℝ)) atTop (𝓝 1) := by
  have hc : (fun N : ℕ ↦ (4 * ((N : ℝ) + 1)) ^ (1 / N : ℝ)) =
       (fun x : ℝ ↦ x ^ (4 / (1 * x + -4))) ∘ fun N : ℕ ↦ 4 * ((N : ℝ) + 1) := by
    ext1 N
    rcases eq_or_ne N 0 with rfl | hN₀
    · simp
    simp only [Function.comp_apply]
    congr 1
    ring
  rw [hc]
  exact (tendsto_rpow_div_mul_add 4 1 (-4) zero_ne_one).comp <|
    (tendsto_atTop_add_const_right atTop 1 tendsto_natCast_atTop_atTop).const_mul_atTop
      zero_lt_four

[Michael Stoll]

Using docs#tendsto_rpow_div_mul_add is a bit more efficient here, maybe.

[Yakov Pechersky]

Yours is a bit harder than the initial question because you have to show that the root shrinks faster than the linear function grows.

[Yakov Pechersky]

Ah, that was the second question

[Yakov Pechersky]

example : Tendsto (fun n : ℕ ↦ (4 * ((n : ℝ) + 1)) ^ (1 / n : ℝ)) atTop (𝓝 1) := by
  have := (tendsto_rpow_div_mul_add 1 4⁻¹ (-1) (by norm_num))
  have hn : Tendsto (fun n : ℝ ↦ (4 * (n + 1))) atTop atTop := by
    apply Tendsto.const_mul_atTop (by norm_num)
    sorry -- don't remember lemma names
  refine (this.comp (hn.comp tendsto_natCast_atTop_atTop)).congr ?_
  intro
  simp

[Michael Stoll]

This is the same proof, modulo permutation...

[Yakov Pechersky]

Yeah, just avoiding the explicit hc writing

[Michael Stoll]

import Mathlib

open Filter Topology

example : Tendsto (fun n : ℕ ↦ (4 * ((n : ℝ) + 1)) ^ (1 / n : ℝ)) atTop (𝓝 1) := by
  have := tendsto_rpow_div_mul_add 1 4⁻¹ (-1) (by norm_num)
  have hn : Tendsto (fun x : ℝ ↦ (4 * (x + 1))) atTop atTop :=
    (tendsto_atTop_add_const_right atTop 1 tendsto_id).const_mul_atTop zero_lt_four
  exact (this.comp (hn.comp tendsto_natCast_atTop_atTop)).congr fun N ↦ by simp

[Yakov Pechersky]

This is a lot like the "invisible mathematics" talk

[Michael Stoll]

I guessI should listen to it :smiley: