Convergence of a complex series bounded by a geometric sum

Stream: Is there code for X?

[Mark Gerads]

image.png
I [need something like this] and[ want to know if someone already did this].

[Ruben Van de Velde]

I'd start looking at https://leanprover-community.github.io/mathlib_docs/analysis/specific_limits.html

[Mark Gerads]

The entire file (_target/deps/mathlib/src/analysis/specific_limits.lean) does not have a single 'ℂ' in it.

[Yaël Dillies]

That's because it might not be the correct level of generality.

[Yaël Dillies]

What about docs#summable_geometric_of_norm_lt_1? That sounds close.

[Yury G. Kudryashov]

This plus something like docs#summable_of_norm_bounded

[Mark Gerads]

Yaël Dillies said:

What about docs#summable_geometric_of_norm_lt_1? That sounds close.

If I were to generalize, I need something along the lines of :
lemma summable_bounded_by_geometric_of_norm_lt_1
{f : ℕ → K} (h0 : ∥ξ∥ < 1) (h1 : ∀ (k : ℕ), ∥ξ ^ k∥ ≥ ∥f k∥)
: summable f :=

Yury G. Kudryashov said:

This plus something like docs#summable_of_norm_bounded

summable_of_norm_bounded is indeed the missing piece I needed.