eventual monotonicity for summable_condensed_iff

Stream: Is there code for X?

[Joris van Winden]

I am trying to show that the series $\sum_{n = 0} (n \sqrt{\log n})^{-1}$ (where the summand is defined to be zero for $n \in \{0,1\}$) is not summable. My strategy was to use the condensation test given by summable_condensed_iff_of_nonneg.

The problem is that the summand is only antitone for $n \geq 2$ (instead of $n \geq 1$, as is required by summable_condensed_iff_nonneg). I could shift my summation index using summable_nat_add_iff, but then the transformed series is not so nice to work with.

My question is the following: is there a way to efficiently work around summable_condensed_iff_of_nonneg so that the monotonicity/positivity hypotheses are only required for sufficiently large $n$?

[Antoine Chambert-Loir]

I would prove a corollary of docs#summable_condensed_iff_of_nonneg that only assumes eventual mononicity/positivity. One needs to rewrite the series as the sum of the first a terms plus the translated series to which that lemma would apply.

[Antoine Chambert-Loir]

In particular, I would prove that f(n+a) is monotone under the assumption that f(n) <= f(m) as soon as a<=n<=m, and the latter will be reasonably clear in your case.

[Bhavik Mehta]

It may also be feasible to generalise docs#summable_condensed_iff_of_nonneg in mathlib to only assume eventual things, then the current version can be deduced from that

[Antoine Chambert-Loir]

Indeed. What would be the best design principle for mathlib?

[Antoine Chambert-Loir]

I fear that one would have to introduce Function.eventuallyMonotone, and then proves Function.monotone.eventuallyMonotone_zero…

[Joris van Winden]

I expect a predicate EventuallyMonotone could be useful more generally.

[Bhavik Mehta]

Perhaps h_nonneg being docs#Filter.EventuallyLE while h_mono becomes ∃ k, ∀ m n : ℕ, k < m → m ≤ n → f n ≤ f m may be enough for now; equivalently ∃ k, AntitoneOn f (Set.Ioi k)

[Joris van Winden]

Antoine Chambert-Loir said:

I would prove a corollary of docs#summable_condensed_iff_of_nonneg that only assumes eventual mononicity/positivity. One needs to rewrite the series as the sum of the first a terms plus the translated series to which that lemma would apply.

There is the issue that 'condensing' the series does not commute with shifting the index. So maybe instead it is more convenient to set the first $n$ terms equal to $f (m)$, assuming that $f$ is monotone starting from $m$.

[Ruben Van de Velde]

Yeah, I tried to prove it earlier, but didn't get far. Maybe because I didn't think through the maths first

[Joris van Winden]

I think I found a nice proof!

Let m be such that n => f n is antitone and nonnegative for m ≤ n. Then apply summable_condensed_iff_of_nonneg to n => f (max n m), and use summable_congr_atTop to conclude that f is summable.

[Joris van Winden]

#34985

[Antoine Chambert-Loir]

nice trick.