diff options
| author | Reynald Affeldt | 2020-06-17 06:40:42 +0900 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-24 18:13:39 +0200 |
| commit | 85ea6531db1cbab7d0334438791c67f55b93cf6c (patch) | |
| tree | 134024eeace85e6391c3f1e4e80cf397984fca79 /mathcomp/algebra/ssrnum.v | |
| parent | f25ef67ad2f58a30f1e700da89811b193755d84e (diff) | |
missing lemmas discovered while developing mathcomp-analysis
Diffstat (limited to 'mathcomp/algebra/ssrnum.v')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 5 |
1 files changed, 5 insertions, 0 deletions
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). |