|
Section Bigmaxr. |
|
|
|
Variable (R : realDomainType). |
|
|
|
Lemma bigmaxr_mkcond I r (P : pred I) (F : I -> R) x : |
|
\big[maxr/x]_(i <- r | P i) F i = |
|
\big[maxr/x]_(i <- r) (if P i then F i else x). |
|
Proof. |
|
rewrite unlock; elim: r x => //= i r ihr x. |
|
case P; rewrite ihr // maxr_r //; elim: r {ihr} => //= j r ihr. |
|
by rewrite ler_maxr ihr orbT. |
|
Qed. |
|
|
|
Lemma bigminr_maxr I r (P : pred I) (F : I -> R) x : |
|
\big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i. |
|
Proof. |
|
by elim/big_rec2: _ => [|i y _ _ ->]; rewrite ?oppr_max opprK. |
|
Qed. |
|
|
|
Lemma bigminr_mkcond I r (P : pred I) (F : I -> R) x : |
|
\big[minr/x]_(i <- r | P i) F i = |
|
\big[minr/x]_(i <- r) (if P i then F i else x). |
|
Proof. |
|
rewrite !bigminr_maxr bigmaxr_mkcond; congr (- _). |
|
by apply: eq_bigr => i _; case P. |
|
Qed. |
|
|
|
Lemma bigmaxr_split I r (P : pred I) (F1 F2 : I -> R) x : |
|
\big[maxr/x]_(i <- r | P i) (maxr (F1 i) (F2 i)) = |
|
maxr (\big[maxr/x]_(i <- r | P i) F1 i) (\big[maxr/x]_(i <- r | P i) F2 i). |
|
Proof. |
|
by elim/big_rec3: _ => [|i y z _ _ ->]; rewrite ?maxrr // maxrCA -!maxrA maxrCA. |
|
Qed. |
|
|
|
Lemma bigminr_split I r (P : pred I) (F1 F2 : I -> R) x : |
|
\big[minr/x]_(i <- r | P i) (minr (F1 i) (F2 i)) = |
|
minr (\big[minr/x]_(i <- r | P i) F1 i) (\big[minr/x]_(i <- r | P i) F2 i). |
|
Proof. |
|
rewrite !bigminr_maxr -oppr_max -bigmaxr_split; congr (- _). |
|
by apply: eq_bigr => i _; rewrite oppr_min. |
|
Qed. |
|
|
|
Lemma filter_andb I r (a P : pred I) : |
|
[seq i <- r | P i && a i] = [seq i <- [seq j <- r | P j] | a i]. |
|
Proof. by elim: r => //= i r ->; case P. Qed. |
|
|
|
Lemma bigmaxr_idl I r (P : pred I) (F : I -> R) x : |
|
\big[maxr/x]_(i <- r | P i) F i = maxr x (\big[maxr/x]_(i <- r | P i) F i). |
|
Proof. |
|
rewrite -big_filter; elim: [seq i <- r | P i] => [|i l ihl]. |
|
by rewrite big_nil maxrr. |
|
by rewrite big_cons maxrCA -ihl. |
|
Qed. |
|
|
|
Lemma bigminr_idl I r (P : pred I) (F : I -> R) x : |
|
\big[minr/x]_(i <- r | P i) F i = minr x (\big[minr/x]_(i <- r | P i) F i). |
|
Proof. by rewrite !bigminr_maxr {1}bigmaxr_idl oppr_max opprK. Qed. |
|
|
|
Lemma bigmaxrID I r (a P : pred I) (F : I -> R) x : |
|
\big[maxr/x]_(i <- r | P i) F i = |
|
maxr (\big[maxr/x]_(i <- r | P i && a i) F i) |
|
(\big[maxr/x]_(i <- r | P i && ~~ a i) F i). |
|
Proof. |
|
rewrite -!(big_filter _ (fun _ => _ && _)) !filter_andb !big_filter. |
|
rewrite ![in RHS](bigmaxr_mkcond _ _ F) !big_filter -bigmaxr_split. |
|
have eqmax : forall i, P i -> |
|
maxr (if a i then F i else x) (if ~~ a i then F i else x) = maxr (F i) x. |
|
by move=> i _; case: (a i) => //=; rewrite maxrC. |
|
rewrite [RHS](eq_bigr _ eqmax) -!(big_filter _ P). |
|
elim: [seq j <- r | P j] => [|j l ihl]; first by rewrite !big_nil. |
|
by rewrite !big_cons -maxrA -bigmaxr_idl ihl. |
|
Qed. |
|
|
|
Lemma bigminrID I r (a P : pred I) (F : I -> R) x : |
|
\big[minr/x]_(i <- r | P i) F i = |
|
minr (\big[minr/x]_(i <- r | P i && a i) F i) |
|
(\big[minr/x]_(i <- r | P i && ~~ a i) F i). |
|
Proof. by rewrite !bigminr_maxr -oppr_max -bigmaxrID. Qed. |
|
|
|
Lemma bigmaxr_seq1 I (i : I) (F : I -> R) x : |
|
\big[maxr/x]_(j <- [:: i]) F j = maxr (F i) x. |
|
Proof. by rewrite unlock /=. Qed. |
|
|
|
Lemma bigminr_seq1 I (i : I) (F : I -> R) x : |
|
\big[minr/x]_(j <- [:: i]) F j = minr (F i) x. |
|
Proof. by rewrite unlock /=. Qed. |
|
|
|
Lemma bigmaxr_pred1_eq (I : finType) (i : I) (F : I -> R) x : |
|
\big[maxr/x]_(j | j == i) F j = maxr (F i) x. |
|
Proof. by rewrite -big_filter filter_index_enum enum1 bigmaxr_seq1. Qed. |
|
|
|
Lemma bigminr_pred1_eq (I : finType) (i : I) (F : I -> R) x : |
|
\big[minr/x]_(j | j == i) F j = minr (F i) x. |
|
Proof. by rewrite bigminr_maxr bigmaxr_pred1_eq oppr_max !opprK. Qed. |
|
|
|
Lemma bigmaxr_pred1 (I : finType) i (P : pred I) (F : I -> R) x : |
|
P =1 pred1 i -> \big[maxr/x]_(j | P j) F j = maxr (F i) x. |
|
Proof. by move/(eq_bigl _ _)->; apply: bigmaxr_pred1_eq. Qed. |
|
|
|
Lemma bigminr_pred1 (I : finType) i (P : pred I) (F : I -> R) x : |
|
P =1 pred1 i -> \big[minr/x]_(j | P j) F j = minr (F i) x. |
|
Proof. by move/(eq_bigl _ _)->; apply: bigminr_pred1_eq. Qed. |
|
|
|
Lemma bigmaxrD1 (I : finType) j (P : pred I) (F : I -> R) x : |
|
P j -> \big[maxr/x]_(i | P i) F i |
|
= maxr (F j) (\big[maxr/x]_(i | P i && (i != j)) F i). |
|
Proof. |
|
move=> Pj; rewrite (bigmaxrID _ (pred1 j)) [in RHS]bigmaxr_idl maxrA. |
|
by congr maxr; apply: bigmaxr_pred1 => i; rewrite /= andbC; case: eqP => //->. |
|
Qed. |
|
|
|
Lemma bigminrD1 (I : finType) j (P : pred I) (F : I -> R) x : |
|
P j -> \big[minr/x]_(i | P i) F i |
|
= minr (F j) (\big[minr/x]_(i | P i && (i != j)) F i). |
|
Proof. |
|
by move=> Pj; rewrite !bigminr_maxr (bigmaxrD1 _ _ Pj) oppr_max opprK. |
|
Qed. |
|
|
|
Lemma ler_bigmaxr_cond (I : finType) (P : pred I) (F : I -> R) x i0 : |
|
P i0 -> F i0 <= \big[maxr/x]_(i | P i) F i. |
|
Proof. by move=> Pi0; rewrite (bigmaxrD1 _ _ Pi0) ler_maxr lerr. Qed. |
|
|
|
Lemma bigminr_ler_cond (I : finType) (P : pred I) (F : I -> R) x i0 : |
|
P i0 -> \big[minr/x]_(i | P i) F i <= F i0. |
|
Proof. by move=> Pi0; rewrite (bigminrD1 _ _ Pi0) ler_minl lerr. Qed. |
|
|
|
Lemma ler_bigmaxr (I : finType) (F : I -> R) (i0 : I) x : |
|
F i0 <= \big[maxr/x]_i F i. |
|
Proof. exact: ler_bigmaxr_cond. Qed. |
|
|
|
Lemma bigminr_ler (I : finType) (F : I -> R) (i0 : I) x : |
|
\big[minr/x]_i F i <= F i0. |
|
Proof. exact: bigminr_ler_cond. Qed. |
|
|
|
Lemma bigmaxr_lerP (I : finType) (P : pred I) m (F : I -> R) x : |
|
reflect (x <= m /\ forall i, P i -> F i <= m) |
|
(\big[maxr/x]_(i | P i) F i <= m). |
|
Proof. |
|
apply: (iffP idP) => [|[lexm leFm]]; last first. |
|
by elim/big_ind: _ => // ??; rewrite ler_maxl =>->. |
|
rewrite bigmaxr_idl ler_maxl => /andP[-> leFm]; split=> // i Pi. |
|
by apply: ler_trans leFm; apply: ler_bigmaxr_cond. |
|
Qed. |
|
|
|
Lemma bigminr_gerP (I : finType) (P : pred I) m (F : I -> R) x : |
|
reflect (m <= x /\ forall i, P i -> m <= F i) |
|
(m <= \big[minr/x]_(i | P i) F i). |
|
Proof. |
|
rewrite bigminr_maxr ler_oppr; apply: (iffP idP). |
|
by move=> /bigmaxr_lerP [? lemF]; split=> [|??]; rewrite -ler_opp2 ?lemF. |
|
by move=> [? lemF]; apply/bigmaxr_lerP; split=> [|??]; rewrite ler_opp2 ?lemF. |
|
Qed. |
|
|
|
Lemma bigmaxr_sup (I : finType) i0 (P : pred I) m (F : I -> R) x : |
|
P i0 -> m <= F i0 -> m <= \big[maxr/x]_(i | P i) F i. |
|
Proof. by move=> Pi0 ?; apply: ler_trans (ler_bigmaxr_cond _ _ Pi0). Qed. |
|
|
|
Lemma bigminr_inf (I : finType) i0 (P : pred I) m (F : I -> R) x : |
|
P i0 -> F i0 <= m -> \big[minr/x]_(i | P i) F i <= m. |
|
Proof. by move=> Pi0 ?; apply: ler_trans (bigminr_ler_cond _ _ Pi0) _. Qed. |
|
|
|
Lemma bigmaxr_ltrP (I : finType) (P : pred I) m (F : I -> R) x : |
|
reflect (x < m /\ forall i, P i -> F i < m) |
|
(\big[maxr/x]_(i | P i) F i < m). |
|
Proof. |
|
apply: (iffP idP) => [|[ltxm ltFm]]; last first. |
|
by elim/big_ind: _ => // ??; rewrite ltr_maxl =>->. |
|
rewrite bigmaxr_idl ltr_maxl => /andP[-> ltFm]; split=> // i Pi. |
|
by apply: ler_lt_trans ltFm; apply: ler_bigmaxr_cond. |
|
Qed. |
|
|
|
Lemma bigminr_gtrP (I : finType) (P : pred I) m (F : I -> R) x : |
|
reflect (m < x /\ forall i, P i -> m < F i) |
|
(m < \big[minr/x]_(i | P i) F i). |
|
Proof. |
|
rewrite bigminr_maxr ltr_oppr; apply: (iffP idP). |
|
by move=> /bigmaxr_ltrP [? ltmF]; split=> [|??]; rewrite -ltr_opp2 ?ltmF. |
|
by move=> [? ltmF]; apply/bigmaxr_ltrP; split=> [|??]; rewrite ltr_opp2 ?ltmF. |
|
Qed. |
|
|
|
Lemma bigmaxr_gerP (I : finType) (P : pred I) m (F : I -> R) x : |
|
reflect (m <= x \/ exists2 i, P i & m <= F i) |
|
(m <= \big[maxr/x]_(i | P i) F i). |
|
Proof. |
|
apply: (iffP idP) => [|[lemx|[i Pi lemFi]]]; last 2 first. |
|
- by rewrite bigmaxr_idl ler_maxr lemx. |
|
- by rewrite (bigmaxrD1 _ _ Pi) ler_maxr lemFi. |
|
rewrite lerNgt => /bigmaxr_ltrP /asboolPn. |
|
rewrite asbool_and negb_and => /orP [/asboolPn/negP|/existsp_asboolPn [i]]. |
|
by rewrite -lerNgt; left. |
|
by move=> /asboolPn/imply_asboolPn [Pi /negP]; rewrite -lerNgt; right; exists i. |
|
Qed. |
|
|
|
Lemma bigminr_lerP (I : finType) (P : pred I) m (F : I -> R) x : |
|
reflect (x <= m \/ exists2 i, P i & F i <= m) |
|
(\big[minr/x]_(i | P i) F i <= m). |
|
Proof. |
|
rewrite bigminr_maxr ler_oppl; apply: (iffP idP). |
|
by move=> /bigmaxr_gerP [?|[i ??]]; [left|right; exists i => //]; |
|
rewrite -ler_opp2. |
|
by move=> [?|[i ??]]; apply/bigmaxr_gerP; [left|right; exists i => //]; |
|
rewrite ler_opp2. |
|
Qed. |
|
|
|
Lemma bigmaxr_gtrP (I : finType) (P : pred I) m (F : I -> R) x : |
|
reflect (m < x \/ exists2 i, P i & m < F i) |
|
(m < \big[maxr/x]_(i | P i) F i). |
|
Proof. |
|
apply: (iffP idP) => [|[ltmx|[i Pi ltmFi]]]; last 2 first. |
|
- by rewrite bigmaxr_idl ltr_maxr ltmx. |
|
- by rewrite (bigmaxrD1 _ _ Pi) ltr_maxr ltmFi. |
|
rewrite ltrNge => /bigmaxr_lerP /asboolPn. |
|
rewrite asbool_and negb_and => /orP [/asboolPn/negP|/existsp_asboolPn [i]]. |
|
by rewrite -ltrNge; left. |
|
by move=> /asboolPn/imply_asboolPn [Pi /negP]; rewrite -ltrNge; right; exists i. |
|
Qed. |
|
|
|
Lemma bigminr_ltrP (I : finType) (P : pred I) m (F : I -> R) x : |
|
reflect (x < m \/ exists2 i, P i & F i < m) |
|
(\big[minr/x]_(i | P i) F i < m). |
|
Proof. |
|
rewrite bigminr_maxr ltr_oppl; apply: (iffP idP). |
|
by move=> /bigmaxr_gtrP [?|[i ??]]; [left|right; exists i => //]; |
|
rewrite -ltr_opp2. |
|
by move=> [?|[i ??]]; apply/bigmaxr_gtrP; [left|right; exists i => //]; |
|
rewrite ltr_opp2. |
|
Qed. |
|
|
|
End Bigmaxr. |
|
|
|
Arguments bigmaxr_mkcond {R I r}. |
|
Arguments bigmaxrID {R I r}. |
|
Arguments bigmaxr_pred1 {R I} i {P F}. |
|
Arguments bigmaxrD1 {R I} j {P F}. |
|
Arguments ler_bigmaxr_cond {R I P F}. |
|
Arguments ler_bigmaxr {R I F}. |
|
Arguments bigmaxr_sup {R I} i0 {P m F}. |
|
Arguments bigminr_mkcond {R I r}. |
|
Arguments bigminrID {R I r}. |
|
Arguments bigminr_pred1 {R I} i {P F}. |
|
Arguments bigminrD1 {R I} j {P F}. |
|
Arguments bigminr_ler_cond {R I P F}. |
|
Arguments bigminr_ler {R I F}. |
|
Arguments bigminr_inf {R I} i0 {P m F}. |