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.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
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
Proof.
by split. Qed.
Lemma fsets_self (
F : set T)
: finite_set F -> fsets F F.
Proof.
by move=> finF; split. Qed.
Lemma fsets0 : fsets set0 = [set set0].
Proof.
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].
Local Notation "\esum_ ( i 'in' P ) A" := (
esum P (
fun i => A)).
Lemma esum_set0 a : \esum_(
i in set0)
a i = 0.
Proof.
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 :
(
forall x, S x -> 0 <= a x)
-> 0 <= \esum_(
i in S)
a i.
Proof.
Lemma esum_fset (
F : set T)
a : finite_set F ->
(
forall i, i \in F -> 0 <= a i)
->
\esum_(
i in F)
a i = \sum_(
i \in F)
a i.
Proof.
move=> finF f0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
by apply ereal_sup_ub; exists F => //; exact: fsets_self.
apply ub_ereal_sup => /= ? -[F' [finF' F'F] <-].
apply/lee_fsum_nneg_subset => //; first exact/subsetP.
by move=> t; rewrite inE/= => /andP[_] /f0.
Qed.
Lemma esum_set1 t a : 0 <= a t -> \esum_(
i in [set t])
a i = a t.
Proof.
by move=> ?; rewrite esum_fset// ?fset_set1// ?fsbig_set1// => t' /[!inE] ->.
Qed.
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.
Proof.
by move=> [X IX /le_trans->//]; apply: ereal_sup_ub => /=; exists X. Qed.
Lemma esum1 [R : realFieldType] [I : choiceType] (
D : set I) (
a : I -> \bar R)
:
(
forall i, D i -> a i = 0)
-> \esum_(
i in D)
a i = 0.
Proof.
move=> a0; rewrite /esum (
_ : [set _ | _ in _] = [set 0])
?ereal_sup1//.
apply/seteqP; split=> x //= => [[X [finX XI]] <-|->].
by rewrite fsbig1// => i /XI/a0.
by exists set0; rewrite ?fsbig_set0//; exact: fsets_set0.
Qed.
Lemma le_esum [R : realType] [T : choiceType] (
I : set T) (
a b : T -> \bar R)
:
(
forall i, I i -> a i <= b i)
->
\esum_(
i in I)
a i <= \esum_(
i in I)
b i.
Proof.
Lemma eq_esum [R : realType] [T : choiceType] (
I : set T) (
a b : T -> \bar R)
:
(
forall i, I i -> a i = b i)
->
\esum_(
i in I)
a i = \esum_(
i in I)
b i.
Proof.
by move=> e; apply/eqP; rewrite eq_le !le_esum// => i Ii; rewrite e. Qed.
Lemma esumD [R : realType] [T : choiceType] (
I : set T) (
a b : T -> \bar R)
:
(
forall i, I i -> 0 <= a i)
-> (
forall 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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Lemma esumID (
R : realType) (
I : choiceType) (
B : set I) (
A : set I)
(
F : I -> \bar R)
:
(
forall 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).
Proof.
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)
:
(
forall 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.
Proof.
Lemma esum_esum [R : realType] [T1 T2 : choiceType]
(
I : set T1) (
J : T1 -> set T2) (
a : T1 -> T2 -> \bar R)
:
(
forall 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.
Proof.
Lemma lee_sum_fset_nat (
R : realDomainType)
(
f : (
\bar R)
^nat) (
F : {fset nat})
n (
P : pred nat)
:
(
forall 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.
Proof.
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)
:
(
forall i, P i -> 0%E <= f i)
->
\sum_(
i <- F | P i)
f i <= \sum_(
i <oo | P i)
f i.
Proof.
Arguments lee_sum_fset_lim {R f} F P.
Lemma nneseries_esum (
R : realType) (
a : nat -> \bar R) (
P : pred nat)
:
(
forall n, P n -> 0 <= a n)
->
\sum_(
i <oo | P i)
a i = \esum_(
i in [set x | P x])
a i.
Proof.
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).
Proof.
elim/choicePpointed: T => T in e P *.
rewrite !emptyE => /Pbij[{}e ->].
by rewrite -[in LHS](
image_eq e)
image_set0 !esum_set0.
elim/choicePpointed: T' => T' in a e Q *; first by have := no (
e point).
move=> /(
@pPbij _ _ _)
[{}e ->].
gen have le_esum : T T' a P Q e /
\esum_(
j in Q)
a j <= \esum_(
i in P)
a (
e i)
; last first.
apply/eqP; rewrite eq_le le_esum//=.
rewrite [leRHS](
_ : _ = \esum_(
j in Q)
a (
e (
e^-1%FUN j)))
; last first.
by apply: eq_esum => i Qi; rewrite invK ?inE.
by rewrite le_esum => //= i Qi; rewrite a_ge0//; exact: funS.
rewrite ub_ereal_sup => //= _ [X [finX XQ] <-]; rewrite ereal_sup_ub => //=.
exists [set` (
e^-1 @` (
fset_set X))
%fset].
split=> [|t /= /imfsetP[t'/=]]; first exact: finite_fset.
by rewrite in_fset_set// inE => /XQ Qt' ->; exact: funS.
rewrite fsbig_finite//= set_fsetK big_imfset => //=; last first.
move=> x y; rewrite !in_fset_set// !inE => /XQ ? /XQ ? /(
congr1 e).
by rewrite !invK ?inE.
by rewrite -fsbig_finite//; apply: eq_fsbigr=> x /[!inE]/XQ ?; rewrite invK ?inE.
Qed.
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)
: (
forall 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.
Proof.
Lemma nneseries_interchange (
R : realType) (
a : nat -> nat -> \bar R)
(
P Q : pred nat)
: (
forall 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.
Proof.
move=> a0; rewrite !nneseries_esum_prod//.
rewrite (
reindex_esum (
Q `*` P)
_ (
fun x => (
x.
2, x.
1)))
//; split=> //=.
by move=> [i j] [/=].
by move=> [i1 i2] [j1 j2] /= _ _ [] -> ->.
by move=> [i1 i2] [Pi1 Qi2] /=; exists (
i2, i1).
Qed.
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).
Proof.
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)
:
(
forall 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).
Proof.
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] :
(
forall 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).
Proof.
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 -> (
forall 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.
Proof.
move=> tJ a0; rewrite esum_esum//; apply: reindex_esum => //; split.
- by move=> [/= i j] [Ki Jij]; exists i.
- move=> [/= i1 j1] [/= i2 j2]; rewrite ?inE/=.
move=> [K1 J1] [K2 J2] j12; congr (
_, _)
=> //.
by apply: (
@tJ i1 i2)
=> //; exists j1; split=> //; rewrite j12.
- by move=> j [i Ki Jij]/=; exists (
i, j).
Qed.
Lemma esum_bigcup J a : trivIset [set i | a @` J i != [set 0]] J ->
(
forall 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.
Proof.
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 -> forall x, D x -> `| f x | < +oo.
Proof.
Lemma summableE D f : summable D f = (
\esum_(
x in D)
`| f x | \is a fin_num).
Proof.
Lemma summableD D f g : summable D f -> summable D g -> summable D (
f \+ g).
Proof.
Lemma summableN D f : summable D f = summable D (
\- f).
Proof.
by rewrite /summable; congr (
_ < +oo)
; apply: eq_esum => t Dt; rewrite abseN.
Qed.
Lemma summableB D f g : summable D f -> summable D g -> summable D (
f \- g).
Proof.
Lemma summable_funepos D f : summable D f -> summable D f^\+.
Proof.
Lemma summable_funeneg D f : summable D f -> summable D f^\-.
Proof.
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).
Proof.
Lemma summable_cvg (
P : pred nat) (
f : (
\bar R)
^nat)
:
(
forall i, P i -> 0 <= f i)
%E -> summable P f ->
cvg (
fun n => \sum_(
0 <= k < n | P k)
fine (
f k))
%R.
Proof.
Lemma summable_nneseries_lim (
P : pred nat) (
f : (
\bar R)
^nat)
:
(
forall 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.
Proof.
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.
Proof.
move=> Pf.
pose A_ n := (
\sum_(
0 <= k < n | P k)
fine (
f^\+ k))
%R.
pose B_ n := (
\sum_(
0 <= k < n | P k)
fine (
f^\- k))
%R.
pose C_ n := fine (
\sum_(
0 <= k < n | P k)
f k).
pose A := lim A_.
pose B := lim B_.
suff: ((
fun n => C_ n - (
A - B))
--> (
0 : R^o))
%R.
move=> CAB.
rewrite [X in X - _]summable_nneseries_lim//; last exact/summable_funepos.
rewrite [X in _ - X]summable_nneseries_lim//; last exact/summable_funeneg.
rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split; last first.
apply: (
@cvg_sub0 _ _ _ _ _ _ (
cst (
A - B)
%R)
_ CAB)
; exact: cvg_cst.
apply: nearW => n; rewrite fin_num_abs; apply: le_lt_trans Pf => /=.
by rewrite -nneseries_esum ?(
le_trans (
lee_abs_sum _ _ _))
?nneseries_lim_ge.
have : ((
fun x => A_ x - B_ x)
--> A - B)
%R.
apply: cvgD.
- by apply: summable_cvg => //; exact/summable_funepos.
- by apply: cvgN; apply: summable_cvg => //; exact/summable_funeneg.
move=> /cvgrPdist_lt cvgAB; apply/cvgrPdist_lt => e e0.
move: cvgAB => /(
_ _ e0)
[N _/= hN] /=.
near=> n.
rewrite distrC subr0.
have -> : (
C_ = A_ \- B_)
%R.
apply/funext => k.
rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//.
apply eq_bigr => i Pi; rewrite -fineB//.
- by rewrite [in LHS](
funeposneg f).
- by rewrite fin_num_abs (
@summable_pinfty _ _ P)
//; exact/summable_funepos.
- by rewrite fin_num_abs (
@summable_pinfty _ _ P)
//; exact/summable_funeneg.
by rewrite distrC; apply: hN; near: n; exists N.
Unshelve.
all: by end_near. Qed.
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^\-.
Proof.
move=> Pfoo; rewrite -nneseries_esum; last first.
by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite -leNgt.
rewrite -nneseries_esum ?[LHS]summable_eseries//.
by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite leNgt.
Qed.
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 : (
forall x, D x -> 0 <= f x)
->
esum_posneg D f = \esum_(
x in D)
f x.
Proof.
move=> Sa; rewrite /esum_posneg [X in _ - X](
_ : _ = 0)
?sube0; last first.
by rewrite esum1// => x Sx; rewrite -[LHS]/(
f^\- x) (
ge0_funenegE Sa)
// inE.
by apply: eq_esum => t St; apply/max_idPl; exact: Sa.
Qed.
Lemma esumB D f g : summable D f -> summable D g ->
(
forall i, D i -> 0 <= f i)
-> (
forall 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.
Proof.
End esumB.