Library mathcomp.analysis.esum

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

Reserved Notation "\esum_ ( i 'in' P ) F"
  (at level 41, F at level 41, format "\esum_ ( i 'in' P ) F").

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Local Open Scope ereal_scope.

Section set_of_fset_in_a_set.
Variable (T : choiceType).
Implicit Type S : set T.

Definition fsets S : set {fset T} := [set F | [set` F] `<=` S].

Lemma fsets_set0 S : fsets S fset0.

Lemma fsets_self (F : {fset T}) : fsets [set x | x \in F] F.

Lemma fsetsP S (F : {fset T}) : [set` F] `<=` S ↔ fsets S F.

Lemma fsets0 : fsets set0 = [set fset0].

End set_of_fset_in_a_set.

Section esum.
Variables (R : realFieldType) (T : choiceType).
Implicit Types (S : set T) (a : T → \bar R).

Definition esum S a := ereal_sup [set \sum_(x <- A) a x | A in fsets S].


Lemma esum_set0 a : \esum_(i in set0) a i = 0.

End esum.

Notation "\esum_ ( i 'in' P ) F" := (esum P (fun i ⇒ F)) : ring_scope.

Section esum_realType.
Variables (R : realType) (T : choiceType).
Implicit Types (a : T → \bar R).

Lemma esum_ge0 (S : set T) a : (∀ x, S x → 0 ≤ a x) → 0 ≤ \esum_(i in S) a i.

Lemma esum_fset (F : {fset T}) a : (∀ i, i \in F → 0 ≤ a i) →
  \esum_(i in [set` F]) a i = \sum_(i <- F) a i.

Lemma sum_fset_set (A : set T) a : finite_set A →
  (∀ i, A i → 0 ≤ a i) →
  \sum_(i <- fset_set A) a i = \esum_(i in A) a i.

End esum_realType.

Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T → \bar R) x :
  (exists2 X : {fset T}, fsets I X & x ≤ \sum_(i <- X) a i) →
  x ≤ \esum_(i in I) a i.

Lemma esum0 [R : realFieldType] [I : choiceType] (D : set I) (a : I → \bar R) :
  (∀ i, D i → a i = 0) → \esum_(i in D) a i = 0.

Lemma le_esum [R : realType] [T : choiceType] (I : set T) (a b : T → \bar R) :
  (∀ i, I i → a i ≤ b i) →
  \esum_(i in I) a i ≤ \esum_(i in I) b i.

Lemma eq_esum [R : realType] [T : choiceType] (I : set T) (a b : T → \bar R) :
  (∀ i, I i → a i = b i) →
  \esum_(i in I) a i = \esum_(i in I) b i.

Lemma esumD [R : realType] [T : choiceType] (I : set T) (a b : T → \bar R) :
  (∀ i, I i → 0 ≤ a i) → (∀ i, I i → 0 ≤ b i) →
  \esum_(i in I) (a i + b i) = \esum_(i in I) a i + \esum_(i in I) b i.

Lemma esum_mkcond [R : realType] [T : choiceType] (I : set T) (a : T → \bar R) :
  \esum_(i in I) a i = \esum_(i in [set: T]) if i \in I then a i else 0.

Lemma esum_mkcondr [R : realType] [T : choiceType] (I J : set T) (a : T → \bar R) :
  \esum_(i in I `&` J) a i = \esum_(i in I) if i \in J then a i else 0.

Lemma esum_mkcondl [R : realType] [T : choiceType] (I J : set T) (a : T → \bar R) :
  \esum_(i in I `&` J) a i = \esum_(i in J) if i \in I then a i else 0.

Lemma esumID (R : realType) (I : choiceType) (B : set I) (A : set I)
  (F : I → \bar R) :
  (∀ i, A i → F i ≥ 0) →
  \esum_(i in A) F i = (\esum_(i in A `&` B) F i) +
                        (\esum_(i in A `&` ~` B) F i).
Arguments esumID {R I}.

Lemma esum_sum [R : realType] [T1 T2 : choiceType]
    (I : set T1) (r : seq T2) (P : pred T2) (a : T1 → T2 → \bar R) :
  (∀ i j, I i → P j → 0 ≤ a i j) →
  \esum_(i in I) \sum_(j <- r | P j) a i j =
  \sum_(j <- r | P j) \esum_(i in I) a i j.

Lemma esum_esum [R : realType] [T1 T2 : choiceType]
    (I : set T1) (J : T1 → set T2) (a : T1 → T2 → \bar R) :
  (∀ i j, 0 ≤ a i j) →
  \esum_(i in I) \esum_(j in J i) a i j = \esum_(k in I `*`` J) a k.1 k.2.

Lemma lee_sum_fset_nat (R : realDomainType)
    (f : (\bar R)^nat) (F : {fset nat}) n (P : pred nat) :
    (∀ i, P i → 0%E ≤ f i) →
    [set` F] `<=` `I_n →
  \sum_(i <- F | P i) f i ≤ \sum_(0 ≤ i < n | P i) f i.
Arguments lee_sum_fset_nat {R f} F n P.

Lemma lee_sum_fset_lim (R : realType) (f : (\bar R)^nat) (F : {fset nat})
    (P : pred nat) :
  (∀ i, P i → 0%E ≤ f i) →
  \sum_(i <- F | P i) f i ≤ \sum_(i <oo | P i) f i.
Arguments lee_sum_fset_lim {R f} F P.

Lemma ereal_pseries_esum (R : realType) (a : nat → \bar R) (P : pred nat) :
  (∀ n, P n → 0 ≤ a n) →
  \sum_(i <oo | P i) a i = \esum_(i in [set x | P x]) a i.

Lemma reindex_esum (R : realType) (T T' : choiceType)
    (P : set T) (Q : set T') (e : T → T') (a : T' → \bar R) :
    set_bij P Q e →
    (∀ i, P i → 0 ≤ a (e i)) →
  \esum_(j in Q) a j = \esum_(i in P) a (e i).
Arguments reindex_esum {R T T'} P Q e a.

Lemma esum_image (R : realType) (T T' : choiceType)
    (P : set T) (e : T → T') (a : T' → \bar R) :
    set_inj P e → (∀ i, P i → 0 ≤ a (e i)) →
  \esum_(j in e @` P) a j = \esum_(i in P) a (e i).
