Is there a function already defined for this?

Stream: Is there code for X?

[Ching-Tsun Chou]

Given f : ℕ → ℕ (where we may assume ∀ n, f n > 0) and k : ℕ, I wish to find the largest n : ℕ such that:

(∑ i < n, f i) ≤ k

Is such a function already defined in mathlib?

(Yes, I do know about Nat.findGreatest. I'm just wondering whether theorems about the specific function above already exist in mathlib.)

[Ilmārs Cīrulis]

What this function should return when k < f 0?

[Ching-Tsun Chou]

Sorry, I made a typo: the range of the summation should be i < n. I've corrected the inequality above.

[Yaël Dillies]

I don't think we have anything about this specific instantiation of Nat.findGreatest, no

[Ching-Tsun Chou]

Thanks for the info.