Geometric sequence tends to 0

Stream: maths

[Patrick Stevens]

I'm looking for the following lemma:

theorem decreasing_and_nonneg (f : ℕ → ℚ) (N : ℕ)
  (nonneg : ∀ k ≥ N, 0 ≤ f k) (decreasing : ∀ k ≥ N, f (k + 1) ≤ f k / 2) :
  ∀ ε > 0, ∃ n ≥ N, ∀ m ≥ n, f m < ε := sorry

(This is in service of proving that sqrt_aux, an explicit definition of a Cauchy sequence defining sqrt x, converges.)

I found analysis.specific_limits.basic and tendsto_at_top_of_geom_le which seems to be closest to what I want, but it talks about infinity rather than 0 :( and I'd prefer to stay in the rationals for this. Does anyone know where I can find it, or am I likely to have to prove it?

[Filippo A. E. Nuccio]

I think that the major problem you are facing is that limits of these kind are treated using filters in mathlib.

[Filippo A. E. Nuccio]

See for instance docs#eventually_lt_of_tendsto_lt

[Patrick Stevens]

Ah, I see, thanks - I do need the epsilon formulation because I'm going to plug the result into an is_cau_seq, but I'll see if I can filterise my hypotheses

[Filippo A. E. Nuccio]

One good way to epsilon-ise filter definitions is through eventually-holding properties, see for instance here docs#le_of_tendsto.

[Filippo A. E. Nuccio]

The ∀ᶠ means " for almost all" or " for all but finitely many" according to context.

[Filippo A. E. Nuccio]

Or perhaps docs#tendsto_at_top is really what you want!