Library mathcomp.classical.fsbigop

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
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.

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.
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.
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].

Lemma finite_support_uniq (T : Type) (J : choiceType) (i : T) (P : set J)
    (F : J → T) : uniq (finite_support i P F).
#[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 = [::].

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.

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
   & (∀ 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).

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.

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).
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) :
    (∀ i, i \notin A → f i = idx) →
  \big[op/idx]_(i \in [set: T]) f i = \big[op/idx]_(i <- A) f i.
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.

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.

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.

Lemma bigfs (R : Type) (idx : R) (op : Monoid.com_law idx) (T : choiceType)
    (r : seq T) (P : {pred T}) (f : T → R) : uniq r →
    (∀ 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.

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 →
    (∀ 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.
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.

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

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.

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.
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.

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.
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.

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.

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).
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).
Arguments fsbigID {R idx op I} B.

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

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).
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).

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).
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]) (*NB: not needed in the integral case*)→
  times a (\big[plus/zero]_(i \in P) F i) =
  \big[plus/zero]_(i \in P) times a (F i).

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 (*NB: not needed in the integral case*) →
  times a (\big[plus/zero]_(i \in P) F i) =
  \big[plus/zero]_(i \in P) times a (F i).

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.

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).

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.

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.

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).

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).

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).

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).

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

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.

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).

Lemma fsumr_ge0 (R : numDomainType) (I : choiceType) (P : set I) (F : I → R) :
  (∀ i, P i → 0 ≤ F i) → 0 ≤ \sum_(i \in P) F i.

Lemma fsumr_le0 (R : numDomainType) (I : choiceType) (P : set I) (F : I → R) :
  (∀ i, P i → F i ≤ 0) → \sum_(i \in P) F i ≤ 0.

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.

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.

Lemma pfsumr_eq0 (R : realDomainType) (I : choiceType) (P : set I)
    (F : I → R) :
  finite_set P →
  (∀ i, P i → 0 ≤ F i) →
  \sum_(i \in P) F i = 0 → ∀ i, P i → F i = 0.

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.

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

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.

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.