sum.v 9.4 KB
 Björn Brandenburg committed Dec 04, 2019 1 2 ``````Require Export rt.util.notation. Require Export rt.util.nat. `````` Björn Brandenburg committed Nov 19, 2019 3 `````` `````` Felipe Cerqueira committed Jun 06, 2016 4 ``````From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path. `````` Felipe Cerqueira committed Mar 31, 2016 5 `````` `````` Sergey Bozhko committed Apr 05, 2019 6 ``````(* Lemmas about sum. *) `````` Felipe Cerqueira committed Oct 18, 2016 7 8 9 10 11 12 13 14 ``````Section ExtraLemmas. Lemma leq_sum_seq (I: eqType) (r: seq I) (P : pred I) (E1 E2 : I -> nat) : (forall 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. `````` Sergey Bozhko committed Apr 05, 2019 15 `````` by apply leq_sum; move => j /andP [IN H]; apply LE. `````` Felipe Cerqueira committed Oct 18, 2016 16 17 `````` Qed. `````` Sergey Bozhko committed Nov 19, 2019 18 19 20 21 22 23 24 25 26 27 `````` Lemma eq_sum_seq: forall (I: eqType) (r: seq I) (P: pred I) (E1 E2 : I -> nat), (forall 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; rewrite eqn_leq; apply/andP; split. - apply leq_sum_seq; intros. by move: (H i H0 H1) => /eqP EQ; rewrite EQ. - apply leq_sum_seq; intros. by move: (H i H0 H1) => /eqP EQ; rewrite EQ. Qed. `````` Björn Brandenburg committed Nov 15, 2019 28 `````` `````` Felipe Cerqueira committed Oct 18, 2016 29 30 31 32 `````` Lemma sum_nat_eq0_nat (T : eqType) (F : T -> nat) (r: seq T) : all (fun x => F x == 0) r = (\sum_(i <- r) F i == 0). Proof. destruct (all (fun x => F x == 0) r) eqn:ZERO. `````` Sergey Bozhko committed Sep 24, 2019 33 `````` - move: ZERO => /allP ZERO; rewrite -leqn0. `````` Felipe Cerqueira committed Oct 18, 2016 34 35 36 37 `````` rewrite big_seq_cond (eq_bigr (fun x => 0)); first by rewrite big_const_seq iter_addn mul0n addn0 leqnn. intro i; rewrite andbT; intros IN. specialize (ZERO i); rewrite IN in ZERO. `````` Sergey Bozhko committed Apr 05, 2019 38 `````` by move: ZERO => /implyP ZERO; apply/eqP; apply ZERO. `````` Sergey Bozhko committed Sep 24, 2019 39 `````` - apply negbT in ZERO; rewrite -has_predC in ZERO. `````` Felipe Cerqueira committed Oct 18, 2016 40 41 42 43 `````` move: ZERO => /hasP ZERO; destruct ZERO as [x IN NEQ]; simpl in NEQ. rewrite (big_rem x) /=; last by done. symmetry; apply negbTE; rewrite neq_ltn; apply/orP; right. apply leq_trans with (n := F x); last by apply leq_addr. `````` Sergey Bozhko committed Apr 05, 2019 44 `````` by rewrite lt0n. `````` Felipe Cerqueira committed Oct 18, 2016 45 `````` Qed. `````` Björn Brandenburg committed Nov 15, 2019 46 `````` `````` Sergey Bozhko committed Apr 05, 2019 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 `````` Lemma sum_seq_gt0P: forall (T:eqType) (r: seq T) (F: T -> nat), reflect (exists i, i \in r /\ 0 < F i) (0 < \sum_(i <- r) F i). Proof. intros; apply: (iffP idP); intros. { induction r; first by rewrite big_nil in H. destruct (F a > 0) eqn:POS. exists a; split; [by rewrite in_cons; apply/orP; left | by done]. apply negbT in POS; rewrite -leqNgt leqn0 in POS; move: POS => /eqP POS. rewrite big_cons POS add0n in H. clear POS. feed IHr; first by done. move: IHr => [i [IN POS]]. exists i; split; [by rewrite in_cons; apply/orP;right | by done]. } { move: H => [i [IN POS]]. rewrite (big_rem i) //=. apply leq_trans with (F i); [by done | by rewrite leq_addr]. } Qed. `````` Sergey Bozhko committed Nov 19, 2019 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 `````` Lemma sum_notin_rem_eqn: forall (T:eqType) (a: T) xs P F, a \notin xs -> \sum_(x <- xs | P x && (x != a)) F x = \sum_(x <- xs | P x) F x. Proof. intros ? ? ? ? ? NOTIN. induction xs; first by rewrite !big_nil. rewrite !big_cons. rewrite IHxs; clear IHxs; last first. { apply/memPn; intros y IN. move: NOTIN => /memPn NOTIN. by apply NOTIN; rewrite in_cons; apply/orP; right. } 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. Qed. `````` Björn Brandenburg committed May 16, 2019 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 `````` (* 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. (* A sum of natural numbers equals zero iff all terms are zero. *) Lemma big_nat_eq0 m n F: \sum_(m <= i < n) F i = 0 <-> (forall 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. `````` Sergey Bozhko committed Dec 10, 2019 110 `````` (* We prove that if any element of a set r is bounded by constant [const], `````` Sergey Bozhko committed Apr 05, 2019 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 `````` then the sum of the whole set is bounded by [const * size r]. *) Lemma sum_majorant_constant: forall (T: eqType) (r: seq T) (P: pred T) F const, (forall a, a \in r -> P a -> F a <= const) -> \sum_(j <- r | P j) F j <= const * (size [seq j <- r | P j]). Proof. clear; intros. induction r; first by rewrite big_nil. feed IHr. { 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. rewrite mulnDr. apply leq_add; last by done. rewrite size_filter. simpl; rewrite addn0. rewrite EQ muln1. apply H; last by done. by rewrite in_cons; apply/orP; left. } { apply leq_trans with (const * size [seq j <- r | P j]); first by done. rewrite leq_mul2l; apply/orP; right. rewrite -cat1s filter_cat size_cat. by rewrite leq_addl. } Qed. `````` Sergey Bozhko committed Dec 10, 2019 141 `````` (* We prove that if for any element x of a set [xs] the following two statements hold `````` Sergey Bozhko committed Apr 05, 2019 142 143 `````` (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 `````` Sergey Bozhko committed Dec 10, 2019 144 `````` any element x of [xs]. *) `````` Sergey Bozhko committed Apr 05, 2019 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 `````` Lemma sum_majorant_eqn: forall (T: eqType) xs F1 F2 (P: pred T), (forall x, x \in xs -> P x -> F1 x <= F2 x) -> \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x -> (forall x, x \in xs -> P x -> F1 x = F2 x). Proof. intros T xs F1 F2 P H1 H2 x IN PX. induction xs; first by done. have Fact: \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 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: forall a b c d, a + b = c + d -> a <= c -> b >= d. `````` Sergey Bozhko committed Sep 24, 2019 164 `````` { clear; intros; ssromega. } `````` Sergey Bozhko committed Apr 05, 2019 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 `````` move: IN; rewrite in_cons; move => /orP [/eqP EQ | IN]. { subst a. rewrite PX in H2. specialize (H1 x). feed_n 2 H1; [ by rewrite in_cons; apply/orP; left | by done | ]. move: (EqLeq (F1 x) (\sum_(j <- xs | P j) F1 j) (F2 x) (\sum_(j <- xs | P j) F2 j) H2 H1) => Q. have EQ: \sum_(j <- xs | P j) F1 j = \sum_(j <- xs | P j) F2 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 (F1 a) (\sum_(j <- xs | P j) F1 j) (F2 a) (\sum_(j <- xs | P j) F2 j) H2 H1) => Q. by apply/eqP; rewrite eqn_leq; apply/andP; split. } Qed. (* We prove that the sum of Δ ones is equal to Δ. *) Lemma sum_of_ones: forall t Δ, \sum_(t <= x < t + Δ) 1 = Δ. Proof. intros. `````` Björn Brandenburg committed Nov 15, 2019 194 `````` rewrite big_const_nat iter_addn_0 mul1n. `````` Sergey Bozhko committed Apr 05, 2019 195 196 197 `````` rewrite addnC -addnBA; last by done. by rewrite subnn addn0. Qed. `````` Sergey Bozhko committed Aug 20, 2019 198 `````` `````` Sergey Bozhko committed Nov 19, 2019 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 `````` (* We show that 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 : forall f t Δ, \sum_(t <= x < t + Δ) f x < Δ -> exists x, t <= x < t + Δ /\ f x = 0. Proof. induction Δ; intros; first by rewrite ltn0 in H. destruct (f (t + Δ)) eqn: EQ. { exists (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]]. exists z; split; last by done. apply/andP; split; first by done. by rewrite ltnS ltnW. } Qed. `````` Sergey Bozhko committed Apr 05, 2019 220 221 `````` End ExtraLemmas. `````` Sergey Bozhko committed Nov 19, 2019 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 `````` (* Lemmas about arithmetic with sums. *) Section SumArithmetic. Lemma sum_seq_diff: forall (T:eqType) (rs: seq T) (F G : T -> nat), (forall i : T, i \in rs -> G i <= F i) -> \sum_(i <- rs) (F i - G i) = \sum_(i <- rs) F i - \sum_(i <- rs) G i. Proof. intros. induction rs; first by rewrite !big_nil subn0. rewrite !big_cons subh2. - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHrs. by intros; apply H; rewrite in_cons; apply/orP; right. - by apply H; 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 H; rewrite in_cons; apply/orP; right. Qed. Lemma sum_diff: forall n F G, (forall i (LT: 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. Lemma sum_pred_diff: forall (T: eqType) (rs: seq T) (P: T -> bool) (F: T -> nat), \sum_(r <- rs | P r) F r = \sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r. Proof. clear; intros. induction rs; first by rewrite !big_nil subn0. rewrite !big_cons !IHrs; clear IHrs. 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. End SumArithmetic.``````