Zulip Chat Archive

Stream: new members

Topic: big_operator not starting from zero

Horatiu Cheval (Aug 22 2021 at 13:58):

What would be the recommended way, with best API, for writing a big operator over a range not starting from zero, like i=nn+mai\prod_{i = n}^{n + m} a_i?
I can think of two options:

 i in range (m + 1), a (n + i)


 i in (range (n + m + 1)).filter (nat.le n), a i

Is one better supported than the other, or maybe there's some other standard option?

Ruben Van de Velde (Aug 22 2021 at 14:05):

Without much experience to cloud my judgment, I'd probably pick the first option :)

Horatiu Cheval (Aug 22 2021 at 14:36):

That's what I tried at first too. But then how do I go about decomposing it into products starting from zero, i.e. i=0man+ii=0n1ai=i=0n+mai \prod_{i=0}^m a_{n + i} \cdot \prod_{i = 0}^{n-1} a_i = \prod_{i=0}^{n+m} a_i?

Horatiu Cheval (Aug 22 2021 at 14:39):

This seemed not hard to do (haven't tried yet) in the second variant with some results about products over unions of finsets, which exist in mathlib

Eric Wieser (Aug 22 2021 at 15:18):

We already have that lemma somewhere

Eric Wieser (Aug 22 2021 at 15:18):

docs#finset.prod_range_add, guessed by what the statement would be

Horatiu Cheval (Aug 22 2021 at 17:34):

That's great, thank you!

Bolton Bailey (Aug 23 2021 at 09:45):

For your additional reference there is also docs#finset.Ico, which represents more directly an interval of naturals. You may have more luck working with range, depending on what lemmas you want to use.

Last updated: Dec 20 2023 at 11:08 UTC