let f be Real_Sequence; for a, r being positive Real st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )
let a, r be positive Real; ( r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) implies ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) )
deffunc H1( Nat, Real) -> Element of REAL = In (((f . ($1 + 1)) - (f . $1)),REAL);
consider g being sequence of REAL such that
A1:
( g . 0 = f . 0 & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) )
from NAT_1:sch 12();
now for n being Nat holds f . (n + 1) = (f . n) + (g . (n + 1))let n be
Nat;
f . (n + 1) = (f . n) + (g . (n + 1))A2:
g . (n + 1) = H1(
n,
g . n)
by A1;
thus f . (n + 1) =
((f . (n + 1)) - (f . n)) + (f . n)
.=
(f . n) + (g . (n + 1))
by A2
;
verum end;
then A3:
f = Partial_Sums g
by A1, SERIES_1:def 1;
A5:
|.r.| = r
by COMPLEX1:43;
assume A6:
r < 1
; ( ex n being Nat st not |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) or ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) )
then A7:
r GeoSeq is summable
by A5, SERIES_1:24;
assume A8:
for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n)
; ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )
(a * (r ")) (#) (r GeoSeq) is summable
by A7, SERIES_1:10;
then
abs g is summable
by A4, A9, SERIES_1:19;
then A12:
g is absolutely_summable
by SERIES_1:def 4;
then
g is summable
;
hence
f is convergent
by A3, SERIES_1:def 2; for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r)
let n be Nat; |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r)
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
A14:
(a * (r to_power n)) (#) (r GeoSeq) is summable
by A7, SERIES_1:10;
then
abs (g ^\ (n9 + 1)) is summable
by A13, SERIES_1:20;
then A15:
g ^\ (n9 + 1) is absolutely_summable
by SERIES_1:def 4;
lim f = Sum g
by A3, SERIES_1:def 3;
then
lim f = (f . n) + (Sum (g ^\ (n9 + 1)))
by A3, A12, SERIES_1:15;
then A16:
|.((lim f) - (f . n)).| <= Sum (abs (g ^\ (n9 + 1)))
by A15, Th6;
A17:
Sum (abs (g ^\ (n9 + 1))) <= Sum ((a * (r to_power n)) (#) (r GeoSeq))
by A14, A13, SERIES_1:20;
Sum ((a * (r to_power n)) (#) (r GeoSeq)) =
(a * (r to_power n)) * (Sum (r GeoSeq))
by A7, SERIES_1:10
.=
(a * (r to_power n)) * (1 / (1 - r))
by A6, A5, SERIES_1:24
.=
(a * (r to_power n)) / (1 - r)
by XCMPLX_1:99
;
hence
|.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r)
by A17, A16, XXREAL_0:2; verum