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 signed topology.
Require Import sequences functions cardinality normedtype numfun fsbigop.

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 : {fset T} | [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 esum_set1 t a : 0 ≤ a t → \esum_(i in [set t]) a i = a t.

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.

Lemma fsbig_esum (A : set T) a : finite_set A → (∀ x, 0 ≤ a x) →
  \sum_(x \in A) (a x) = \esum_(x in A) a x.
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 nneseries_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 →
  \esum_(j in Q) a j = \esum_(i in P) a (e i).
Arguments reindex_esum {R T T'} P Q e a.

Section nneseries_interchange.
Local Open Scope ereal_scope.

Let nneseries_esum_prod (R : realType) (a : nat → nat → \bar R)
  (P Q : pred nat) : (∀ i j, 0 ≤ a i j) →
  \sum_(i <oo | P i) \sum_(j <oo | Q j) a i j =
  \esum_(i in P `*` Q) a i.1 i.2.

Lemma nneseries_interchange (R : realType) (a : nat → nat → \bar R)
  (P Q : pred nat) : (∀ i j, 0 ≤ a i j) →
  \sum_(i <oo | P i) \sum_(j <oo | Q j) a i j =
  \sum_(j <oo | Q j) \sum_(i <oo | P i) a i j.

End nneseries_interchange.

Lemma esum_image (R : realType) (T T' : choiceType)
    (P : set T) (e : T → T') (a : T' → \bar R) :
    set_inj P e →
  \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.

Definition summable (T : choiceType) (R : realType) (D : set T)
  (f : T → \bar R) := (\esum_(x in D) `| f x | < +oo)%E.

Section summable_lemmas.
Local Open Scope ereal_scope.
Variables (T : choiceType) (R : realType).
Implicit Types (D : set T) (f : T → \bar R).

Lemma summable_pinfty D f : summable D f → ∀ x, D x → `| f x | < +oo.

Lemma summableE D f : summable D f = (\esum_(x in D) `| f x | \is a fin_num).

Lemma summableD D f g : summable D f → summable D g → summable D (f \+ g).

Lemma summableN D f : summable D f = summable D (\- f).

Lemma summableB D f g : summable D f → summable D g → summable D (f \- g).

Lemma summable_funepos D f : summable D f → summable D f^\+.

Lemma summable_funeneg D f : summable D f → summable D f^\-.

End summable_lemmas.

Import numFieldNormedType.Exports.

Section summable_nat.
Local Open Scope ereal_scope.
Variable R : realType.

Lemma summable_fine_sum r (P : pred nat) (f : nat → \bar R) : summable P f →
  (\sum_(0 ≤ k < r | P k) fine (f k))%R = fine (\sum_(0 ≤ k < r | P k) f k).

Lemma summable_cvg (P : pred nat) (f : (\bar R)^nat) :
  (∀ i, P i → 0 ≤ f i)%E → summable P f →
  cvg (fun n ⇒ \sum_(0 ≤ k < n | P k) fine (f k))%R.

Lemma summable_nneseries_lim (P : pred nat) (f : (\bar R)^nat) :
    (∀ i, P i → 0 ≤ f i)%E → summable P f →
  \sum_(i <oo | P i) f i =
  (lim (fun n ⇒ (\sum_(0 ≤ k < n | P k) fine (f k))%R))%:E.

Lemma summable_nneseries (f : nat → \bar R) (P : pred nat) : summable P f →
  \sum_(i <oo | P i) (f i) =
  \sum_(i <oo | P i) f^\+ i - \sum_(i <oo | P i) f^\- i.

Lemma summable_nneseries_esum (f : nat → \bar R) (P : pred nat) :
  summable P f → \sum_(i <oo | P i) f i = esum P f^\+ - esum P f^\-.

End summable_nat.

Section esumB.
Local Open Scope ereal_scope.
Variables (R : realType) (T : choiceType).
Implicit Types (D : set T) (f g : T → \bar R).

Let esum_posneg D f := esum D f^\+ - esum D f^\-.

Let ge0_esum_posneg D f : (∀ x, D x → 0 ≤ f x) →
  esum_posneg D f = \esum_(x in D) f x.

Lemma esumB D f g : summable D f → summable D g →
  (∀ i, D i → 0 ≤ f i) → (∀ i, D i → 0 ≤ g i) →
  \esum_(i in D) (f \- g)^\+ i - \esum_(i in D) (f \- g)^\- i =
  \esum_(i in D) f i - \esum_(i in D) g i.

End esumB.