limit comparison test for sums

Stream: Is there code for X?

[Joris van Winden]

Is there a lemma in mathlib which says that if f / g converges to a constant, then f is summable iff g is summable (i.e., the limit comparison test)? The closest I could find was summable_of_isBigO, but this is not really useful to me since I want to apply the test to show divergence.

A similar theorem can also be formulated in terms of Asymptotics.isTheta, but there I still found nothing.

[Etienne Marion]

I would say the closest is IsEquivalent.summable_iff_nat (it is the case where the constant is one). Also your constant would have to be nonzero.

You can also use summable_of_isBigO to do a reasoning by contrapositive.

[Sébastien Gouëzel]

docs#IsEquivalent.summable_iff gives it when the ratio tends to 1, from which the general case follows easily.

[Joris van Winden]

Would it be worthwhile to add an IsTheta version of summable_iff?