let X be Banach_Algebra; for w, z being Element of X
for p being Real st p > 0 holds
ex n being Nat st
for k being Nat st n <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
let w, z be Element of X; for p being Real st p > 0 holds
ex n being Nat st
for k being Nat st n <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
let p be Real; ( p > 0 implies ex n being Nat st
for k being Nat st n <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p )
assume A1:
p > 0
; ex n being Nat st
for k being Nat st n <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
reconsider pp = p as Real ;
set p1 = min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))));
A2:
1 <= Sum (||.z.|| rExpSeq)
by Th29;
then
0 * (Sum (||.z.|| rExpSeq)) < 4 * (Sum (||.z.|| rExpSeq))
by XREAL_1:68;
then A3:
0 / (4 * (Sum (||.z.|| rExpSeq))) < p / (4 * (Sum (||.z.|| rExpSeq)))
by A1, XREAL_1:74;
A4:
1 <= Sum (||.w.|| rExpSeq)
by Th29;
then
0 * (Sum (||.w.|| rExpSeq)) < 4 * (Sum (||.w.|| rExpSeq))
by XREAL_1:68;
then
0 / (4 * (Sum (||.w.|| rExpSeq))) < p / (4 * (Sum (||.w.|| rExpSeq)))
by A1, XREAL_1:74;
then A5:
min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) > 0
by A3, XXREAL_0:15;
Partial_Sums (w rExpSeq) is convergent
by LOPBAN_3:def 1;
then
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((Partial_Sums (w rExpSeq)) . m) - ((Partial_Sums (w rExpSeq)) . n)).|| < s
by LOPBAN_3:4;
then
Partial_Sums (w rExpSeq) is Cauchy_sequence_by_Norm
by LOPBAN_3:5;
then consider n2 being Nat such that
A6:
for k, l being Nat st n2 <= k & n2 <= l holds
||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . l)).|| < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))
by A5, RSSPACE3:8;
||.z.|| rExpSeq is summable
by SIN_COS:45;
then
Partial_Sums (||.z.|| rExpSeq) is convergent
by SERIES_1:def 2;
then consider n1 being Nat such that
A7:
for k, l being Nat st n1 <= k & n1 <= l holds
|.(((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . l)).| < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))
by A5, COMSEQ_3:4;
set n3 = n1 + n2;
take n4 = (n1 + n2) + (n1 + n2); for k being Nat st n4 <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
A8:
now for n, k, l being Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).||let n,
k,
l be
Nat;
( l <= k implies ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| )assume A9:
l <= k
;
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).||A10:
||.(((z rExpSeq) . l) * (((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l)))).|| <= ||.((z rExpSeq) . l).|| * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).||
by LOPBAN_3:38;
0 <= ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).||
by NORMSP_1:4;
then A11:
||.((z rExpSeq) . l).|| * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).||
by Th14, XREAL_1:64;
||.(Conj (k,z,w)).|| . l =
||.((Conj (k,z,w)) . l).||
by NORMSP_0:def 4
.=
||.(((z rExpSeq) . l) * (((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l)))).||
by A9, Def9
;
hence
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).||
by A10, A11, XXREAL_0:2;
verum end;
A12:
now for k, l being Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq)))let k,
l be
Nat;
( l <= k implies ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) )A13:
||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ||.((Partial_Sums (w rExpSeq)) . k).|| + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).||
by NORMSP_1:3;
||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= Sum (||.w.|| rExpSeq)
by Th28;
then A14:
(Sum (||.w.|| rExpSeq)) + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq)) + (Sum (||.w.|| rExpSeq))
by XREAL_1:6;
||.((Partial_Sums (w rExpSeq)) . k).|| <= Sum (||.w.|| rExpSeq)
by Th28;
then
||.((Partial_Sums (w rExpSeq)) . k).|| + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq)) + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).||
by XREAL_1:6;
then
||.((Partial_Sums (w rExpSeq)) . k).|| + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= 2
* (Sum (||.w.|| rExpSeq))
by A14, XXREAL_0:2;
then A15:
||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= 2
* (Sum (||.w.|| rExpSeq))
by A13, XXREAL_0:2;
assume
l <= k
;
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq)))then A16:
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).||
by A8;
0 <= (||.z.|| rExpSeq) . l
by Th27;
then
((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq)))
by A15, XREAL_1:64;
hence
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq)))
by A16, XXREAL_0:2;
verum end;
now for k being Nat st n4 <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
0 < p / 4
by A1, XREAL_1:224;
then A17:
0 + (p / 4) < (p / 4) + (p / 4)
by XREAL_1:6;
A18:
0 <> Sum (||.z.|| rExpSeq)
by Th29;
A19:
(Sum (||.z.|| rExpSeq)) * (p / (4 * (Sum (||.z.|| rExpSeq)))) =
(Sum (||.z.|| rExpSeq)) * (p * ((4 * (Sum (||.z.|| rExpSeq))) "))
by XCMPLX_0:def 9
.=
((Sum (||.z.|| rExpSeq)) * p) * ((4 * (Sum (||.z.|| rExpSeq))) ")
.=
((Sum (||.z.|| rExpSeq)) * p) / (4 * (Sum (||.z.|| rExpSeq)))
by XCMPLX_0:def 9
.=
p / 4
by A18, XCMPLX_1:91
;
let k be
Nat;
( n4 <= k implies |.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p )assume A20:
n4 <= k
;
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < pA21:
0 + (n1 + n2) <= (n1 + n2) + (n1 + n2)
by XREAL_1:6;
then
k -' (n1 + n2) = k - (n1 + n2)
by A20, XREAL_1:233, XXREAL_0:2;
then A22:
k = (k -' (n1 + n2)) + (n1 + n2)
;
A23:
n1 + n2 <= k
by A20, A21, XXREAL_0:2;
now for l being Nat st l <= n1 + n2 holds
||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l)let l be
Nat;
( l <= n1 + n2 implies ||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l) )A24:
0 + n2 <= n1 + n2
by XREAL_1:6;
0 + (n1 + n2) <= (n1 + n2) + (n1 + n2)
by XREAL_1:6;
then
n2 <= n4
by A24, XXREAL_0:2;
then A25:
n2 <= k
by A20, XXREAL_0:2;
A26:
0 <= (||.z.|| rExpSeq) . l
by Th27;
assume A27:
l <= n1 + n2
;
||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l)then A28:
((n1 + n2) + (n1 + n2)) - (n1 + n2) <= ((n1 + n2) + (n1 + n2)) - l
by XREAL_1:10;
l <= k
by A23, A27, XXREAL_0:2;
then A29:
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).||
by A8;
n4 - l <= k - l
by A20, XREAL_1:9;
then A30:
n1 + n2 <= k - l
by A28, XXREAL_0:2;
k -' l = k - l
by A23, A27, XREAL_1:233, XXREAL_0:2;
then
n2 <= k -' l
by A24, A30, XXREAL_0:2;
then
||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| < min (
(pp / (4 * (Sum (||.z.|| rExpSeq)))),
(pp / (4 * (Sum (||.w.|| rExpSeq)))))
by A6, A25;
then
((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))))
by A26, XREAL_1:64;
hence
||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l)
by A29, XXREAL_0:2;
verum end; then A31:
(Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) <= ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))))
by COMSEQ_3:7;
A32:
n1 + 0 <= n1 + n2
by XREAL_1:6;
then
n1 <= k
by A23, XXREAL_0:2;
then
|.(((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2))).| <= min (
(pp / (4 * (Sum (||.z.|| rExpSeq)))),
(pp / (4 * (Sum (||.w.|| rExpSeq)))))
by A7, A32;
then
((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2)) <= min (
(pp / (4 * (Sum (||.z.|| rExpSeq)))),
(pp / (4 * (Sum (||.w.|| rExpSeq)))))
by A20, A21, Th30, XXREAL_0:2;
then A33:
(((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2))) * (2 * (Sum (||.w.|| rExpSeq))) <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * (2 * (Sum (||.w.|| rExpSeq)))
by A4, XREAL_1:64;
for
l being
Nat st
l <= k holds
||.(Conj (k,z,w)).|| . l <= (2 * (Sum (||.w.|| rExpSeq))) * ((||.z.|| rExpSeq) . l)
by A12;
then
((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) <= (((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2))) * (2 * (Sum (||.w.|| rExpSeq)))
by A22, COMSEQ_3:8;
then A34:
((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * (2 * (Sum (||.w.|| rExpSeq)))
by A33, XXREAL_0:2;
A35:
0 <> Sum (||.w.|| rExpSeq)
by Th29;
((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) <= (Sum (||.z.|| rExpSeq)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))))
by A5, Th28, XREAL_1:64;
then A36:
(Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) <= (Sum (||.z.|| rExpSeq)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))))
by A31, XXREAL_0:2;
(Sum (||.z.|| rExpSeq)) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) <= (Sum (||.z.|| rExpSeq)) * (p / (4 * (Sum (||.z.|| rExpSeq))))
by A2, XREAL_1:64, XXREAL_0:17;
then
(Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) <= p / 4
by A36, A19, XXREAL_0:2;
then A37:
(Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2) < p / 2
by A17, XXREAL_0:2;
0 * (Sum (||.w.|| rExpSeq)) < 2
* (Sum (||.w.|| rExpSeq))
by A4, XREAL_1:68;
then A38:
(2 * (Sum (||.w.|| rExpSeq))) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) <= (2 * (Sum (||.w.|| rExpSeq))) * (p / (4 * (Sum (||.w.|| rExpSeq))))
by XREAL_1:64, XXREAL_0:17;
(2 * (Sum (||.w.|| rExpSeq))) * (p / (4 * (Sum (||.w.|| rExpSeq)))) =
(2 * (Sum (||.w.|| rExpSeq))) * (p * ((4 * (Sum (||.w.|| rExpSeq))) "))
by XCMPLX_0:def 9
.=
((2 * (Sum (||.w.|| rExpSeq))) * p) * ((4 * (Sum (||.w.|| rExpSeq))) ")
.=
((2 * p) * (Sum (||.w.|| rExpSeq))) / (4 * (Sum (||.w.|| rExpSeq)))
by XCMPLX_0:def 9
.=
(2 * p) / 4
by A35, XCMPLX_1:91
.=
p / 2
;
then
((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) <= p / 2
by A34, A38, XXREAL_0:2;
then
(((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2))) + ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) < (p / 2) + (p / 2)
by A37, XREAL_1:8;
hence
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
by Th31;
verum end;
hence
for k being Nat st n4 <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
; verum