Arguments esum_image {R T T'} P e a.

Lemma esum_pred_image (R : realType) (T : choiceType) (a : T → \bar R)
    (e : nat → T) (P : pred nat) :
    (∀ n, P n → 0 ≤ a (e n)) →
    set_inj P e →
  \esum_(i in e @` P) a i = \sum_(i <oo | P i) a (e i).
Arguments esum_pred_image {R T} a e P.

Lemma esum_set_image [R : realType] [T : choiceType] [a : T → \bar R]
    [e : nat → T] [P : set nat] :
    (∀ n : nat, P n → 0 ≤ a (e n)) →
  set_inj P e →
  \esum_(i in [set e x | x in P]) a i = \sum_(i <oo | i \in P) a (e i).
Arguments esum_set_image {R T} a e P.

Section esum_bigcup.
Variables (R : realType) (T : choiceType) (K : set nat).
Implicit Types (J : nat → set T) (a : T → \bar R).

Lemma esum_bigcupT J a : trivIset setT J → (∀ x, 0 ≤ a x) →
  \esum_(i in \bigcup_(k in K) (J k)) a i =
  \esum_(i in K) \esum_(j in J i) a j.

Lemma esum_bigcup J a : trivIset [set i | a @` J i != [set 0]] J →
    (∀ x : T, (\bigcup_(k in K) J k) x → 0 ≤ a x) →
  \esum_(i in \bigcup_(k in K) J k) a i = \esum_(k in K) \esum_(j in J k) a j.

End esum_bigcup.

Arguments esum_bigcupT {R T K} J a.
Arguments esum_bigcup {R T K} J a.