Library mathcomp.analysis.esum
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import reals ereal signed topology sequences normedtype numfun.
From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import reals ereal signed topology sequences normedtype numfun.
Summation over classical sets
This file provides a definition of sum over classical sets and a few
lemmas in particular for the case of sums of non-negative terms.
fsets S == the set of finite sets (fset) included in S
\esum_(i in I) f i == summation of non-negative extended real numbers over
classical sets; I is a classical set and f is a
function whose codomain is included in the extended
reals; it is 0 if I = set0 and sup(\sum_A a) where A
is a finite set included in I o.w.
summable D f := \esum_(x in D) `| f x | < +oo
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 (set T) := [set F | finite_set F ∧ F `<=` S].
Lemma fsets_set0 S : fsets S set0.
Lemma fsets_self (F : set T) : finite_set F → fsets F F.
Lemma fsets0 : fsets set0 = [set set0].
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 \in 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 : set T) a : finite_set F →
(∀ i, i \in F → 0 ≤ a i) →
\esum_(i in F) a i = \sum_(i \in F) a i.
Lemma esum_set1 t a : 0 ≤ a t → \esum_(i in [set t]) a i = a t.
End esum_realType.
Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T → \bar R) x :
(exists2 X : set T, fsets I X & x ≤ \sum_(i \in X) a i) →
x ≤ \esum_(i in I) a i.
Lemma esum1 [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, I i → J 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_eseries (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_eseries_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.