diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 6 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 5 |
2 files changed, 11 insertions, 0 deletions
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 2bde8dd..9a3c7d7 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -835,6 +835,9 @@ Qed. Lemma mulrnAC x m n : x *+ m *+ n = x *+ n *+ m. Proof. by rewrite -!mulrnA mulnC. Qed. +Lemma iter_addr_0 n (m : V) : iter n (+%R m) 0 = m *+ n. +Proof. by elim: n => //= n ->; rewrite mulrS. Qed. + Lemma sumrN I r P (F : I -> V) : (\sum_(i <- r | P i) - F i = - (\sum_(i <- r | P i) F i)). Proof. by rewrite (big_morph _ opprD oppr0). Qed. @@ -856,6 +859,9 @@ Lemma sumr_const (I : finType) (A : pred I) (x : V) : \sum_(i in A) x = x *+ #|A|. Proof. by rewrite big_const -iteropE. Qed. +Lemma sumr_const_nat (m n : nat) (x : V) : \sum_(n <= i < m) x = x *+ (m - n). +Proof. by rewrite big_const_nat iter_addr_0. Qed. + Lemma telescope_sumr n m (f : nat -> V) : n <= m -> \sum_(n <= k < m) (f k.+1 - f k) = f m - f n. Proof. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 6198b44..45cd336 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -2016,6 +2016,11 @@ Lemma ler_sum I (r : seq I) (P : pred I) (F G : I -> R) : \sum_(i <- r | P i) F i <= \sum_(i <- r | P i) G i. Proof. exact: (big_ind2 _ (lexx _) ler_add). Qed. +Lemma ler_sum_nat (m n : nat) (F G : nat -> R) : + (forall i, (m <= i < n)%N -> F i <= G i) -> + \sum_(m <= i < n) F i <= \sum_(m <= i < n) G i. +Proof. by move=> le_FG; rewrite !big_nat ler_sum. Qed. + Lemma psumr_eq0 (I : eqType) (r : seq I) (P : pred I) (F : I -> R) : (forall i, P i -> 0 <= F i) -> (\sum_(i <- r | P i) (F i) == 0) = (all (fun i => (P i) ==> (F i == 0)) r). |