Library mathcomp.analysis.fsbigop

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
Require Import mathcomp_extra boolp classical_sets signed functions cardinality.
Require Import reals ereal topology normedtype.

Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope classical_set_scope.
Local Open Scope 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 ']'").
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).

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 ']'").
Notation "\sum_ ( i '\in' A ) F" := (\big[+%R/0%R]_(i \in A) F) : ring_scope.
Notation "\sum_ ( i '\in' A ) F" := (\big[+%E/0%E]_(i \in A) F) : ereal_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).

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.

#[deprecated(note="Use fsbigID instead")]
Lemma 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 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.

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

#[deprecated(note="use reindex_fsbig, fsbig_image or reindex_fsbigT instead")]
Lemma 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 reindex_inside {R idx op I J} _ _.
Arguments reindex_fsbigT {R idx op I J} _ _.
#[deprecated(note="use reindex_fsbigT instead")]
Notation reindex_inside_setT := reindex_fsbigT.

Lemma ge0_mule_fsumr (T : choiceType) (R : realDomainType) (x : \bar R)
    (F : T → \bar R) (P : set T) : (∀ i : T, 0 ≤ F i)%E →
  (x × (\sum_(i \in P) F i) = \sum_(i \in P) x × F i)%E.

Lemma ge0_mule_fsuml (T : choiceType) (R : realDomainType) (x : \bar R)
    (F : T → \bar R) (P : set T) : (∀ i : T, 0 ≤ F i)%E →
  ((\sum_(i \in P) F i) × x = \sum_(i \in P) F i × x)%E.

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 fsume_ge0 (R : numDomainType) (I : choiceType) (P : set I)
    (F : I → \bar R) :
  (∀ i, P i → (0 ≤ F i)%E) → (0 ≤ \sum_(i \in P) F i)%E.

Lemma fsume_le0 (R : numDomainType) (T : choiceType) (f : T → \bar R) (P : set T) :
  (∀ t, P t → (f t ≤ 0)%E) → (\sum_(i \in P) f i ≤ 0)%E.

Lemma fsume_gt0 (R : realDomainType) (I : choiceType) (P : set I)
    (F : I → \bar R) :
  (0 < \sum_(i \in P) F i)%E → exists2 i, P i & (0 < F i)%E.

Lemma fsume_lt0 (R : realDomainType) (I : choiceType) (P : set I)
    (F : I → \bar R) :
  (\sum_(i \in P) F i < 0)%E → exists2 i, P i & (F i < 0)%E.

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

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 pair_fsum (T1 T2 : choiceType) (R : realDomainType)
    (f : T1 → T2 → \bar R) (P : set T1) (Q : set T2) :
    finite_set P → finite_set Q →
  (\sum_(x \in P) \sum_(y \in Q) f x y = \sum_(x \in P `*` Q) f x.1 x.2)%E.

Lemma exchange_fsum (T : choiceType) (R : realDomainType) (P Q : set T)
     (f : T → T → \bar R) :
    finite_set P → finite_set Q →
  (\sum_(i \in P) \sum_(j \in Q) f i j = \sum_(j \in Q) \sum_(i \in P) f i j)%E.