x<1 if geometric progression converges

Stream: Is there code for X?

[Filippo A. E. Nuccio]

I was unable to find the

lemma nnreal.lt_one_of_tendsto_pow_0 (a : ℝ≥0) (h : tendsto (λ n : ℕ, a^n) at_top (𝓝 0)) :
  a < 1

It was not hard to prove it, but I cannot believe it is not there...

[Oliver Nash]

It seems to me that this is indeed missing.

You probably saw that we have the converse docs#NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 so I guess we should upgrade that to an iff.

[Yury G. Kudryashov]

Unless you want to do the job twice, I suggest that you submit this (iff) lemma to mathlib4.

[Filippo A. E. Nuccio]

I am happy to do so, but I have been told by "some" Maintainer (that I will not mention) that it is probably better to wait until the freeze. Should I go ahead or wait? I will ping three maintainers, so you cannot guess who they were :rofl: @Adam Topaz @Riccardo Brasca @Johan Commelin

[Scott Morrison]

It is fine to add this to mathlib4 now. The current situation allows for adding new lemmas. Please don't open new mathlib3 PRs unless they are useful for the port, or represent significant new work that you don't want lost.

[Adam Topaz]

I think it was me that made that comment? But that was before I realized that the port will be finished before the freeze :)

[Filippo A. E. Nuccio]

Now that the Copenhagen Masterclass is over, #5656.