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.