Module mathcomp.classical.fsbigop

From mathcomp Require Import boot order ssralg ssrnum ssrint interval finmap.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions cardinality.

# Finitely-supported big operators ``` finite_support idx D F := D `&` F @^-1` [set~ idx] \big[op/idx]_(i \in A) F i == iterated application of the operator op with neutral idx over finite_support idx A F \sum_(i \in A) F i == iterated addition, in ring_scope ```

Reserved Notation "\big [ op / idx ]_ ( i '\in' A ) F"
  (F at level 36, A at level 60,
           format "'[' \big [ op / idx ]_ ( i '\in' A ) '/ ' F ']'").

Reserved Notation "\sum_ ( i '\in' A ) F"
  (F at level 41, A at level 60,
    format "'[' \sum_ ( i '\in' A ) '/ ' F ']'").

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Notation :=
  (\big[op/idx]_( <- fset_set (A `&` ((fun => F) @^-1` [set~ idx]))) F)
    (only parsing) : big_scope.

Lemma : unit

Proof.

exact: tt. Qed.

Definition { : choiceType} { : Type} ( : T) ( : set I)
    ( : I -> T) : seq I :=
  locked_with finite_index_key (fset_set (D `&` F @^-1` [set~ idx] : set I)).
Notation :=
    (\big[op/idx]_( <- finite_support idx D (fun => F)) F)
  : big_scope.

Lemma ( : Type) ( : choiceType) ( : T) ( : set J)
    ( : J -> T) : finite_set (P `&` F @^-1` [set~ i]) ->
  finite_support i P F =i P `&` F @^-1` [set~ i].

Proof.

by move=> finF j; rewrite /finite_support unlock in_fset_set. Qed.

Lemma ( : Type) ( : choiceType) ( : T) ( : set J)
( : J -> T) : uniq (finite_support i P F).

Proof.

by rewrite /finite_support unlock; exact: fset_uniq. Qed.

#[global] Hint Resolve finite_support_uniq : core.

Lemma ( : Type) ( : choiceType) ( : T) ( : set J)
( : J -> T) : infinite_set (P `&` F @^-1` [set~ i]) ->
finite_support i P F = [::].

Proof.

move=> infinF; rewrite /finite_support unlock.
by rewrite /fset_set/=; case: pselect => //.
Qed.

Lemma { : choiceType} { : Type} ( : T) ( : set I)
( : I -> T) : {in D, F =1 G} ->
finite_support idx D F = finite_support idx D G.

Proof.

by move=> eqFG; rewrite /finite_support !unlock// (eq_preimage _ eqFG).
Qed.

Variant ( : choiceType)
  ( : set T) ( : T -> R) ( : R) : seq T -> Type :=
| of infinite_set (P `&` F @^-1` [set~ idx]) :
    finite_support_spec P F idx [::]
| ( : {fset T}) of [set` X] `<=` P
   & (forall , P i -> i \notin X -> F i = idx)
   & [set` X] = (P `&` F @^-1` [set~ idx]) :
    finite_support_spec P F idx X.

Lemma ( : choiceType) ( : set T) ( : T -> R) ( : R) :
  finite_support_spec P F idx (finite_support idx P F).

Proof.

rewrite /finite_support unlock/= /fset_set.
case: pselect=> // Xfin; last by constructor.
case: cid => //= X eqX; constructor; rewrite -?eqX//.
move=> i Pi NXi /=; have : (P `\` [set` X]) i by split=> //=; apply/negP.
by rewrite -eqX /= => -[_]; apply: contra_notP.
Qed.

Notation := (\big[+%R/0%R]_( \in A) F) : ring_scope.

Lemma ( : Type) ( : R) ( : R -> R -> R)
( : choiceType) ( : T -> R) ( : set T) :
P = Q -> \big[op/idx]_( \in P) f x = \big[op/idx]_( \in Q) f x.

Proof.

by move=> ->. Qed.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
( : choiceType) ( : T -> R) ( : set T) :
{in P, f =1 g} -> (\big[op/idx]_( \in P) f x = \big[op/idx]_( \in P) g x).

Proof.

move=> fg; rewrite (eq_finite_support _ fg); apply: eq_big_seq => x.
by case: finite_supportP => //= X XP _ gidx xX; rewrite fg // ?inE; apply/XP.
Qed.

Arguments eq_fsbigr {R idx op T f} g.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx) ( : choiceType)
    ( : {fset T}) ( : T -> R) :
    (forall , i \notin A -> f i = idx) ->
  \big[op/idx]_( \in [set: T]) f i = \big[op/idx]_( <- A) f i.

Proof.

elim/Peq: R => R in idx op f *.
move=> Af; have Afin : finite_set (f @^-1` [set~ idx]).
  by apply: (finite_subfset A) => x; apply: contra_notT => /Af.
rewrite [in RHS](big_fsetID _ [pred | f x == idx])/=.
rewrite [X in _ = op X _]big_fset [X in _ = op X _]big1 ?Monoid.simpm//.
  by move=> i /= /eqP.
apply eq_fbigl => r.
rewrite in_finite_support// ?setTI// /preimage/=; apply/idP/idP => /=.
  rewrite !inE/=; apply: contra_notP => /negP.
  by rewrite negb_and negbK => /orP[|/eqP//]; exact: Af.
by rewrite !inE/= => /andP[_ /eqP].
Qed.

Arguments fsbigTE {R idx op T} A f.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
    ( : choiceType) ( : set T) ( : T -> R) :
  \big[op/idx]_( \in A) f i =
  \big[op/idx]_( \in [set: T]) patch (fun=> idx) A f i.

Proof.

elim/Peq: R => R in idx op f *.
rewrite -big_mkcond/= -[in RHS]big_filter; apply: perm_big.
rewrite uniq_perm ?filter_uniq//= => i; rewrite mem_filter.
set g := fun => if i \in A then f i else idx.
have gAf : setT `&` g @^-1` [set~ idx] = (A `&` f @^-1` [set~ idx]).
  rewrite setTI; apply/predeqP => x; split; rewrite /preimage/g/=.
    by case: ifPn; rewrite (inE, notin_setE).
  by case: ifPn; rewrite (inE, notin_setE) => ? [].
case: finite_supportP => //.
  rewrite -gAf; case: finite_supportP=> //=; first by rewrite ?inE andbF.
  by move=> X _ gidx <-//.
move=> X XA fidx XE; case: finite_supportP; rewrite gAf -?XE//=.
move=> Y _ gidx /predeqP/=/(_ _)/propext YX.
by apply/idP/andP => [|[]]; rewrite YX// inE => Xi; split=> //; apply: XA.
Qed.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
    ( : choiceType) ( : set T) ( : T -> R) :
  \big[op/idx]_( \in I `&` J) a i =
  \big[op/idx]_( \in I) if i \in J then a i else idx.

Proof.

rewrite fsbig_mkcond [RHS]fsbig_mkcond.
by under eq_fsbigr do rewrite patch_setI.
Qed.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
    ( : choiceType) ( : set T) ( : T -> R) :
  \big[op/idx]_( \in I `&` J) a i =
  \big[op/idx]_( \in J) if i \in I then a i else idx.

Proof.

rewrite fsbig_mkcond [RHS]fsbig_mkcond setIC.
by under eq_fsbigr do rewrite patch_setI.
Qed.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx) ( : choiceType)
    ( : seq T) ( : {pred T}) ( : T -> R) : uniq r ->
    (forall , P i -> i \notin r -> f i = idx) ->
  \big[op/idx]_( <- r | P i) f i = \big[op/idx]_( \in [set` P]) f i.

Proof.

move=> r_uniq fidx; rewrite fsbig_mkcond.
rewrite (fsbigTE [fset x | in r]%fset).
by move=> i; rewrite inE/= /patch mem_setE; case: ifP=> // + /fidx->.
rewrite -big_mkcond; under [RHS]eq_bigl do rewrite mem_setE.
by apply: perm_big; rewrite uniq_perm// => i; rewrite !inE.
Qed.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx) ( : choiceType)
    ( : set T) ( : seq T) ( : T -> R) :
    uniq r ->
    [set` r] `<=` A ->
    (forall , A i -> i \notin r -> f i = idx) ->
  \big[op/idx]_( \in A) f i = \big[op/idx]_( <- r | i \in A) f i.

Proof.

move=> r_uniq rQ fidx; rewrite [RHS]bigfs ?set_mem_set//=.
by move=> i; rewrite inE; apply: fidx.
Qed.

Arguments fsbigE {R idx op T A}.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
    ( : choiceType) ( : seq I) ( : I -> R) :
  uniq r ->
  \big[op/idx]_( <- r) F a = \big[op/idx]_( \in [set` r]) F a.

