(n+1)^{1/n} tends to 1

Stream: Is there code for X?

[Jiang Jiedong]

Hi everyone,
Is this result:
$\lim_{n \to \infty} (n+1)^{1/n} = 1$
currently in Mathlib? If not, what theorems should I add to mathlib to get this result? Thank you!

[Damiano Testa]

I hope that sorry would be required somewhere...

[Etienne Marion]

This tends to $1$

[Jiang Jiedong]

Etienne Marion said:

This tends to $1$

Thank you! This is a stupid typo of me. Modified.

[Bjørn Kjos-Hanssen]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/LHopital.html

[Kevin Buzzard]

I would take logs and then hope that we have log(n) is o(n).

[Yan Yablonovskiy]

Jiang Jiedong said:

Hi everyone,
Is this result:
$\lim_{n \to \infty} (n+1)^{1/n} = 1$
currently in Mathlib? If not, what theorems should I add to mathlib to get this result? Thank you!

Taking logs and justifying via regular limit laws and continuity.

Then as others have also said, can use LHopitals. A very oblique but curious proof could be using prime number theorem, if it were in mathlib.

[Damiano Testa]

There is docs#tendsto_rpow_div. You can then argue that your sequence is bounded below by n ^ (1 / n) and above by (2 * n) ^ (1 / n).

[Jiang Jiedong]

Damiano Testa said:

There is docs#tendsto_rpow_div. You can then argue that your sequence is bounded below by n ^ (1 / n) and above by (2 * n) ^ (1 / n).

Thanks! This seems to be the shortest path.