let X, Z be non empty set ; for F being Functional_Sequence of X,REAL st Z common_on_dom F holds
for a, r being positive real number st r < 1 & ( for n being natural number holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_unif_conv_on Z & ( for n being natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
let F be Functional_Sequence of X,REAL ; ( Z common_on_dom F implies for a, r being positive real number st r < 1 & ( for n being natural number holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_unif_conv_on Z & ( for n being natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) )
assume A1:
Z common_on_dom F
; for a, r being positive real number st r < 1 & ( for n being natural number holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_unif_conv_on Z & ( for n being natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
Z c= dom (F . 0 )
by A1, SEQFUNC:def 10;
then reconsider Z9 = Z as non empty Subset of X by XBOOLE_1:1;
deffunc H1( Element of Z9) -> Element of REAL = lim (F # $1);
let a, r be positive real number ; ( r < 1 & ( for n being natural number holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) implies ( F is_unif_conv_on Z & ( for n being natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) )
assume A2:
r < 1
; ( ex n being natural number st not (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) or ( F is_unif_conv_on Z & ( for n being natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) )
consider f being Function of Z9,REAL such that
A3:
for x being Element of Z9 holds f . x = H1(x)
from FUNCT_2:sch 4();
reconsider f = f as PartFunc of X,REAL by RELSET_1:17;
assume A4:
for n being natural number holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n)
; ( F is_unif_conv_on Z & ( for n being natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
thus
F is_unif_conv_on Z
for n being natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r)proof
thus
Z common_on_dom F
by A1;
SEQFUNC:def 13 ex b1 being Element of K6(K7(X,REAL )) st
( Z = dom b1 & ( for b2 being Element of REAL holds
( b2 <= 0 or ex b3 being Element of NAT st
for b4 being Element of NAT
for b5 being Element of X holds
( not b3 <= b4 or not b5 in Z or not b2 <= abs (((F . b4) . b5) - (b1 . b5)) ) ) ) )
take
f
;
( Z = dom f & ( for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT
for b4 being Element of X holds
( not b2 <= b3 or not b4 in Z or not b1 <= abs (((F . b3) . b4) - (f . b4)) ) ) ) )
thus
Z = dom f
by FUNCT_2:def 1;
for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT
for b4 being Element of X holds
( not b2 <= b3 or not b4 in Z or not b1 <= abs (((F . b3) . b4) - (f . b4)) ) )
A5:
1
- r > 0
by A2, XREAL_1:52;
let p be
Real;
( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT
for b3 being Element of X holds
( not b1 <= b2 or not b3 in Z or not p <= abs (((F . b2) . b3) - (f . b3)) ) )
assume
p > 0
;
ex b1 being Element of NAT st
for b2 being Element of NAT
for b3 being Element of X holds
( not b1 <= b2 or not b3 in Z or not p <= abs (((F . b2) . b3) - (f . b3)) )
then
p * (1 - r) > 0
by A5, XREAL_1:131;
then A6:
(p * (1 - r)) / a > 0
by XREAL_1:141;
consider k being
Element of
NAT such that A7:
k >= 1
+ (log r,((p * (1 - r)) / a))
by MESFUNC1:11;
A8:
(
a * ((p * (1 - r)) / a) = (p * (1 - r)) * (a / a) &
a / a = 1 )
by XCMPLX_1:60, XCMPLX_1:76;
k > log r,
((p * (1 - r)) / a)
by A7, XREAL_1:41;
then
r to_power k < r to_power (log r,((p * (1 - r)) / a))
by A2, POWER:45;
then
r to_power k < (p * (1 - r)) / a
by A2, A6, POWER:def 3;
then
a * (r to_power k) < a * ((p * (1 - r)) / a)
by XREAL_1:70;
then
(a * (r to_power k)) / (1 - r) < (p * (1 - r)) / (1 - r)
by A5, A8, XREAL_1:76;
then A9:
(a * (r to_power k)) / (1 - r) < p
by A5, XCMPLX_1:90;
take
k
;
for b1 being Element of NAT
for b2 being Element of X holds
( not k <= b1 or not b2 in Z or not p <= abs (((F . b1) . b2) - (f . b2)) )
let n be
Element of
NAT ;
for b1 being Element of X holds
( not k <= n or not b1 in Z or not p <= abs (((F . n) . b1) - (f . b1)) )let x be
Element of
X;
( not k <= n or not x in Z or not p <= abs (((F . n) . x) - (f . x)) )
assume that A10:
n >= k
and A11:
x in Z
;
not p <= abs (((F . n) . x) - (f . x))
A12:
(
(F . n) . x = (F # x) . n &
|.(((F . n) . x) - (f . x)).| = |.((f . x) - ((F . n) . x)).| )
by COMPLEX1:146, SEQFUNC:def 11;
now let n be
natural number ;
|.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)A13:
n in NAT
by ORDINAL1:def 13;
then A14:
(F # x) . n = (F . n) . x
by SEQFUNC:def 11;
A15:
Z c= dom (F . (n + 1))
by A1, SEQFUNC:def 10;
Z c= dom (F . n)
by A1, A13, SEQFUNC:def 10;
then
x in (dom (F . n)) /\ (dom (F . (n + 1)))
by A11, A15, XBOOLE_0:def 4;
then
x in dom ((F . n) - (F . (n + 1)))
by VALUED_1:12;
then A16:
(
((F . n) - (F . (n + 1))) . x = ((F . n) . x) - ((F . (n + 1)) . x) &
x in Z /\ (dom ((F . n) - (F . (n + 1)))) )
by A11, VALUED_1:13, XBOOLE_0:def 4;
(F . n) - (F . (n + 1)),
Z is_absolutely_bounded_by a * (r to_power n)
by A4;
then
|.(((F . n) . x) - ((F . (n + 1)) . x)).| <= a * (r to_power n)
by A16, Def1;
hence
|.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)
by A14, SEQFUNC:def 11;
verum end;
then A17:
|.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r)
by A2, Th9;
(
n = k or
n > k )
by A10, XXREAL_0:1;
then
r to_power n <= r to_power k
by A2, POWER:45;
then A18:
a * (r to_power n) <= a * (r to_power k)
by XREAL_1:66;
1
- r > 1
- 1
by A2, XREAL_1:12;
then
(a * (r to_power n)) / (1 - r) <= (a * (r to_power k)) / (1 - r)
by A18, XREAL_1:74;
then A19:
|.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power k)) / (1 - r)
by A17, XXREAL_0:2;
f . x = lim (F # x)
by A3, A11;
hence
|.(((F . n) . x) - (f . x)).| < p
by A9, A19, A12, XXREAL_0:2;
verum
end;
then A20:
F is_point_conv_on Z
by SEQFUNC:23;
let n9 be natural number ; (lim F,Z) - (F . n9),Z is_absolutely_bounded_by (a * (r to_power n9)) / (1 - r)
let z be set ; TIETZE:def 1 ( z in Z /\ (dom ((lim F,Z) - (F . n9))) implies abs (((lim F,Z) - (F . n9)) . z) <= (a * (r to_power n9)) / (1 - r) )
reconsider n = n9 as Element of NAT by ORDINAL1:def 13;
assume A21:
z in Z /\ (dom ((lim F,Z) - (F . n9)))
; abs (((lim F,Z) - (F . n9)) . z) <= (a * (r to_power n9)) / (1 - r)
then reconsider x = z as Element of X ;
A22:
z in Z9
by A21, XBOOLE_0:def 4;
now let n be
natural number ;
|.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)A23:
(F # x) . (n + 1) = (F . (n + 1)) . x
by SEQFUNC:def 11;
A24:
Z c= dom (F . (n + 1))
by A1, SEQFUNC:def 10;
A25:
n in NAT
by ORDINAL1:def 13;
then
Z c= dom (F . n)
by A1, SEQFUNC:def 10;
then
z in (dom (F . n)) /\ (dom (F . (n + 1)))
by A22, A24, XBOOLE_0:def 4;
then A26:
x in dom ((F . n) - (F . (n + 1)))
by VALUED_1:12;
then A27:
x in Z /\ (dom ((F . n) - (F . (n + 1))))
by A22, XBOOLE_0:def 4;
A28:
(F . n) - (F . (n + 1)),
Z is_absolutely_bounded_by a * (r to_power n)
by A4;
(F # x) . n = (F . n) . x
by A25, SEQFUNC:def 11;
then
((F . n) - (F . (n + 1))) . x = ((F # x) . n) - ((F # x) . (n + 1))
by A26, A23, VALUED_1:13;
hence
|.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)
by A27, A28, Def1;
verum end;
then A29:
|.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r)
by A2, Th9;
Z = dom (lim F,Z)
by A20, SEQFUNC:def 14;
then
|.(((lim F,Z) . x) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r)
by A20, A22, A29, SEQFUNC:def 14;
then A30:
|.(((lim F,Z) . x) - ((F . n) . x)).| <= (a * (r to_power n)) / (1 - r)
by SEQFUNC:def 11;
z in dom ((lim F,Z) - (F . n9))
by A21, XBOOLE_0:def 4;
hence
abs (((lim F,Z) - (F . n9)) . z) <= (a * (r to_power n9)) / (1 - r)
by A30, VALUED_1:13; verum