let f be nonnegative Function of [:NAT,NAT:],ExtREAL; for seq being ExtREAL_sequence st ( for m being Element of NAT holds seq . m = lim_inf (ProjMap2 (f,m)) ) holds
Sum seq <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f))
let seq be ExtREAL_sequence; ( ( for m being Element of NAT holds seq . m = lim_inf (ProjMap2 (f,m)) ) implies Sum seq <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f)) )
assume A1:
for m being Element of NAT holds seq . m = lim_inf (ProjMap2 (f,m))
; Sum seq <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f))
A2:
for m, N, n being Element of NAT st n >= N holds
(inferior_realsequence (ProjMap2 (f,m))) . N <= f . (n,m)
proof
let m be
Element of
NAT ;
for N, n being Element of NAT st n >= N holds
(inferior_realsequence (ProjMap2 (f,m))) . N <= f . (n,m)let N,
n be
Element of
NAT ;
( n >= N implies (inferior_realsequence (ProjMap2 (f,m))) . N <= f . (n,m) )
assume
n >= N
;
(inferior_realsequence (ProjMap2 (f,m))) . N <= f . (n,m)
then A4:
(inferior_realsequence (ProjMap2 (f,m))) . N <= (inferior_realsequence (ProjMap2 (f,m))) . n
by RINFSUP2:7;
(inferior_realsequence (ProjMap2 (f,m))) . n <= (ProjMap2 (f,m)) . n
by RINFSUP2:8;
then
(inferior_realsequence (ProjMap2 (f,m))) . n <= f . (
n,
m)
by MESFUNC9:def 7;
hence
(inferior_realsequence (ProjMap2 (f,m))) . N <= f . (
n,
m)
by A4, XXREAL_0:2;
verum
end;
deffunc H1( Element of NAT ) -> Element of bool [:omega,ExtREAL:] = inferior_realsequence (ProjMap2 (f,$1));
deffunc H2( Element of NAT , Element of NAT ) -> Element of ExtREAL = (inferior_realsequence (ProjMap2 (f,$2))) . $1;
consider g being Function of [:NAT,NAT:],ExtREAL such that
A5:
for n, m being Element of NAT holds g . (n,m) = H2(n,m)
from BINOP_1:sch 4();
then
g is nonnegative
by SUPINF_2:51;
then reconsider g = g as nonnegative V183() Function of [:NAT,NAT:],ExtREAL ;
A6:
for m, N, n being Element of NAT st n >= N holds
(Partial_Sums_in_cod2 g) . (N,m) <= (Partial_Sums_in_cod2 f) . (n,m)
proof
let m be
Element of
NAT ;
for N, n being Element of NAT st n >= N holds
(Partial_Sums_in_cod2 g) . (N,m) <= (Partial_Sums_in_cod2 f) . (n,m)let N,
n be
Element of
NAT ;
( n >= N implies (Partial_Sums_in_cod2 g) . (N,m) <= (Partial_Sums_in_cod2 f) . (n,m) )
assume A7:
n >= N
;
(Partial_Sums_in_cod2 g) . (N,m) <= (Partial_Sums_in_cod2 f) . (n,m)
defpred S1[
Nat]
means (Partial_Sums_in_cod2 g) . (
N,$1)
<= (Partial_Sums_in_cod2 f) . (
n,$1);
A8:
(Partial_Sums_in_cod2 g) . (
N,
0) =
g . (
N,
0)
by DefCSM
.=
(inferior_realsequence (ProjMap2 (f,0))) . N
by A5
;
(Partial_Sums_in_cod2 f) . (
n,
0)
= f . (
n,
0)
by DefCSM;
then A9:
S1[
0 ]
by A2, A7, A8;
A10:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
reconsider k1 =
k as
Element of
NAT by ORDINAL1:def 12;
assume A11:
S1[
k]
;
S1[k + 1]
g . (
N,
(k1 + 1))
= (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . N
by A5;
then A12:
g . (
N,
(k1 + 1))
<= f . (
n,
(k1 + 1))
by A2, A7;
(
(Partial_Sums_in_cod2 g) . (
N,
(k + 1))
= ((Partial_Sums_in_cod2 g) . (N,k)) + (g . (N,(k1 + 1))) &
(Partial_Sums_in_cod2 f) . (
n,
(k + 1))
= ((Partial_Sums_in_cod2 f) . (n,k)) + (f . (n,(k1 + 1))) )
by DefCSM;
hence
S1[
k + 1]
by A11, A12, XXREAL_3:36;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A9, A10);
hence
(Partial_Sums_in_cod2 g) . (
N,
m)
<= (Partial_Sums_in_cod2 f) . (
n,
m)
;
verum
end;
A13:
for m, N, n being Element of NAT st n >= N holds
(Partial_Sums_in_cod2 g) . (N,m) <= (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . n
proof
let m be
Element of
NAT ;
for N, n being Element of NAT st n >= N holds
(Partial_Sums_in_cod2 g) . (N,m) <= (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . nlet N,
n be
Element of
NAT ;
( n >= N implies (Partial_Sums_in_cod2 g) . (N,m) <= (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . n )
assume A14:
n >= N
;
(Partial_Sums_in_cod2 g) . (N,m) <= (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . n
consider Y being non
empty Subset of
ExtREAL such that A15:
(
Y = { ((ProjMap2 ((Partial_Sums_in_cod2 f),m)) . k) where k is Nat : n <= k } &
(inferior_realsequence (ProjMap2 ((Partial_Sums_in_cod2 f),m))) . n = inf Y )
by RINFSUP2:def 6;
for
x being
ExtReal st
x in Y holds
(Partial_Sums_in_cod2 g) . (
N,
m)
<= x
then
(Partial_Sums_in_cod2 g) . (
N,
m) is
LowerBound of
Y
by XXREAL_2:def 2;
then A19:
(Partial_Sums_in_cod2 g) . (
N,
m)
<= (inferior_realsequence (ProjMap2 ((Partial_Sums_in_cod2 f),m))) . n
by A15, XXREAL_2:def 4;
consider Z being non
empty Subset of
ExtREAL such that A20:
(
Z = { ((lim_in_cod2 (Partial_Sums_in_cod2 f)) . k) where k is Nat : n <= k } &
(inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . n = inf Z )
by RINFSUP2:def 6;
for
z being
ExtReal st
z in Z holds
ex
y being
ExtReal st
(
y in Y &
y <= z )
proof
let z be
ExtReal;
( z in Z implies ex y being ExtReal st
( y in Y & y <= z ) )
assume
z in Z
;
ex y being ExtReal st
( y in Y & y <= z )
then consider j being
Nat such that A21:
(
z = (lim_in_cod2 (Partial_Sums_in_cod2 f)) . j &
n <= j )
by A20;
reconsider j1 =
j as
Element of
NAT by ORDINAL1:def 12;
z = lim (ProjMap1 ((Partial_Sums_in_cod2 f),j1))
by A21, D1DEF6;
then A23:
z = sup (ProjMap1 ((Partial_Sums_in_cod2 f),j1))
by RINFSUP2:37;
set y =
(ProjMap2 ((Partial_Sums_in_cod2 f),m)) . j1;
take
(ProjMap2 ((Partial_Sums_in_cod2 f),m)) . j1
;
( (ProjMap2 ((Partial_Sums_in_cod2 f),m)) . j1 in Y & (ProjMap2 ((Partial_Sums_in_cod2 f),m)) . j1 <= z )
(ProjMap2 ((Partial_Sums_in_cod2 f),m)) . j1 =
(Partial_Sums_in_cod2 f) . (
j1,
m)
by MESFUNC9:def 7
.=
(ProjMap1 ((Partial_Sums_in_cod2 f),j1)) . m
by MESFUNC9:def 6
;
hence
(
(ProjMap2 ((Partial_Sums_in_cod2 f),m)) . j1 in Y &
(ProjMap2 ((Partial_Sums_in_cod2 f),m)) . j1 <= z )
by A15, A21, A23, RINFSUP2:23;
verum
end;
then
inf Y <= inf Z
by XXREAL_2:64;
hence
(Partial_Sums_in_cod2 g) . (
N,
m)
<= (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . n
by A15, A20, A19, XXREAL_0:2;
verum
end;
defpred S1[ Nat] means for m being Element of NAT st m = $1 holds
(Partial_Sums seq) . m = lim (ProjMap2 ((Partial_Sums_in_cod2 g),m));
then A28:
S1[ 0 ]
;
P1:
for m being Element of NAT holds ProjMap2 ((Partial_Sums_in_cod2 g),m) is convergent
proof
let m be
Element of
NAT ;
ProjMap2 ((Partial_Sums_in_cod2 g),m) is convergent
for
j,
i being
Nat st
i <= j holds
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i <= (ProjMap2 ((Partial_Sums_in_cod2 g),m)) . j
proof
let j,
i be
Nat;
( i <= j implies (ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i <= (ProjMap2 ((Partial_Sums_in_cod2 g),m)) . j )
reconsider i1 =
i,
j1 =
j as
Element of
NAT by ORDINAL1:def 12;
assume B2:
i <= j
;
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i <= (ProjMap2 ((Partial_Sums_in_cod2 g),m)) . j
B3:
(
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i1 = (Partial_Sums_in_cod2 g) . (
i,
m) &
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . j1 = (Partial_Sums_in_cod2 g) . (
j,
m) )
by MESFUNC9:def 7;
defpred S2[
Nat]
means (Partial_Sums_in_cod2 g) . (
i,$1)
<= (Partial_Sums_in_cod2 g) . (
j,$1);
B4:
(Partial_Sums_in_cod2 g) . (
i,
0) =
g . (
i,
0)
by DefCSM
.=
(inferior_realsequence (ProjMap2 (f,0))) . i1
by A5
;
(Partial_Sums_in_cod2 g) . (
j,
0) =
g . (
j,
0)
by DefCSM
.=
(inferior_realsequence (ProjMap2 (f,0))) . j1
by A5
;
then B5:
S2[
0 ]
by B2, B4, RINFSUP2:7;
B6:
for
l being
Nat st
S2[
l] holds
S2[
l + 1]
proof
let l be
Nat;
( S2[l] implies S2[l + 1] )
reconsider l1 =
l as
Element of
NAT by ORDINAL1:def 12;
assume B7:
S2[
l]
;
S2[l + 1]
(
g . (
i,
(l + 1))
= (inferior_realsequence (ProjMap2 (f,(l1 + 1)))) . i1 &
g . (
j,
(l + 1))
= (inferior_realsequence (ProjMap2 (f,(l1 + 1)))) . j1 )
by A5;
then B8:
g . (
i,
(l + 1))
<= g . (
j,
(l + 1))
by B2, RINFSUP2:7;
(
(Partial_Sums_in_cod2 g) . (
i,
(l + 1))
= ((Partial_Sums_in_cod2 g) . (i,l)) + (g . (i,(l + 1))) &
(Partial_Sums_in_cod2 g) . (
j,
(l + 1))
= ((Partial_Sums_in_cod2 g) . (j,l)) + (g . (j,(l + 1))) )
by DefCSM;
hence
S2[
l + 1]
by B7, B8, XXREAL_3:36;
verum
end;
for
l being
Nat holds
S2[
l]
from NAT_1:sch 2(B5, B6);
hence
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i <= (ProjMap2 ((Partial_Sums_in_cod2 g),m)) . j
by B3;
verum
end;
then
ProjMap2 (
(Partial_Sums_in_cod2 g),
m) is
non-decreasing
by RINFSUP2:7;
hence
ProjMap2 (
(Partial_Sums_in_cod2 g),
m) is
convergent
by RINFSUP2:37;
verum
end;
A29:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
reconsider k1 =
k as
Element of
NAT by ORDINAL1:def 12;
assume A30:
S1[
k]
;
S1[k + 1]
now for m being Element of NAT st m = k + 1 holds
(Partial_Sums seq) . m = lim (ProjMap2 ((Partial_Sums_in_cod2 g),m))let m be
Element of
NAT ;
( m = k + 1 implies (Partial_Sums seq) . m = lim (ProjMap2 ((Partial_Sums_in_cod2 g),m)) )assume B00:
m = k + 1
;
(Partial_Sums seq) . m = lim (ProjMap2 ((Partial_Sums_in_cod2 g),m))then B0:
(Partial_Sums seq) . m =
((Partial_Sums seq) . k) + (seq . (k + 1))
by MESFUNC9:def 1
.=
(lim (ProjMap2 ((Partial_Sums_in_cod2 g),k1))) + (seq . (k + 1))
by A30
.=
(lim (ProjMap2 ((Partial_Sums_in_cod2 g),k1))) + (lim_inf (ProjMap2 (f,(k + 1))))
by A1
;
B1:
lim_inf (ProjMap2 (f,(k + 1))) =
sup (inferior_realsequence (ProjMap2 (f,(k1 + 1))))
by RINFSUP2:def 9
.=
lim (inferior_realsequence (ProjMap2 (f,(k1 + 1))))
by RINFSUP2:37
;
B9:
ProjMap2 (
(Partial_Sums_in_cod2 g),
k1) is
convergent
by P1;
B10:
inferior_realsequence (ProjMap2 (f,(k1 + 1))) is
convergent
by RINFSUP2:37;
for
n being
object st
n in dom (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) holds
0. <= (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . n
then C2:
inferior_realsequence (ProjMap2 (f,(k1 + 1))) is
nonnegative
by SUPINF_2:52;
for
i being
Nat holds
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i = ((ProjMap2 ((Partial_Sums_in_cod2 g),k1)) . i) + ((inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . i)
proof
let i be
Nat;
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i = ((ProjMap2 ((Partial_Sums_in_cod2 g),k1)) . i) + ((inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . i)
reconsider i1 =
i as
Element of
NAT by ORDINAL1:def 12;
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i1 =
(Partial_Sums_in_cod2 g) . (
i,
m)
by MESFUNC9:def 7
.=
((Partial_Sums_in_cod2 g) . (i,k)) + (g . (i,(k + 1)))
by B00, DefCSM
.=
((ProjMap2 ((Partial_Sums_in_cod2 g),k1)) . i1) + (g . (i,(k + 1)))
by MESFUNC9:def 7
;
hence
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i = ((ProjMap2 ((Partial_Sums_in_cod2 g),k1)) . i) + ((inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . i)
by A5;
verum
end; hence
(Partial_Sums seq) . m = lim (ProjMap2 ((Partial_Sums_in_cod2 g),m))
by B0, B1, B9, B10, C2, MESFUNC9:11;
verum end;
hence
S1[
k + 1]
;
verum
end;
A30:
for k being Nat holds S1[k]
from NAT_1:sch 2(A28, A29);
A31:
for m being Nat holds (Partial_Sums seq) . m <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f))
for m being object st m in dom seq holds
0 <= seq . m
then
seq is nonnegative
by SUPINF_2:52;
then
Partial_Sums seq is non-decreasing
by MESFUNC9:16;
then
lim (Partial_Sums seq) <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f))
by A31, MESFUNC9:9, RINFSUP2:37;
hence
Sum seq <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f))
by MESFUNC9:def 3; verum