diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 24 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 4 |
2 files changed, 21 insertions, 7 deletions
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 6128fa0..918c2d3 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1089,6 +1089,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. @@ -1263,13 +1267,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. @@ -5654,6 +5663,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. @@ -5742,7 +5752,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. @@ -6007,6 +6018,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 2ebbdcc..974c81e 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3435,7 +3435,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}. @@ -3468,7 +3468,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. |