Finite sums over ordered filters

This file records elementary consequences of a finite family being zero away from an initial interval. They are useful whenever a filtered finite sum is evaluated after all of its nonzero terms have been passed.

theorem Finset.sum_filter_eq_zero_of_forall_ne_zero_le {ι : Type u_1} {α : Type u_2} {M : Type u_3} [Preorder α] [AddCommMonoid M] (s : Finset ι) {a : ι → α} {e : ι → M} {p q : α} (hpq : p < q) (ha : ∀ i ∈ s, e i ≠ 0 → a i ≤ p) : {i ∈ s | a i = q}.sum e = 0

If all nonzero terms of a finite family have indices at or to the left of p, then its sum over the terms indexed by q vanishes whenever p < q.

theorem Finset.lt_sum_filter_of_lt_zero_of_forall_ne_zero_le {ι : Type u_1} {γ : Type u_4} {β : Type u_5} [PartialOrder γ] [LT β] [AddCommMonoid β] (s : Finset ι) {a : ι → γ} {e : ι → β} {p : γ} {c : β} (hc : c < 0) (hp : c < {i ∈ s | a i = p}.sum e) (ha : ∀ i ∈ s, e i ≠ 0 → a i ≤ p) {q : γ} : p ≤ q → c < {i ∈ s | a i = q}.sum e

If all nonzero terms of a finite family have indices at or to the left of p, then a filtered sum beyond p is bounded below by any negative c that also bounds the sum at p from below.