diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 11 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 24 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 4 |
3 files changed, 31 insertions, 8 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 251beb6..16ce76c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -46,7 +46,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `ssrnat.v`, new lemma: `oddS` - in `ssrnat.v`, new lemmas: `subnA`, `addnBn`, `addnCAC`, `addnACl` - in `finset.v`, new lemmas: `mem_imset_eq`, `mem_imset2_eq`. - These lemmas will lose the `_eq` suffix in the next release, when the shortende names will become availabe (cf. Renamed section) + These lemmas will lose the `_eq` suffix in the next release, when the shortende names will become available (cf. Renamed section) - Added a factory `distrLatticePOrderMixin` in order.v to build a `distrLatticeType` from a `porderType`. @@ -237,6 +237,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `comm_horner_mx2`, `horner_mx_stable`, `comm_mx_stable_kermxpoly`, and `comm_mx_stable_geigenspace`. +- in `ssralg.v`: + + Lemma `expr_sum` : equivalent for ring of `expn_sum` + + Lemma `prodr_natmul` : generalization of `prodrMn_const`. + Its name will become `prodrMn` in the next release when this name will become available (cf. Renamed section) + + ### Changed - in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 @@ -338,6 +344,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + `itv_gte` -> `itv_ge` + `l(t|e)r_in_itv` -> `lt_in_itv` +- in `ssralg.v` + + `prodrMn` has been renamed `prodrMn_const` (with deprecation alias, cf. Added section) + ### Removed - in `interval.v`, we remove the following: diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 3100697..5680a24 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1091,6 +1091,10 @@ Proof. by elim: m => [|m IHm]; rewrite ?mul1r // !exprS -mulrA -IHm. Qed. Lemma exprSr x n : x ^+ n.+1 = x ^+ n * x. Proof. by rewrite -addn1 exprD expr1. Qed. +Lemma expr_sum x (I : Type) (s : seq I) (P : pred I) F : + x ^+ (\sum_(i <- s | P i) F i) = \prod_(i <- s | P i) x ^+ F i :> R. +Proof. exact: (big_morph _ (exprD _)). Qed. + Lemma commr_sym x y : comm x y -> comm y x. Proof. by []. Qed. Lemma commr_refl x : comm x x. Proof. by []. Qed. @@ -1273,13 +1277,18 @@ rewrite -sum1_card; elim/big_rec3: _ => [|i x n _ _ ->]; first by rewrite mulr1. by rewrite exprS !mulrA mulN1r !mulNr commrX //; apply: commrN1. Qed. -Lemma prodrMn n (I : finType) (A : pred I) (F : I -> R) : - \prod_(i in A) (F i *+ n) = \prod_(i in A) F i *+ n ^ #|A|. +Lemma prodr_natmul (I : Type) (s : seq I) (P : pred I) + (F : I -> R) (g : I -> nat) : + \prod_(i <- s | P i) (F i *+ g i) = + \prod_(i <- s | P i) (F i) *+ \prod_(i <- s | P i) g i. Proof. -rewrite -sum1_card; elim/big_rec3: _ => // i x m _ _ ->. -by rewrite mulrnAr mulrnAl expnS mulrnA. +by elim/big_rec3: _ => // i y1 y2 y3 _ ->; rewrite mulrnAr mulrnAl -mulrnA. Qed. +Lemma prodrMn_const n (I : finType) (A : pred I) (F : I -> R) : + \prod_(i in A) (F i *+ n) = \prod_(i in A) F i *+ n ^ #|A|. +Proof. by rewrite prodr_natmul prod_nat_const. Qed. + Lemma natr_prod I r P (F : I -> nat) : (\prod_(i <- r | P i) F i)%:R = \prod_(i <- r | P i) (F i)%:R :> R. Proof. exact: (big_morph _ natrM). Qed. @@ -5667,6 +5676,7 @@ Definition expr0n := expr0n. Definition expr1n := expr1n. Definition exprD := exprD. Definition exprSr := exprSr. +Definition expr_sum := expr_sum. Definition commr_sym := commr_sym. Definition commr_refl := commr_refl. Definition commr0 := commr0. @@ -5758,7 +5768,8 @@ Definition exprMn := exprMn. Definition prodrXl := prodrXl. Definition prodrXr := prodrXr. Definition prodrN := prodrN. -Definition prodrMn := prodrMn. +Definition prodrMn_const := prodrMn_const. +Definition prodr_natmul := prodr_natmul. Definition natr_prod := natr_prod. Definition prodr_undup_exp_count := prodr_undup_exp_count. Definition exprDn := exprDn. @@ -6023,6 +6034,9 @@ Definition imaginary_exists := imaginary_exists. Notation null_fun V := (null_fun V) (only parsing). Notation in_alg A := (in_alg_loc A). +Notation prodrMn := + (fun n A F => deprecate prodrMn prodrMn_const _ n _ A F) (only parsing). + End Theory. Notation in_alg A := (in_alg_loc A). diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 0244891..a2a2395 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3462,7 +3462,7 @@ have [m leAm] := ubnP #|A|; elim: m => // m IHm in A leAm E n * => Ege0. apply/leifP; case: ifPn => [/forall_inP-Econstant | Enonconstant]. have [i /= Ai | A0] := pickP (mem A); last by rewrite [n]eq_card0 ?big_pred0. have /eqfun_inP-E_i := Econstant i Ai; rewrite -(eq_bigr _ E_i) sumr_const. - by rewrite exprMn_n prodrMn -(eq_bigr _ E_i) prodr_const. + by rewrite exprMn_n prodrMn_const -(eq_bigr _ E_i) prodr_const. set mu := \sum_(i in A) E i; pose En i := E i *+ n. pose cmp_mu s := [pred i | s * mu < s * En i]. have{Enonconstant} has_cmp_mu e (s := (-1) ^+ e): {i | i \in A & cmp_mu s i}. @@ -3495,7 +3495,7 @@ have ->: \sum_(k in A') E' k = mu *+ n'. apply: (addrI mu); rewrite -mulrS -Dn -sumrMnl (bigD1 i Ai) big_andbC /=. rewrite !(bigD1 j A'j) /= addrCA eqxx !addrA subrK; congr (_ + _). by apply: eq_bigr => k /andP[_ /negPf->]. -rewrite prodrMn exprMn_n -/n' ler_pmuln2r ?expn_gt0; last by case: (n'). +rewrite prodrMn_const exprMn_n -/n' ler_pmuln2r ?expn_gt0; last by case: (n'). have ->: \prod_(k in A') E' k = E' j * pi. by rewrite (bigD1 j) //=; congr *%R; apply: eq_bigr => k /andP[_ /negPf->]. rewrite -(ler_pmul2l mu_gt0) -exprS -Dn mulrA; apply: lt_le_trans. |