Library prosa.util.sum
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
Require Export prosa.util.notation.
Require Export prosa.util.nat.
Section SumsOverSequences.
Require Export prosa.util.notation.
Require Export prosa.util.nat.
Section SumsOverSequences.
Consider any type I with a decidable equality ...
... and assume we are given a sequence ...
... and a predicate P.
First, we will show some properties of the sum performed over a single function
yielding natural numbers.
Consider any function that yields natural numbers...
We start showing that having every member of r equal to zero is equivalent to
having the sum of all the elements of r equal to zero, and vice-versa.
Lemma sum_nat_eq0_nat :
all (fun x ⇒ F x == 0) r = (\sum_(i <- r) F i == 0).
Proof.
destruct (all (fun x ⇒ F x == 0) r) eqn:ZERO.
{ move: ZERO ⇒ /allP ZERO; rewrite -leqn0.
rewrite big_seq_cond (eq_bigr (fun x ⇒ 0)); first by rewrite big_const_seq iter_addn.
move⇒ i; rewrite andbT⇒IN.
specialize (ZERO i); rewrite IN in ZERO.
by move: ZERO ⇒ /implyP ZERO; apply/eqP; apply ZERO. }
{ apply negbT in ZERO; rewrite -has_predC in ZERO.
move: ZERO ⇒ /hasP [x IN NEQ].
rewrite (big_rem x) //=.
symmetry; apply negbTE; rewrite neq_ltn; apply/orP; right.
apply leq_trans with (n := F x); last by apply leq_addr.
by rewrite lt0n. }
Qed.
all (fun x ⇒ F x == 0) r = (\sum_(i <- r) F i == 0).
Proof.
destruct (all (fun x ⇒ F x == 0) r) eqn:ZERO.
{ move: ZERO ⇒ /allP ZERO; rewrite -leqn0.
rewrite big_seq_cond (eq_bigr (fun x ⇒ 0)); first by rewrite big_const_seq iter_addn.
move⇒ i; rewrite andbT⇒IN.
specialize (ZERO i); rewrite IN in ZERO.
by move: ZERO ⇒ /implyP ZERO; apply/eqP; apply ZERO. }
{ apply negbT in ZERO; rewrite -has_predC in ZERO.
move: ZERO ⇒ /hasP [x IN NEQ].
rewrite (big_rem x) //=.
symmetry; apply negbTE; rewrite neq_ltn; apply/orP; right.
apply leq_trans with (n := F x); last by apply leq_addr.
by rewrite lt0n. }
Qed.
In the same way, if at least one element of r is not zero, then the sum of all
elements of r must be strictly positive, and vice-versa.
Lemma sum_seq_gt0P:
reflect (∃ i, i \in r ∧ 0 < F i) (0 < \sum_(i <- r) F i).
Proof.
apply: (iffP idP); move⇒ LT0.
{ induction r; first by rewrite big_nil in LT0.
destruct (F a > 0) eqn:POS.
- ∃ a.
by split ⇒ //; rewrite in_cons; apply /orP; left.
- apply negbT in POS; rewrite -leqNgt leqn0 in POS; move: POS ⇒ /eqP POS.
rewrite big_cons POS add0n in LT0.
move: (IHl LT0) ⇒ [i [IN POSi]].
by ∃ i; split ⇒ //; rewrite in_cons; apply /orP; right. }
{ move: LT0 ⇒ [i [IN POS]].
rewrite (big_rem i) //=.
by apply leq_trans with (F i); last by rewrite leq_addr. }
Qed.
reflect (∃ i, i \in r ∧ 0 < F i) (0 < \sum_(i <- r) F i).
Proof.
apply: (iffP idP); move⇒ LT0.
{ induction r; first by rewrite big_nil in LT0.
destruct (F a > 0) eqn:POS.
- ∃ a.
by split ⇒ //; rewrite in_cons; apply /orP; left.
- apply negbT in POS; rewrite -leqNgt leqn0 in POS; move: POS ⇒ /eqP POS.
rewrite big_cons POS add0n in LT0.
move: (IHl LT0) ⇒ [i [IN POSi]].
by ∃ i; split ⇒ //; rewrite in_cons; apply /orP; right. }
{ move: LT0 ⇒ [i [IN POS]].
rewrite (big_rem i) //=.
by apply leq_trans with (F i); last by rewrite leq_addr. }
Qed.
Next, we show that if a number a is not contained in r, then filtering or not
filtering a when summing leads to the same result.
Lemma sum_notin_rem_eqn:
∀ a,
a \notin r →
\sum_(x <- r | P x && (x != a)) F x = \sum_(x <- r | P x) F x.
Proof.
intros a NOTIN.
induction r; first by rewrite !big_nil.
rewrite !big_cons IHl.
{ move: NOTIN ⇒ /memPn NOTIN.
move: (NOTIN a0) ⇒ NEQ.
feed NEQ; first by (rewrite in_cons; apply/orP; left).
by rewrite NEQ Bool.andb_true_r. }
{ apply /memPn; intros y IN.
move: NOTIN ⇒ /memPn NOTIN.
by apply NOTIN; rewrite in_cons; apply/orP; right. }
Qed.
∀ a,
a \notin r →
\sum_(x <- r | P x && (x != a)) F x = \sum_(x <- r | P x) F x.
Proof.
intros a NOTIN.
induction r; first by rewrite !big_nil.
rewrite !big_cons IHl.
{ move: NOTIN ⇒ /memPn NOTIN.
move: (NOTIN a0) ⇒ NEQ.
feed NEQ; first by (rewrite in_cons; apply/orP; left).
by rewrite NEQ Bool.andb_true_r. }
{ apply /memPn; intros y IN.
move: NOTIN ⇒ /memPn NOTIN.
by apply NOTIN; rewrite in_cons; apply/orP; right. }
Qed.
We prove that if any element of r is bounded by constant c,
then the sum of the whole set is bounded by c × size r.
Lemma sum_majorant_constant:
∀ c,
(∀ a, a \in r → P a → F a ≤ c) →
\sum_(j <- r | P j) F j ≤ c × (size [seq j <- r | P j]).
Proof.
intros.
induction r; first by rewrite big_nil.
feed IHl.
{ intros; apply H.
- by rewrite in_cons; apply/orP; right.
- by done. }
rewrite big_cons.
destruct (P a) eqn:EQ.
{ rewrite -cat1s filter_cat size_cat mulnDr.
apply leq_add; last by done.
rewrite size_filter //= EQ addn0 muln1.
apply H; last by done.
by rewrite in_cons; apply/orP; left. }
{ apply leq_trans with (c × size [seq j <- l | P j]); first by done.
rewrite leq_mul2l; apply /orP; right.
by rewrite -cat1s filter_cat size_cat leq_addl. }
Qed.
∀ c,
(∀ a, a \in r → P a → F a ≤ c) →
\sum_(j <- r | P j) F j ≤ c × (size [seq j <- r | P j]).
Proof.
intros.
induction r; first by rewrite big_nil.
feed IHl.
{ intros; apply H.
- by rewrite in_cons; apply/orP; right.
- by done. }
rewrite big_cons.
destruct (P a) eqn:EQ.
{ rewrite -cat1s filter_cat size_cat mulnDr.
apply leq_add; last by done.
rewrite size_filter //= EQ addn0 muln1.
apply H; last by done.
by rewrite in_cons; apply/orP; left. }
{ apply leq_trans with (c × size [seq j <- l | P j]); first by done.
rewrite leq_mul2l; apply /orP; right.
by rewrite -cat1s filter_cat size_cat leq_addl. }
Qed.
Next, we show that the sum of the elements in r respecting P can
be obtained by removing from the total sum over r the sum of the elements
in r not respecting P.
Lemma sum_pred_diff:
\sum_(r <- r | P r) F r =
\sum_(r <- r) F r - \sum_(r <- r | ~~ P r) F r.
Proof.
induction r; first by rewrite !big_nil subn0.
rewrite !big_cons !IHl; clear IHl.
case (P a); simpl; last by rewrite subnDl.
rewrite addnBA; first by done.
rewrite big_mkcond leq_sum //.
intros t _.
by case (P t).
Qed.
\sum_(r <- r | P r) F r =
\sum_(r <- r) F r - \sum_(r <- r | ~~ P r) F r.
Proof.
induction r; first by rewrite !big_nil subn0.
rewrite !big_cons !IHl; clear IHl.
case (P a); simpl; last by rewrite subnDl.
rewrite addnBA; first by done.
rewrite big_mkcond leq_sum //.
intros t _.
by case (P t).
Qed.
Summing natural numbers over a superset can only yields a greater sum.
Requiring the absence of duplicate in r is a simple way to
guarantee that the set inclusion r ≤ rs implies the actually
required multiset inclusion.
Lemma leq_sum_sub_uniq :
∀ (rs: seq I),
uniq r →
{subset r ≤ rs} →
\sum_(i <- r) F i ≤ \sum_(i <- rs) F i.
Proof.
intros rs UNIQ SUB; generalize dependent rs.
induction r as [| x r1' IH]; first by ins; rewrite big_nil.
intros rs SUB.
have IN: x \in rs by apply SUB; rewrite in_cons eq_refl orTb.
simpl in UNIQ; move: UNIQ ⇒ /andP [NOTIN UNIQ]; specialize (IH UNIQ).
destruct (splitPr IN).
rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
rewrite mem_cat in_cons eq_refl in IN.
rewrite -big_cat /=.
apply IH; red; intros x0 IN0.
rewrite mem_cat.
feed (SUB x0); first by rewrite in_cons IN0 orbT.
rewrite mem_cat in_cons in SUB.
move:SUB ⇒ /orP [SUB1 | /orP [/eqP EQx | SUB2]]; [by rewrite SUB1 | | by rewrite SUB2 orbT].
by rewrite -EQx IN0 in NOTIN.
Qed.
End SumOfOneFunction.
∀ (rs: seq I),
uniq r →
{subset r ≤ rs} →
\sum_(i <- r) F i ≤ \sum_(i <- rs) F i.
Proof.
intros rs UNIQ SUB; generalize dependent rs.
induction r as [| x r1' IH]; first by ins; rewrite big_nil.
intros rs SUB.
have IN: x \in rs by apply SUB; rewrite in_cons eq_refl orTb.
simpl in UNIQ; move: UNIQ ⇒ /andP [NOTIN UNIQ]; specialize (IH UNIQ).
destruct (splitPr IN).
rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
rewrite mem_cat in_cons eq_refl in IN.
rewrite -big_cat /=.
apply IH; red; intros x0 IN0.
rewrite mem_cat.
feed (SUB x0); first by rewrite in_cons IN0 orbT.
rewrite mem_cat in_cons in SUB.
move:SUB ⇒ /orP [SUB1 | /orP [/eqP EQx | SUB2]]; [by rewrite SUB1 | | by rewrite SUB2 orbT].
by rewrite -EQx IN0 in NOTIN.
Qed.
End SumOfOneFunction.
In this section, we show some properties of the sum performed over two different functions.
Consider three functions that yield natural numbers.
Assume that E2 dominates E1 in all the points contained in the set r and respecting
the predicate P. We prove that, if we sum both function over those points, then the sum
of E2 will dominate the sum of E1.
Lemma leq_sum_seq :
(∀ i, i \in r → P i → E1 i ≤ E2 i) →
\sum_(i <- r | P i) E1 i ≤ \sum_(i <- r | P i) E2 i.
Proof.
intros LE.
rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
by apply leq_sum; move ⇒ j /andP [IN H]; apply LE.
Qed.
(∀ i, i \in r → P i → E1 i ≤ E2 i) →
\sum_(i <- r | P i) E1 i ≤ \sum_(i <- r | P i) E2 i.
Proof.
intros LE.
rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
by apply leq_sum; move ⇒ j /andP [IN H]; apply LE.
Qed.
In the same way, if E1 equals E2 in all the points considered above, then also the two
sums will be identical.
Lemma eq_sum_seq:
(∀ i, i \in r → P i → E1 i == E2 i) →
\sum_(i <- r | P i) E1 i == \sum_(i <- r | P i) E2 i.
Proof.
move⇒ EQ.
rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
rewrite eqn_leq; apply /andP; split.
all: apply leq_sum; move ⇒ j /andP [IN H].
all: by move:(EQ j IN H) ⇒ LEQ; ssrlia.
Qed.
(∀ i, i \in r → P i → E1 i == E2 i) →
\sum_(i <- r | P i) E1 i == \sum_(i <- r | P i) E2 i.
Proof.
move⇒ EQ.
rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
rewrite eqn_leq; apply /andP; split.
all: apply leq_sum; move ⇒ j /andP [IN H].
all: by move:(EQ j IN H) ⇒ LEQ; ssrlia.
Qed.
Assume that P1 implies P2 in all the points contained in
the set r. We prove that, if we sum both functions over those
points, then the sum of E conditioned by P2 will dominate
the sum of E conditioned by P1.
Lemma leq_sum_seq_pred:
(∀ i, i \in r → P1 i → P2 i) →
\sum_(i <- r | P1 i) E i ≤ \sum_(i <- r | P2 i) E i.
Proof.
intros LE.
induction r; first by rewrite !big_nil.
rewrite !big_cons.
destruct (P1 a) eqn:P1a; first (move: P1a ⇒ /eqP; rewrite eqb_id ⇒ P1a).
- rewrite LE //; last by rewrite in_cons; apply/orP; left.
rewrite leq_add2l.
by apply IHl; intros; apply LE ⇒ //; rewrite in_cons; apply/orP; right.
- destruct (P2 a) eqn:P2a.
+ by eapply leq_trans;
[apply IHl; intros; apply LE ⇒ //; rewrite in_cons; apply/orP; right
| apply leq_addl].
+ by apply IHl; intros; apply LE ⇒ //; rewrite in_cons; apply/orP; right.
Qed.
(∀ i, i \in r → P1 i → P2 i) →
\sum_(i <- r | P1 i) E i ≤ \sum_(i <- r | P2 i) E i.
Proof.
intros LE.
induction r; first by rewrite !big_nil.
rewrite !big_cons.
destruct (P1 a) eqn:P1a; first (move: P1a ⇒ /eqP; rewrite eqb_id ⇒ P1a).
- rewrite LE //; last by rewrite in_cons; apply/orP; left.
rewrite leq_add2l.
by apply IHl; intros; apply LE ⇒ //; rewrite in_cons; apply/orP; right.
- destruct (P2 a) eqn:P2a.
+ by eapply leq_trans;
[apply IHl; intros; apply LE ⇒ //; rewrite in_cons; apply/orP; right
| apply leq_addl].
+ by apply IHl; intros; apply LE ⇒ //; rewrite in_cons; apply/orP; right.
Qed.
Next, we prove that if for any element x of a set xs the following two statements
hold (1) F1 x is less than or equal to F2 x and (2) the sum F1 x_1, ..., F1 x_n
is equal to the sum of F2 x_1, ..., F2 x_n, then F1 x is equal to F2 x for
any element x of xs.
Lemma sum_majorant_eqn:
∀ xs,
(∀ x, x \in xs → P x → E1 x ≤ E2 x) →
\sum_(x <- xs | P x) E1 x = \sum_(x <- xs | P x) E2 x →
(∀ x, x \in xs → P x → E1 x = E2 x).
Proof.
intros xs H1 H2 x IN PX.
induction xs; first by done.
have Fact: \sum_(j <- xs | P j) E1 j ≤ \sum_(j <- xs | P j) E2 j.
{ rewrite [in X in X ≤ _]big_seq_cond [in X in _ ≤ X]big_seq_cond leq_sum //.
move ⇒ y /andP [INy PY].
apply: H1; last by done.
by rewrite in_cons; apply/orP; right. }
feed IHxs.
{ intros x' IN' PX'.
apply H1; last by done.
by rewrite in_cons; apply/orP; right. }
rewrite big_cons [RHS]big_cons in H2.
have EqLeq: ∀ a b c d, a + b = c + d → a ≤ c → b ≥ d by intros; ssrlia.
move: IN; rewrite in_cons; move ⇒ /orP [/eqP EQ | IN].
{ subst a.
rewrite PX in H2.
specialize (H1 x).
feed_n 2 H1⇒ //; first by rewrite in_cons; apply/orP; left.
move: (EqLeq
(E1 x) (\sum_(j <- xs | P j) E1 j)
(E2 x) (\sum_(j <- xs | P j) E2 j) H2 H1) ⇒ Q.
have EQ: \sum_(j <- xs | P j) E1 j = \sum_(j <- xs | P j) E2 j.
{ by apply /eqP; rewrite eqn_leq; apply/andP; split. }
by move: H2 ⇒ /eqP; rewrite EQ eqn_add2r; move ⇒ /eqP EQ'. }
{ destruct (P a) eqn:PA; last by apply IHxs.
apply: IHxs; last by done.
specialize (H1 a).
feed_n 2 (H1); [ by rewrite in_cons; apply/orP; left | by done | ].
move: (EqLeq
(E1 a) (\sum_(j <- xs | P j) E1 j)
(E2 a) (\sum_(j <- xs | P j) E2 j) H2 H1) ⇒ Q.
by apply/eqP; rewrite eqn_leq; apply/andP; split. }
Qed.
∀ xs,
(∀ x, x \in xs → P x → E1 x ≤ E2 x) →
\sum_(x <- xs | P x) E1 x = \sum_(x <- xs | P x) E2 x →
(∀ x, x \in xs → P x → E1 x = E2 x).
Proof.
intros xs H1 H2 x IN PX.
induction xs; first by done.
have Fact: \sum_(j <- xs | P j) E1 j ≤ \sum_(j <- xs | P j) E2 j.
{ rewrite [in X in X ≤ _]big_seq_cond [in X in _ ≤ X]big_seq_cond leq_sum //.
move ⇒ y /andP [INy PY].
apply: H1; last by done.
by rewrite in_cons; apply/orP; right. }
feed IHxs.
{ intros x' IN' PX'.
apply H1; last by done.
by rewrite in_cons; apply/orP; right. }
rewrite big_cons [RHS]big_cons in H2.
have EqLeq: ∀ a b c d, a + b = c + d → a ≤ c → b ≥ d by intros; ssrlia.
move: IN; rewrite in_cons; move ⇒ /orP [/eqP EQ | IN].
{ subst a.
rewrite PX in H2.
specialize (H1 x).
feed_n 2 H1⇒ //; first by rewrite in_cons; apply/orP; left.
move: (EqLeq
(E1 x) (\sum_(j <- xs | P j) E1 j)
(E2 x) (\sum_(j <- xs | P j) E2 j) H2 H1) ⇒ Q.
have EQ: \sum_(j <- xs | P j) E1 j = \sum_(j <- xs | P j) E2 j.
{ by apply /eqP; rewrite eqn_leq; apply/andP; split. }
by move: H2 ⇒ /eqP; rewrite EQ eqn_add2r; move ⇒ /eqP EQ'. }
{ destruct (P a) eqn:PA; last by apply IHxs.
apply: IHxs; last by done.
specialize (H1 a).
feed_n 2 (H1); [ by rewrite in_cons; apply/orP; left | by done | ].
move: (EqLeq
(E1 a) (\sum_(j <- xs | P j) E1 j)
(E2 a) (\sum_(j <- xs | P j) E2 j) H2 H1) ⇒ Q.
by apply/eqP; rewrite eqn_leq; apply/andP; split. }
Qed.
Next, we prove that the summing over the difference of E1 and E2 is
the same as the difference of the two sums performed separately. Since we
are using natural numbers, we have to require that E2 dominates E1 over
the summing points given by r.
Lemma sum_seq_diff:
(∀ i : I, i \in r → E1 i ≤ E2 i) →
\sum_(i <- r) (E2 i - E1 i) = \sum_(i <- r) E2 i - \sum_(i <- r) E1 i.
Proof.
move⇒ LEQ.
induction r; first by rewrite !big_nil subn0.
rewrite !big_cons subnD.
- apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHl.
by intros; apply LEQ; rewrite in_cons; apply/orP; right.
- by apply LEQ; rewrite in_cons; apply/orP; left.
- rewrite big_seq_cond [in X in _ ≤ X]big_seq_cond.
rewrite leq_sum //; move ⇒ i /andP [IN _].
by apply LEQ; rewrite in_cons; apply/orP; right.
Qed.
End SumOfTwoFunctions.
End SumsOverSequences.
(∀ i : I, i \in r → E1 i ≤ E2 i) →
\sum_(i <- r) (E2 i - E1 i) = \sum_(i <- r) E2 i - \sum_(i <- r) E1 i.
Proof.
move⇒ LEQ.
induction r; first by rewrite !big_nil subn0.
rewrite !big_cons subnD.
- apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHl.
by intros; apply LEQ; rewrite in_cons; apply/orP; right.
- by apply LEQ; rewrite in_cons; apply/orP; left.
- rewrite big_seq_cond [in X in _ ≤ X]big_seq_cond.
rewrite leq_sum //; move ⇒ i /andP [IN _].
by apply LEQ; rewrite in_cons; apply/orP; right.
Qed.
End SumOfTwoFunctions.
End SumsOverSequences.
In this section, we prove a variety of properties of sums performed over ranges.
First, we show a trivial identity: any sum of zeros is zero.
Lemma sum0 m n:
\sum_(m ≤ i < n) 0 = 0.
Proof.
by rewrite big_const_nat iter_addn mul0n addn0 //.
Qed.
\sum_(m ≤ i < n) 0 = 0.
Proof.
by rewrite big_const_nat iter_addn mul0n addn0 //.
Qed.
In a similar way, we prove that the sum of Δ ones is equal to Δ.
Lemma sum_of_ones:
∀ t Δ,
\sum_(t ≤ x < t + Δ) 1 = Δ.
Proof.
move⇒ t Δ.
rewrite big_const_nat iter_addn_0.
by ssrlia.
Qed.
∀ t Δ,
\sum_(t ≤ x < t + Δ) 1 = Δ.
Proof.
move⇒ t Δ.
rewrite big_const_nat iter_addn_0.
by ssrlia.
Qed.
Next, we show that a sum of natural numbers equals zero if and only
if all terms are zero.
Lemma big_nat_eq0 m n F:
\sum_(m ≤ i < n) F i = 0 ↔ (∀ i, m ≤ i < n → F i = 0).
Proof.
split.
- rewrite /index_iota ⇒ /eqP.
rewrite -sum_nat_eq0_nat ⇒ /allP ZERO i.
rewrite -mem_index_iota /index_iota ⇒ IN.
by apply/eqP; apply ZERO.
- move⇒ ZERO.
have→ : \sum_(m ≤ i < n) F i = \sum_(m ≤ i < n) 0 by apply eq_big_nat.
by apply sum0.
Qed.
\sum_(m ≤ i < n) F i = 0 ↔ (∀ i, m ≤ i < n → F i = 0).
Proof.
split.
- rewrite /index_iota ⇒ /eqP.
rewrite -sum_nat_eq0_nat ⇒ /allP ZERO i.
rewrite -mem_index_iota /index_iota ⇒ IN.
by apply/eqP; apply ZERO.
- move⇒ ZERO.
have→ : \sum_(m ≤ i < n) F i = \sum_(m ≤ i < n) 0 by apply eq_big_nat.
by apply sum0.
Qed.
Moreover, the fact that the sum is smaller than the range of the summation
implies the existence of a zero element.
Lemma sum_le_summation_range:
∀ f t Δ,
\sum_(t ≤ x < t + Δ) f x < Δ →
∃ x, t ≤ x < t + Δ ∧ f x = 0.
Proof.
induction Δ; intros; first by rewrite ltn0 in H.
destruct (f (t + Δ)) eqn: EQ.
{ ∃ (t + Δ); split; last by done.
by apply/andP; split; [rewrite leq_addr | rewrite addnS ltnS]. }
{ move: H; rewrite addnS big_nat_recr //= ?leq_addr // EQ addnS ltnS; move ⇒ H.
feed IHΔ.
{ by apply leq_ltn_trans with (\sum_(t ≤ i < t + Δ) f i + n); first rewrite leq_addr. }
move: IHΔ ⇒ [z [/andP [LE GE] ZERO]].
∃ z; split; last by done.
apply/andP; split; first by done.
by rewrite ltnS ltnW. }
Qed.
∀ f t Δ,
\sum_(t ≤ x < t + Δ) f x < Δ →
∃ x, t ≤ x < t + Δ ∧ f x = 0.
Proof.
induction Δ; intros; first by rewrite ltn0 in H.
destruct (f (t + Δ)) eqn: EQ.
{ ∃ (t + Δ); split; last by done.
by apply/andP; split; [rewrite leq_addr | rewrite addnS ltnS]. }
{ move: H; rewrite addnS big_nat_recr //= ?leq_addr // EQ addnS ltnS; move ⇒ H.
feed IHΔ.
{ by apply leq_ltn_trans with (\sum_(t ≤ i < t + Δ) f i + n); first rewrite leq_addr. }
move: IHΔ ⇒ [z [/andP [LE GE] ZERO]].
∃ z; split; last by done.
apply/andP; split; first by done.
by rewrite ltnS ltnW. }
Qed.
Next, we prove that the summing over the difference of two functions is
the same as summing over the two functions separately, and then taking the
difference of the two sums. Since we are using natural numbers, we have to
require that one function dominates the other in the summing range.
Lemma sum_diff:
∀ n F G,
(∀ i, i < n → F i ≥ G i) →
\sum_(0 ≤ i < n) (F i - G i) =
(\sum_(0 ≤ i < n) (F i)) - (\sum_(0 ≤ i < n) (G i)).
Proof.
intros n F G ALL.
rewrite sum_seq_diff; first by done.
move⇒ i; rewrite mem_index_iota; move ⇒ /andP [_ LT].
by apply ALL.
Qed.
∀ n F G,
(∀ i, i < n → F i ≥ G i) →
\sum_(0 ≤ i < n) (F i - G i) =
(\sum_(0 ≤ i < n) (F i)) - (\sum_(0 ≤ i < n) (G i)).
Proof.
intros n F G ALL.
rewrite sum_seq_diff; first by done.
move⇒ i; rewrite mem_index_iota; move ⇒ /andP [_ LT].
by apply ALL.
Qed.
Given a sequence r, function F, and a predicate P, we
prove that the fact that the sum of F conditioned by P is
greater than 0 is equivalent to the fact that there exists an
element i \in r such that F i > 0 and P i holds.
Lemma sum_seq_cond_gt0P:
∀ (T : eqType) (r : seq T) (P : T → bool) (F : T → nat),
reflect (∃ i, i \in r ∧ P i ∧ 0 < F i) (0 < \sum_(i <- r | P i) F i).
Proof.
intros; apply: (iffP idP); intros.
{ induction r; first by rewrite big_nil in H.
rewrite big_cons in H.
destruct (P a) eqn:PA, (F a > 0) eqn:POS.
- ∃ a; repeat split; [by rewrite in_cons; apply/orP; left | by done | by done].
- move: POS ⇒ /negP/negP; rewrite -leqNgt leqn0 ⇒ /eqP Z; rewrite Z add0n in H.
apply IHr in H; destruct H as [i [IN [Pi POS]]].
by (∃ i; repeat split; [rewrite in_cons;apply/orP;right | | ]).
- clear POS; apply IHr in H; destruct H as [i [IN [Pi POS]]].
by (∃ i; repeat split; [rewrite in_cons;apply/orP;right | | ]).
- clear POS; apply IHr in H; destruct H as [i [IN [Pi POS]]].
by (∃ i; repeat split; [rewrite in_cons;apply/orP;right | | ]).
}
{ move: H ⇒ [i [IN [Pi POS]]].
rewrite (big_rem i) //=; rewrite Pi.
by apply leq_trans with (F i); last rewrite leq_addr.
}
Qed.
End SumsOverRanges.
∀ (T : eqType) (r : seq T) (P : T → bool) (F : T → nat),
reflect (∃ i, i \in r ∧ P i ∧ 0 < F i) (0 < \sum_(i <- r | P i) F i).
Proof.
intros; apply: (iffP idP); intros.
{ induction r; first by rewrite big_nil in H.
rewrite big_cons in H.
destruct (P a) eqn:PA, (F a > 0) eqn:POS.
- ∃ a; repeat split; [by rewrite in_cons; apply/orP; left | by done | by done].
- move: POS ⇒ /negP/negP; rewrite -leqNgt leqn0 ⇒ /eqP Z; rewrite Z add0n in H.
apply IHr in H; destruct H as [i [IN [Pi POS]]].
by (∃ i; repeat split; [rewrite in_cons;apply/orP;right | | ]).
- clear POS; apply IHr in H; destruct H as [i [IN [Pi POS]]].
by (∃ i; repeat split; [rewrite in_cons;apply/orP;right | | ]).
- clear POS; apply IHr in H; destruct H as [i [IN [Pi POS]]].
by (∃ i; repeat split; [rewrite in_cons;apply/orP;right | | ]).
}
{ move: H ⇒ [i [IN [Pi POS]]].
rewrite (big_rem i) //=; rewrite Pi.
by apply leq_trans with (F i); last rewrite leq_addr.
}
Qed.
End SumsOverRanges.
In this section, we show how it is possible to equate the result of two sums performed
on two different functions and on different intervals, provided that the two functions
match point-wise.
Consider two equally-sized intervals
[t1, t1+d)
and [t2, t2+d)
...
Assume that the two functions match point-wise with each other, with the points taken
in their respective interval.
Lemma big_sum_eq_in_eq_sized_intervals:
\sum_(t1 ≤ t < t1 + d) F1 t = \sum_(t2 ≤ t < t2 + d) F2 t.
Proof.
induction d; first by rewrite !addn0 !big_geq.
rewrite !addnS !big_nat_recr ⇒ //; try by ssrlia.
rewrite IHn //=; last by move⇒ g G_LTl; apply (equal_before_d g); ssrlia.
by rewrite equal_before_d.
Qed.
End SumOfTwoIntervals.
\sum_(t1 ≤ t < t1 + d) F1 t = \sum_(t2 ≤ t < t2 + d) F2 t.
Proof.
induction d; first by rewrite !addn0 !big_geq.
rewrite !addnS !big_nat_recr ⇒ //; try by ssrlia.
rewrite IHn //=; last by move⇒ g G_LTl; apply (equal_before_d g); ssrlia.
by rewrite equal_before_d.
Qed.
End SumOfTwoIntervals.
In this section, we relate the sum of items with the sum over partitions of those items.
x_to_y is the mapping from an item to the partition it is contained in.
We prove that summation of f x over all x is less than or equal to the summation of
sum_of_partition over all partitions.
Lemma sum_over_partitions_le :
\sum_(x <- xs | P x) f x
≤ \sum_(y <- ys) sum_of_partition y.
Proof.
rewrite /sum_of_partition.
induction xs as [| x' xs' LE_TAIL]; first by rewrite big_nil.
have P_HOLDS: ∀ i j, true → P j && (x_to_y j== i) → P j by move⇒ ??? /andP [P_HOLDS _].
have IN_ys: ∀ x : X, x \in xs' → x_to_y x \in ys.
{ by move⇒ ??; apply H_no_partition_missing ⇒ //; rewrite in_cons; apply /orP; right. }
move: LE_TAIL; rewrite (exchange_big_dep P) ⇒ //= LE_TAIL.
rewrite (exchange_big_dep P) //= !big_cons.
case: (P x') ⇒ //=; last by apply LE_TAIL.
apply leq_add ⇒ //; last by apply LE_TAIL.
rewrite big_const_seq iter_addn_0.
apply leq_pmulr; rewrite -has_count.
apply /hasP; eapply ex_intro2 ⇒ //.
by apply H_no_partition_missing, mem_head.
Qed.
\sum_(x <- xs | P x) f x
≤ \sum_(y <- ys) sum_of_partition y.
Proof.
rewrite /sum_of_partition.
induction xs as [| x' xs' LE_TAIL]; first by rewrite big_nil.
have P_HOLDS: ∀ i j, true → P j && (x_to_y j== i) → P j by move⇒ ??? /andP [P_HOLDS _].
have IN_ys: ∀ x : X, x \in xs' → x_to_y x \in ys.
{ by move⇒ ??; apply H_no_partition_missing ⇒ //; rewrite in_cons; apply /orP; right. }
move: LE_TAIL; rewrite (exchange_big_dep P) ⇒ //= LE_TAIL.
rewrite (exchange_big_dep P) //= !big_cons.
case: (P x') ⇒ //=; last by apply LE_TAIL.
apply leq_add ⇒ //; last by apply LE_TAIL.
rewrite big_const_seq iter_addn_0.
apply leq_pmulr; rewrite -has_count.
apply /hasP; eapply ex_intro2 ⇒ //.
by apply H_no_partition_missing, mem_head.
Qed.
In this section, we prove a stronger result about the equality between
the sum over all items and the sum over all partitions of those items.
In order to prove the stronger result of equality, we additionally
assume that the sequences xs and ys are sets, i.e., that each
element is contained at most once.
We prove that summation of f x over all x is equal to the summation of
sum_of_partition over all partitions.
Lemma sum_over_partitions_eq :
\sum_(x <- xs | P x) f x
= \sum_(y <- ys) sum_of_partition y.
Proof.
rewrite /sum_of_partition.
induction xs as [|x' xs' LE_TAIL]; first by rewrite big_nil big1_seq //= ⇒ ??; rewrite big_nil.
rewrite //= in LE_TAIL; feed_n 2 LE_TAIL.
{ by move ⇒ ??; apply H_no_partition_missing; rewrite in_cons; apply /orP; right. }
{ by move: H_xs_unique; rewrite cons_uniq ⇒ /andP [??]. }
rewrite (exchange_big_dep P) //=; last by move⇒ ??? /andP[??].
rewrite !big_cons.
destruct (P x'); last by rewrite LE_TAIL (exchange_big_dep P) //=; move⇒ ??? /andP[??].
have → : \sum_(i <- ys | true && ( x_to_y x' == i)) f x' = f x'.
{ rewrite //= -big_filter.
have → : [seq i <- ys | x_to_y x' == i] = [:: x_to_y x']; last by rewrite unlock //= addn0.
have → : [seq i <- ys | x_to_y x' == i] = [seq i <- ys | i == x_to_y x'].
{ clear H_no_partition_missing LE_TAIL.
induction ys as [| y' ys' LE_TAILy]; first by done.
feed LE_TAILy; first by move: H_ys_unique; rewrite cons_uniq ⇒ /andP [??].
by rewrite //= LE_TAILy //= eq_sym. }
apply filter_pred1_uniq ⇒ //.
by apply H_no_partition_missing; rewrite in_cons; apply /orP; left. }
apply /eqP; rewrite eqn_add2l; apply /eqP.
by rewrite LE_TAIL (exchange_big_dep P) //=; move⇒ ??? /andP[??].
Qed.
End Equality.
End SumOverPartitions.
\sum_(x <- xs | P x) f x
= \sum_(y <- ys) sum_of_partition y.
Proof.
rewrite /sum_of_partition.
induction xs as [|x' xs' LE_TAIL]; first by rewrite big_nil big1_seq //= ⇒ ??; rewrite big_nil.
rewrite //= in LE_TAIL; feed_n 2 LE_TAIL.
{ by move ⇒ ??; apply H_no_partition_missing; rewrite in_cons; apply /orP; right. }
{ by move: H_xs_unique; rewrite cons_uniq ⇒ /andP [??]. }
rewrite (exchange_big_dep P) //=; last by move⇒ ??? /andP[??].
rewrite !big_cons.
destruct (P x'); last by rewrite LE_TAIL (exchange_big_dep P) //=; move⇒ ??? /andP[??].
have → : \sum_(i <- ys | true && ( x_to_y x' == i)) f x' = f x'.
{ rewrite //= -big_filter.
have → : [seq i <- ys | x_to_y x' == i] = [:: x_to_y x']; last by rewrite unlock //= addn0.
have → : [seq i <- ys | x_to_y x' == i] = [seq i <- ys | i == x_to_y x'].
{ clear H_no_partition_missing LE_TAIL.
induction ys as [| y' ys' LE_TAILy]; first by done.
feed LE_TAILy; first by move: H_ys_unique; rewrite cons_uniq ⇒ /andP [??].
by rewrite //= LE_TAILy //= eq_sym. }
apply filter_pred1_uniq ⇒ //.
by apply H_no_partition_missing; rewrite in_cons; apply /orP; left. }
apply /eqP; rewrite eqn_add2l; apply /eqP.
by rewrite LE_TAIL (exchange_big_dep P) //=; move⇒ ??? /andP[??].
Qed.
End Equality.
End SumOverPartitions.