From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import 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"
  (at level 36, F at level 36, op, idx at level 10, i, A at level 50,
           format "'[' \big [ op / idx ]_ ( i '\in' A ) '/ ' F ']'").

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

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 ]_ ( i '\in' A ) F" :=
  (\big[op/idx]_(i <- fset_set (A `&` ((fun i => F) @^-1` [set~ idx]))) F)
    (only parsing) : big_scope.

Lemma finite_index_key : unit

Proof.

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

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

Proof.

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

Proof.

#[global] Hint Resolve finite_support_uniq : core.

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

Proof.

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

Proof.

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

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

Proof.

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

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

Proof.

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

Proof.

Arguments eq_fsbigr {R idx op T f} g.

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

Proof.

Arguments fsbigTE {R idx op T} A f.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

Arguments fsbigE {R idx op T A}.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

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

Proof.

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

Proof.

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

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

Proof.

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

Proof.

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

Proof.

Arguments __deprecated__full_fsbigID {R idx op I} B.

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

Proof.

Arguments fsbigID {R idx op I} B.

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

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

Proof.

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

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

Proof.

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

Proof.

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

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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 reindex_inside := __deprecated__reindex_inside (only parsing).
#[deprecated(note="use reindex_fsbigT instead")]
Notation reindex_inside_setT := reindex_fsbigT (only parsing).

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

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

Proof.

Module mathcomp.classical.fsbigop

Finitely-supported big operators