Library mathcomp.analysis.csum
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat eqtype choice seq fintype order bigop.
From mathcomp Require Import ssralg ssrnum.
From mathcomp Require Import finmap.
Require Import boolp reals ereal classical_sets posnum topology.
Require Import sequences cardinality.
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat eqtype choice seq fintype order bigop.
From mathcomp Require Import ssralg ssrnum.
From mathcomp Require Import finmap.
Require Import boolp reals ereal classical_sets posnum topology.
Require Import sequences cardinality.
Summations 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.
The contents of this file should not be considered as definitive because
it supports on-going developments (such as the Lebesgue measure) and we
anticipate revisions.
\csum(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_F a) where F is a finite set included in I o.w.
Reserved Notation "\csum_ ( i 'in' P ) F"
(at level 41, F at level 41, format "\csum_ ( 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 x | x \in 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 x | x \in F] `<=` S ↔ fsets S F.
Lemma fsets0 : fsets set0 = [set fset0].
End set_of_fset_in_a_set.
Lemma fsets_img (aT rT : choiceType) (S : set aT) (F : {fset aT}) (e : aT → rT) :
fsets S F → fsets (e @` S) (e @` F)%fset.
Definition fsets_ord (P : pred nat) n := [fset i in 'I_n | P i]%fset.
Lemma fsets_ord_nat (P : pred nat) n :
fsets P (@nat_of_ord _ @` fsets_ord P n)%fset.
Lemma fsets_ord_subset (T : pointedType) (F : {fset T})
(e : nat → T) (P : pred nat) : injective e →
[set x | x \in F] `<=` e @` P →
∃ n, (F `<=` e @` (@nat_of_ord _ @` fsets_ord P n))%fset.
Section csum.
Variables (R : realFieldType) (T : choiceType).
Implicit Types (S : set T) (a : T → \bar R).
Definition csum S a :=
ereal_sup [set \sum_(i <- F) a i | F in fsets S].
Lemma csum0 a : \csum_(i in set0) a i = 0.
End csum.
Notation "\csum_ ( i 'in' P ) F" := (csum P (fun i ⇒ F)) : ring_scope.
Section csum_realType.
Variables (R : realType) (T : choiceType).
Implicit Types (a : T → \bar R).
Lemma csum_ge0 (S : set T) a : (∀ x, 0 ≤ a x) → 0 ≤ \csum_(i in S) a i.
Lemma csum_fset (F : {fset T}) a : (∀ i, i \in F → 0 ≤ a i) →
\csum_(i in [set x | x \in F]) a i = \sum_(i <- F) a i.
End csum_realType.
Lemma csum_image (R : realType) (T : pointedType) (a : T → \bar R)
(e : nat → T) (P : pred nat) : (∀ n, P n → 0 ≤ a (e n)) →
injective e →
\csum_(i in e @` P) a i = \sum_(i <oo | P i) a (e i).
Lemma ereal_pseries_csum (R : realType) (a : nat → \bar R) (P : pred nat) :
(∀ n, P n → 0 ≤ a n) →
\sum_(i <oo | P i) a i = \csum_(i in [set x | P x]) a i.
Section csum_bigcup.
Variables (R : realType) (T : pointedType) (K : set nat) (J : nat → set T).
Hypotheses (tJ : trivIset setT J).
Let KJ := \bigcup_(k in K) (J k).
Variable a : T → \bar R.
Hypothesis a0 : ∀ x, 0 ≤ a x.
Let tJ' : ∀ i j : nat, i != j → J i `&` J j = set0.
Lemma csum_bigcup : \csum_(i in \bigcup_(k in K) (J k)) a i =
\csum_(i in K) \csum_(j in J i) a j.
End csum_bigcup.