Proof.

move=> ur; rewrite (fsbigE r)//=; first by move=> + ->.
by rewrite mem_setE big_seq_cond big_mkcondr.
Qed.

Lemma ( : Type) ( : R) ( : Monoid.law idx) ( : choiceType)
( : set I) ( : I -> R) :
(forall , P i -> F i = idx) -> \big[op/idx]_( \in P) F i = idx.

Proof.

move=> PF0; rewrite big1_seq// => i/=; case: finite_supportP=> //=.
by move=> X XP _ _ Xi; rewrite PF0//; apply/XP.
Qed.

Lemma ( : Type) ( : R) ( : Monoid.law idx) ( : choiceType)
( : set I) ( : I -> R) :
infinite_set (P `&` F @^-1` [set~ idx])-> \big[op/idx]_( \in P) F i = idx.

Proof.

by case: finite_supportP; rewrite ?big_nil// => X _ _ <-. Qed.

Lemma ( : choiceType) [ : Type] [ : R]
    ( : Monoid.com_law idx) ( : set T) ( : T -> R) :
    P `<=` D ->
    D `\` P `<=` f @^-1` [set idx] ->
  \big[op/idx]_( \in P) f i = \big[op/idx]_( \in D) f i.

Proof.

move=> PD DPf; rewrite fsbig_mkcond [RHS]fsbig_mkcond.
apply: eq_fsbigr => x _; rewrite /patch; case: ifPn; rewrite (inE, notin_setE).
by move=> Px; rewrite ifT// inE; apply: PD.
by move=> Px; case: ifP => //; rewrite inE => Dx; rewrite DPf.
Qed.

Arguments fsbig_widen {T R idx op} P D f.

Lemma ( : choiceType) [ : Type] [ : R]
( : Monoid.com_law idx) ( : set T) ( : T -> R) :
\big[op/idx]_( \in P) f i = \big[op/idx]_( \in P `&` f @^-1` [set~ idx]) f i.

Proof.

by apply/esym/fsbig_widen => // x [Px /not_andP[]//=]; rewrite notK. Qed.

Lemma ( : choiceType) [ : eqType] [ : R]
    ( : Monoid.com_law idx)
    ( : seq T) ( : set T) ( : T -> R) :
  P `<=` [set` r] ->
  uniq r ->
  [set | i \in r] `\` P `<=` f @^-1` [set idx] ->
  \big[op/idx]_( \in P) f i = \big[op/idx]_( <- r) f i.

Proof.

by move=> *; rewrite (fsbig_widen _ [set` r])// [RHS]fsbig_seq. Qed.

Arguments fsbig_fwiden {T R idx op} r P f.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx) ( : choiceType)
( : T -> R) : \big[op/idx]_( \in set0) F x = idx.

Proof.

by rewrite (fsbigE [::])// big_nil. Qed.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx) ( : choiceType)
( : T -> R) : \big[op/idx]_( \in [set x]) F y = F x.

Proof.

rewrite (fsbigE [:: x])//= ?big_cons ?big_nil ?ifT ?inE ?Monoid.simpm//.
by move=> y /=; rewrite inE => /eqP.
by move=> i ->; rewrite inE eqxx.
Qed.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
    ( : choiceType) ( : set I) ( : set I) ( : I -> R) :
  finite_set (A `&` F @^-1` [set~ idx]) ->
  \big[op/idx]_( \in A) F i = op (\big[op/idx]_( \in A `&` B) F i)
                                  (\big[op/idx]_( \in A `&` ~` B) F i).

Proof.

move=> finF.
have fsbig_setI C : \big[op/idx]_( <-
      [fset x | in fset_set (A `&` F @^-1` [set~ idx]) & x \in C]%fset) F i =
    \big[op/idx]_( \in A `&` C) F i.
  apply: eq_fbigl => i /=; apply/idP/idP.
    rewrite !inE/= => /andP[+ Bi]; rewrite in_fset_set// inE => -[Ai Fi].
    rewrite unlock in_fset_set ?inE// setIAC; last by rewrite inE in Bi.
    exact/finite_setIl.
  rewrite unlock in_fset_set; first by rewrite setIAC; exact/finite_setIl.
  by rewrite inE => -[[Ai Bi] Fi0]; rewrite !inE/= in_fset_set// !mem_set.
rewrite (big_fsetID _ [pred | i \in B])/= [locked_with _ _]unlock.
rewrite fsbig_setI; congr (op _ _); rewrite -fsbig_setI.
by apply eq_fbigl => i; rewrite !inE in_setC.
Qed.

Arguments __deprecated__full_fsbigID {R idx op I} B.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
    ( : choiceType) ( : set I) ( : set I) ( : I -> R) :
    finite_set A ->
  \big[op/idx]_( \in A) F i = op (\big[op/idx]_( \in A `&` B) F i)
                                  (\big[op/idx]_( \in A `&` ~` B) F i).

Proof.

by move=> Afin; apply: __deprecated__full_fsbigID; apply: finite_setIl. Qed.

Arguments fsbigID {R idx op I} B.

#[deprecated(note="Use fsbigID instead")]
Notation := __deprecated__full_fsbigID (only parsing).

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
    ( : choiceType) ( : set I) ( : I -> R) :
    finite_set A -> finite_set B -> A `&` B `<=` F @^-1` [set idx] ->
  \big[op/idx]_( \in A `|` B) F i =
     op (\big[op/idx]_( \in A) F i) (\big[op/idx]_( \in B) F i).

Proof.

move=> Afin Bfin AB0; rewrite (fsbigID A) ?finite_setU; first by split.
rewrite setUK -setDE; congr (op _ _); rewrite setDE setIUl setICr set0U.
by apply: fsbig_widen => //; rewrite -setDE setDD setIC.
Qed.

Arguments fsbigU {R idx op I} [A B F].

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
    ( : choiceType) ( : set I) ( : I -> R) :
    finite_set A -> finite_set B -> A `&` B `<=` set0 ->
  \big[op/idx]_( \in A `|` B) F i =
     op (\big[op/idx]_( \in A) F i) (\big[op/idx]_( \in B) F i).

Proof.

by move=> Af Bf AB0; rewrite fsbigU// => x /AB0. Qed.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
    ( : choiceType) ( : I) ( : set I) ( : I -> R) :
     finite_set A -> A i ->
  \big[op/idx]_( \in A) F j = op (F i) (\big[op/idx]_( \in A `\ i) F j).

Proof.

by move=> *; rewrite (fsbigID [set i]) ?setI1 ?ifT ?inE ?fsbig_set1. Qed.

Arguments fsbigD1 {R idx op I} i A F.

Lemma ( : Type) ( : R) ( : Monoid.mul_law zero)
    ( : Monoid.add_law zero times) ( : choiceType) ( : R) ( : set I)
    ( : I -> R) :
  finite_set (P `&` F @^-1` [set~ zero]) ->
  times a (\big[plus/zero]_( \in P) F i) =
  \big[plus/zero]_( \in P) times a (F i).

Proof.

move=> finF; elim/Peq : R => R in zero times plus a F finF *.
have [->|a0] := eqVneq a zero.
  by rewrite Monoid.mul0m fsbig1//; move=> i _; rewrite Monoid.mul0m.
#[warning="deprecated"] (* FIXME *)
rewrite big_distrr [RHS](full_fsbigID (F @^-1` [set zero])).
  apply: sub_finite_set finF => x /= [Px aFN0].
  by split=> //; apply: contra_not aFN0 => ->; rewrite Monoid.simpm.
set b0 := bigop _ _ _.
set b1 := bigop _ _ _.
set b2 := bigop _ _ _.
rewrite (_ : b1 = zero) ?Monoid.simpm.
  by rewrite /b1 fsbig1// => i [_ ->]; rewrite Monoid.simpm.
apply/esym/fsbig_fwiden => //.
  by move=> x [Px Fx0]; rewrite /= in_finite_support// inE.
move=> i []; rewrite /preimage/= in_finite_support //.
by rewrite !inE => -[Pi]; rewrite /preimage/= => Fi0; tauto.
Qed.

Lemma ( : Type) ( : R) ( : Monoid.mul_law zero)
    ( : Monoid.add_law zero times) ( : choiceType) ( : R) ( : set I)
    ( : I -> R) :
  finite_set P ->
  times a (\big[plus/zero]_( \in P) F i) =
  \big[plus/zero]_( \in P) times a (F i).

Proof.

by move=> Pf; apply: full_fsbig_distrr; apply: finite_setIl. Qed.

Lemma ( : idomainType) ( : choiceType) ( : set I) ( : I -> R) :
a * (\sum_( \in P) F i) = \sum_( \in P) a * F i.

Proof.

have [->|aN0] := eqVneq a 0; first by rewrite mul0r big1// => i; rewrite mul0r.
case: (pselect (finite_set (P `&` F @^-1` [set~ 0]))) => PFfin.
exact: full_fsbig_distrr.
rewrite !fsbig_dflt ?mulr0//; apply: contra_not PFfin; apply: sub_finite_set.
by move=> x [Px /eqP Fx0]; split=> //=; apply/eqP; rewrite mulf_neq0.
Qed.

Lemma ( : idomainType) ( : choiceType) ( : set I) ( : I -> R) :
(\sum_( \in P) F i) * a = \sum_( \in P) (F i * a).

Proof.

by rewrite mulrC mulr_fsumr; under eq_fsbigr do rewrite mulrC. Qed.

Lemma ( : R) ( : Monoid.com_law idx) ( : nat -> R) :
\big[op/idx]_( < n) F a = \big[op/idx]_( \in `I_n) F a.

Proof.

rewrite -(big_mkord xpredT) [LHS]fsbig_seq ?iota_uniq//.
by apply: eq_fsbigl; rewrite -Iiota /index_iota subn0.
Qed.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx) ( : choiceType)
( : set T) ( : T -> R) : finite_set D ->
\big[op/idx]_( \in D) F x = \big[op/idx]_( <- fset_set D) F x.

Proof.

elim/Peq: R => R in idx op F * => Dfin.
by apply: fsbig_fwiden; rewrite ?fset_setK// setDv.
Qed.

Section fsbig2.
Variables ( : Type) ( : R) ( : Monoid.com_law idx).

Lemma { : choiceType} ( : I -> J)
( : J -> R) : set_bij P Q h ->
\big[op/idx]_( \in Q) F j = \big[op/idx]_( \in P) F (h i).

Proof.

elim/choicePpointed: I => I in h P *.
  rewrite !emptyE => /Pbij[{}h ->].
  by rewrite -[in LHS](image_eq h) image_set0 !fsbig_set0.
elim/choicePpointed: J => J in F h Q *; first by have := no (h point).
move=> /(@pPbij _ _ _)[{}h ->].
pose A := P `&` (F \o h) @^-1` [set~ idx].
pose B := Q `&` F @^-1` [set~ idx].
have /(@pPbij _ _ _)[g gh] : set_bij A B h.
  apply: splitbij_sub; rewrite /A /B /preimage //=.
    by move=> x [Px Fhx]; split=> //; apply: funS.
  by move=> x [Qx Fx]; split; rewrite ?invK ?inE//; apply: funS.
case: finite_supportP; rewrite ?big_nil//=.
  case: finite_supportP; rewrite ?big_nil//=.
  move=> X XP _ XE []; rewrite -/B -(image_eq g) /A.
  by apply: finite_image; rewrite -XE.
move=> Y YQ Fidx YE; case: finite_supportP.
  move=> []; rewrite -/A -(image_eq [bij of g^-1%FUN]).
  by apply: finite_image; rewrite /B -YE.
move=> X XP Fhidx XE; suff -> : Y = (h @` X)%fset.
  by rewrite big_imfset// => ? ? ? ? /inj; apply; rewrite inE; apply: XP.
have BY j : (B j) = (j \in Y) by rewrite -[RHS]/([set` Y] j) YE.
have AX i : (A i) = (i \in X) by rewrite -[RHS]/([set` X] i) XE.
rewrite gh; apply/fsetP=> j; apply/idP/imfsetP => [Yj | [i iX ->]]; last first.
  by rewrite -BY; apply: funS; rewrite AX.
by exists (g^-1%FUN j); rewrite ?invK ?inE ?BY// -AX; apply: funS; rewrite BY.
Qed.

Lemma { : choiceType} ( : I -> J) ( : J -> R) : set_inj P h ->
\big[op/idx]_( \in h @` P) F j = \big[op/idx]_( \in P) F (h i).

Proof.

by move=> /inj_bij; apply: reindex_fsbig. Qed.

Lemma { : choiceType} ( : I -> J) ( : J -> R) :
bijective h -> P `<=` h @` Q -> Q `<=` h @^-1` P ->
\big[op/idx]_( \in P) F j = \big[op/idx]_( \in Q) F (h i).

Proof.

move=> hbij PQ QP; apply: reindex_fsbig; split=> //.
by move=> x y _ _ /(bij_inj hbij).
Qed.

Lemma { : choiceType} ( : I -> J) ( : J -> R) :
bijective h ->
\big[op/idx]_( \in [set: J]) F j = \big[op/idx]_( \in [set: I]) F (h i).

Proof.

by rewrite -setTT_bijective => -[? ? ?]; apply: reindex_fsbig. Qed.

End fsbig2.
Arguments reindex_fsbig {R idx op I J} _ _ _.
Arguments fsbig_image {R idx op I J} _ _.
Arguments __deprecated__reindex_inside {R idx op I J} _ _.
Arguments reindex_fsbigT {R idx op I J} _ _.
#[deprecated(note="use reindex_fsbig, fsbig_image or reindex_fsbigT instead")]
Notation := __deprecated__reindex_inside (only parsing).
#[deprecated(note="use reindex_fsbigT instead")]
Notation := reindex_fsbigT (only parsing).

Lemma ( : eqType) ( : R) ( : Monoid.com_law idx)
( : choiceType) ( : set T2) ( : T1 -> T2 -> R) ( : T1) :
\big[op/idx]_( \in Q) f x y != idx -> exists2 , Q y & f x y != idx.

Proof.

apply: contra_neqP => /forall2NP Qf; apply/fsbig1 => y Qy.
by case: (Qf y) => // /negP/negPn/eqP->.
Qed.

Lemma ( : choiceType) ( : eqType) ( : R)
    ( : Monoid.com_law idx) ( : set T) ( : T -> R) : finite_set P ->
  \big[op/idx]_( \in P) op (f x) (g x) =
  op (\big[op/idx]_( \in P) f x) (\big[op/idx]_( \in P) g x).

Proof.

by move=> Pfin; rewrite !fsbig_finite// big_split. Qed.

Lemma ( : numDomainType) ( : choiceType) ( : set I) ( : I -> R) :
(forall , P i -> 0 <= F i) -> 0 <= \sum_( \in P) F i.

Proof.

move=> PF; case: finite_supportP; rewrite ?big_nil// => X XP F0 _.
by rewrite big_seq_cond big_mkcondr sumr_ge0// => i /XP/PF.
Qed.

Lemma ( : numDomainType) ( : choiceType) ( : set I) ( : I -> R) :
(forall , P i -> F i <= 0) -> \sum_( \in P) F i <= 0.

Proof.

move=> PF; case: finite_supportP; rewrite ?big_nil// => X XP F0 _.
by rewrite big_seq_cond big_mkcondr sumr_le0// => i /XP/PF.
Qed.

Lemma ( : realDomainType) ( : choiceType) ( : seq I) ( : set I)
( : I -> R) :
0 < \sum_( \in P) F i -> exists2 , P i & 0 < F i.

Proof.

apply: contraPP => /forall2NP xNPF; rewrite le_gtF// fsumr_le0// => i Pi.
by case: (xNPF i) => // /negP; case: ltP.
Qed.

Lemma ( : realDomainType) ( : choiceType) ( : set I)
( : I -> R) :
\sum_( \in P) F i < 0 -> exists2 , P i & F i < 0.

Proof.

apply: contraPP => /forall2NP xNPF; rewrite le_gtF// fsumr_ge0// => i Pi.
by case: (xNPF i) => // /negP; case: ltP.
Qed.

Lemma ( : realDomainType) ( : choiceType) ( : set I)
    ( : I -> R) :
  finite_set P ->
  (forall , P i -> 0 <= F i) ->
  \sum_( \in P) F i = 0 -> forall , P i -> F i = 0.

Proof.

move=> Pfin F0 /eqP; apply: contraTP => /existsPNP[i Pi /eqP Fi0].
rewrite (fsbigD1 i)//= paddr_eq0 ?F0 ?negb_and ?Fi0//.
by rewrite fsumr_ge0// => j [/F0->].
Qed.

Lemma {} { : choiceType} ( : set I) ( : I -> set T) :
finite_set A ->
\big[setU/set0]_( \in A) F i = \bigcup_( in A) F i.

Proof.

by move=> Afin; rewrite fsbig_finite// bigsetU_fset_set. Qed.

Lemma { : choiceType} ( : set T) :
finite_set A -> \big[setU/set0]_( \in A) [set x] = A.

Proof.

move=> fA; rewrite fsbig_setU//.
by apply/seteqP; split=> [t [x Ax ->]//|t At]; exists t.
Qed.

Lemma ( : Type) ( : R) ( : Monoid.com_law idx)
    ( : choiceType) ( : set I) ( : set J) ( : I -> J -> R) :
  finite_set P -> finite_set Q ->
  \big[op/idx]_( \in P) \big[op/idx]_( \in Q) F i j
  = \big[op/idx]_( \in P `*` Q) F p.1 p.2.

Proof.

move=> Pfin Qfin; have PQfin : finite_set (P `*` Q) by exact: finite_setX.
rewrite !fsbig_finite//=; under eq_bigr do rewrite fsbig_finite//=.
rewrite pair_big_dep_cond/= fset_setX//.
apply: eq_fbigl => -[i j] //=; apply/imfset2P/idP; rewrite inE //=.
by move=> [x + [y + [-> ->]]]; rewrite 4!inE/= !andbT/= => -> ->.
move=> /andP[Pi Qi]; exists i; rewrite 2?inE ?andbT//.
by exists j; rewrite 2?inE ?andbT.
Qed.

Proof.

move=> Pfin Qfin; rewrite 2?pair_fsbig//; pose swap ( : I * J) := (x.2, x.1).
apply/esym/(reindex_fsbig swap).
split=> [? [? ?]//|[? ?] [? ?] /set_mem[? ?] /set_mem[? ?] [-> ->]//|].
by move=> [i j] [? ?]; exists (j, i).
Qed.

Files

Module mathcomp.classical.fsbigop