let T be non trivial RealNormSpace; :: thesis: for f being PartFunc of REAL,T
for g being PartFunc of REAL,REAL st dom f = [.0,1.] & dom g = [.0,1.] & f | [.0,1.] is continuous & g | [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & ( for x being real number st x in ].0,1.[ holds
||.(diff (f,x)).|| <= diff (g,x) ) holds
||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0)
let f be PartFunc of REAL,T; :: thesis: for g being PartFunc of REAL,REAL st dom f = [.0,1.] & dom g = [.0,1.] & f | [.0,1.] is continuous & g | [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & ( for x being real number st x in ].0,1.[ holds
||.(diff (f,x)).|| <= diff (g,x) ) holds
||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0)
let g be PartFunc of REAL,REAL; :: thesis: ( dom f = [.0,1.] & dom g = [.0,1.] & f | [.0,1.] is continuous & g | [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & ( for x being real number st x in ].0,1.[ holds
||.(diff (f,x)).|| <= diff (g,x) ) implies ||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0) )
assume A1: ( dom f = [.0,1.] & dom g = [.0,1.] & f | [.0,1.] is continuous & g | [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & ( for x being real number st x in ].0,1.[ holds
||.(diff (f,x)).|| <= diff (g,x) ) ) ; :: thesis: ||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0)
now :: thesis: for e being Real st 0 < e holds
||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0)) <= e
let e be Real; :: thesis: ( 0 < e implies ||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0)) <= e )
assume A2: 0 < e ; :: thesis: ||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0)) <= e
set e1 = e / 2;
set B = { x where x is Real : ( x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) } ;
now :: thesis: for z being set st z in { x where x is Real : ( x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) } holds
z in REAL
let z be set ; :: thesis: ( z in { x where x is Real : ( x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) } implies z in REAL )
assume z in { x where x is Real : ( x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) } ; :: thesis: z in REAL
then ex x being Real st
( z = x & x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) ;
hence z in REAL ; :: thesis: verum
end;
then reconsider B = { x where x is Real : ( x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) } as Subset of REAL by TARSKI:def 3;
now :: thesis: for r being real number st r in B holds
abs r < 2
let r be real number ; :: thesis: ( r in B implies abs r < 2 )
assume r in B ; :: thesis: abs r < 2
then ex x being Real st
( r = x & x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) ;
then A3: ex t being Real st
( r = t & 0 <= t & t <= 1 ) ;
then abs r = r by ABSVALUE:def 1;
hence abs r < 2 by A3, XXREAL_0:2; :: thesis: verum
end;
then A4: B is real-bounded by SEQ_4:4;
set s = upper_bound B;
A5: ex d being real number st
( 0 < d & d in B )
proof
0 in [.0,1.] ;
then consider d1 being real number such that
A6: ( 0 < d1 & ( for x1 being real number st x1 in [.0,1.] & abs (x1 - 0) < d1 holds
||.((f /. x1) - (f /. 0)).|| < e / 2 ) ) by A2, A1, NFCONT_3:17;
set d2 = d1 / 2;
A7: d1 / 2 < d1 by A6, XREAL_1:216;
take d = min ((d1 / 2),1); :: thesis: ( 0 < d & d in B )
thus A8: 0 < d by A6, XXREAL_0:21; :: thesis: d in B
A9: d <= 1 by XXREAL_0:17;
then A10: d in [.0,1.] by A8;
A11: d <= d1 / 2 by XXREAL_0:17;
abs (d - 0) = d by A8, ABSVALUE:def 1;
then abs (d - 0) < d1 by A11, A7, XXREAL_0:2;
then A12: ||.((f /. d) - (f /. 0)).|| < e / 2 by A6, A10;
A13: [.0,d.] c= dom g by A1, A9, XXREAL_1:34;
A14: g | [.0,d.] is continuous by A1, A9, FCONT_1:16, XXREAL_1:34;
A15: ].0,d.[ c= ].0,1.[ by A9, XXREAL_1:46;
then consider x0 being Real such that
A16: ( x0 in ].0,d.[ & diff (g,x0) = ((g . d) - (g . 0)) / (d - 0) ) by A1, A8, A13, A14, FDIFF_1:26, ROLLE:3;
||.(diff (f,x0)).|| <= diff (g,x0) by A1, A16, A15;
then 0 <= (g . d) - (g . 0) by A8, A16;
then 0 + ||.((f /. d) - (f /. 0)).|| <= ((g . d) - (g . 0)) + (e / 2) by A12, XREAL_1:7;
then 0 + ||.((f /. d) - (f /. 0)).|| <= (((g . d) - (g . 0)) + (e / 2)) + ((e / 2) * d) by A8, A2, XREAL_1:7;
then ||.((f /. d) - (f /. 0)).|| - ((((g . d) - (g . 0)) + (e / 2)) + ((e / 2) * d)) <= 0 by XREAL_1:47;
then ((||.((f /. d) - (f /. 0)).|| - ((g . d) - (g . 0))) - ((e / 2) * d)) - (e / 2) <= 0 ;
hence d in B by A10; :: thesis: verum
end;
then A17: 0 < upper_bound B by A4, SEQ_4:def 1;
now :: thesis: for r being real number st r in B holds
r <= 1
let r be real number ; :: thesis: ( r in B implies r <= 1 )
assume r in B ; :: thesis: r <= 1
then ex x being Real st
( r = x & x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) ;
then ex t being Real st
( r = t & 0 <= t & t <= 1 ) ;
hence r <= 1 ; :: thesis: verum
end;
then A18: upper_bound B <= 1 by A5, SEQ_4:45;
defpred S1[ Element of NAT , Element of REAL ] means ( $2 in B & abs ((upper_bound B) - $2) <= 1 / ($1 + 1) );
A19: now :: thesis: for x being Element of NAT ex r being Element of REAL st S1[x,r]
let x be Element of NAT ; :: thesis: ex r being Element of REAL st S1[x,r]
reconsider t = 1 / (1 + x) as real number ;
consider r being real number such that
A20: ( r in B & (upper_bound B) - t < r ) by A4, A5, SEQ_4:def 1;
reconsider r = r as Element of REAL by XREAL_0:def 1;
take r = r; :: thesis: S1[x,r]
((upper_bound B) - t) + t < r + t by A20, XREAL_1:8;
then A21: (upper_bound B) - r < (t + r) - r by XREAL_1:14;
r <= upper_bound B by A4, A20, SEQ_4:def 1;
then 0 <= (upper_bound B) - r by XREAL_1:48;
hence S1[x,r] by A20, A21, SEQ_2:1; :: thesis: verum
end;
consider sq being Function of NAT,REAL such that
A22: for x being Element of NAT holds S1[x,sq . x] from FUNCT_2:sch 3(A19);
reconsider sq = sq as Real_Sequence ;
A23: now :: thesis: for p1 being real number st 0 < p1 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((sq . m) - (upper_bound B)) < p1
let p1 be real number ; :: thesis: ( 0 < p1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((sq . m) - (upper_bound B)) < p1 )
assume A24: 0 < p1 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((sq . m) - (upper_bound B)) < p1
set p = p1 / 2;
consider n being Element of NAT such that
A25: 1 / (p1 / 2) < n by SEQ_4:3;
(1 / (p1 / 2)) + 0 < n + 1 by A25, XREAL_1:8;
then A26: 1 / (n + 1) <= 1 / (1 / (p1 / 2)) by A24, XREAL_1:118;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs ((sq . m) - (upper_bound B)) < p1
thus for m being Element of NAT st n <= m holds
abs ((sq . m) - (upper_bound B)) < p1 :: thesis: verum
proof
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((sq . m) - (upper_bound B)) < p1 )
assume n <= m ; :: thesis: abs ((sq . m) - (upper_bound B)) < p1
then ( 0 < n + 1 & n + 1 <= m + 1 ) by XREAL_1:6;
then 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
then A27: 1 / (m + 1) <= p1 / 2 by A26, XXREAL_0:2;
( sq . m in B & abs ((upper_bound B) - (sq . m)) <= 1 / (m + 1) ) by A22;
then abs ((sq . m) - (upper_bound B)) <= 1 / (1 + m) by COMPLEX1:60;
then A28: abs ((sq . m) - (upper_bound B)) <= p1 / 2 by A27, XXREAL_0:2;
p1 / 2 < p1 by A24, XREAL_1:216;
hence abs ((sq . m) - (upper_bound B)) < p1 by A28, XXREAL_0:2; :: thesis: verum
end;
end;
then A29: sq is convergent by SEQ_2:def 6;
then A30: lim sq = upper_bound B by A23, SEQ_2:def 7;
deffunc H1( Real) -> Element of REAL = ((||.((f /. $1) - (f /. 0)).|| - ((g . $1) - (g . 0))) - ((e / 2) * $1)) - (e / 2);
A31: for x being Element of REAL holds H1(x) in REAL ;
consider Lg0 being Function of REAL,REAL such that
A32: for x being Element of REAL holds Lg0 . x = H1(x) from FUNCT_2:sch 8(A31);
set Lg = Lg0 | [.0,1.];
A33: dom Lg0 = REAL by FUNCT_2:def 1;
then A34: dom (Lg0 | [.0,1.]) = [.0,1.] by RELAT_1:62;
now :: thesis: for y being set st y in rng sq holds
y in [.0,1.]
let y be set ; :: thesis: ( y in rng sq implies y in [.0,1.] )
assume y in rng sq ; :: thesis: y in [.0,1.]
then ex x being set st
( x in NAT & sq . x = y ) by FUNCT_2:11;
then y in B by A22;
then ex x being Real st
( y = x & x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) ;
hence y in [.0,1.] ; :: thesis: verum
end;
then A35: rng sq c= dom (Lg0 | [.0,1.]) by A34, TARSKI:def 3;
A36: upper_bound B in [.0,1.] by A18, A17;
now :: thesis: for r being real number st 0 < r holds
ex t being set st
( 0 < t & ( for x1 being real number st x1 in dom (Lg0 | [.0,1.]) & abs (x1 - (upper_bound B)) < t holds
abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r ) )
let r be real number ; :: thesis: ( 0 < r implies ex t being set st
( 0 < t & ( for x1 being real number st x1 in dom (Lg0 | [.0,1.]) & abs (x1 - (upper_bound B)) < t holds
abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r ) ) )
set r3 = r / 3;
assume A37: 0 < r ; :: thesis: ex t being set st
( 0 < t & ( for x1 being real number st x1 in dom (Lg0 | [.0,1.]) & abs (x1 - (upper_bound B)) < t holds
abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r ) )
then consider t1 being real number such that
A38: ( 0 < t1 & ( for x1 being real number st x1 in [.0,1.] & abs (x1 - (upper_bound B)) < t1 holds
||.((f /. x1) - (f /. (upper_bound B))).|| < r / 3 ) ) by A1, A36, NFCONT_3:17;
consider t2 being real number such that
A39: ( 0 < t2 & ( for x1 being real number st x1 in [.0,1.] & abs (x1 - (upper_bound B)) < t2 holds
abs ((g . x1) - (g . (upper_bound B))) < r / 3 ) ) by A37, A36, A1, FCONT_1:14;
set t30 = (r / 3) / (e / 2);
set t3 = ((r / 3) / (e / 2)) / 2;
( 0 < ((r / 3) / (e / 2)) / 2 & ((r / 3) / (e / 2)) / 2 < (r / 3) / (e / 2) ) by A2, A37, XREAL_1:216;
then (e / 2) * (((r / 3) / (e / 2)) / 2) < ((r / 3) / (e / 2)) * (e / 2) by A2, XREAL_1:97;
then A40: (e / 2) * (((r / 3) / (e / 2)) / 2) < r / 3 by A2, XCMPLX_1:87;
take t = min ((min (t1,t2)),(((r / 3) / (e / 2)) / 2)); :: thesis: ( 0 < t & ( for x1 being real number st x1 in dom (Lg0 | [.0,1.]) & abs (x1 - (upper_bound B)) < t holds
abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r ) )
A41: ( min (t1,t2) <= t1 & min (t1,t2) <= t2 & 0 < min (t1,t2) ) by A38, A39, XXREAL_0:17, XXREAL_0:21;
hence 0 < t by A2, A37, XXREAL_0:21; :: thesis: for x1 being real number st x1 in dom (Lg0 | [.0,1.]) & abs (x1 - (upper_bound B)) < t holds
abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r
A42: t <= ((r / 3) / (e / 2)) / 2 by XXREAL_0:17;
A43: t <= min (t1,t2) by XXREAL_0:17;
then A44: t <= t1 by A41, XXREAL_0:2;
A45: t <= t2 by A41, A43, XXREAL_0:2;
thus for x1 being real number st x1 in dom (Lg0 | [.0,1.]) & abs (x1 - (upper_bound B)) < t holds
abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r :: thesis: verum
proof
let x1 be real number ; :: thesis: ( x1 in dom (Lg0 | [.0,1.]) & abs (x1 - (upper_bound B)) < t implies abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r )
A46: x1 is Element of REAL by XREAL_0:def 1;
assume that
A47: x1 in dom (Lg0 | [.0,1.]) and
A48: abs (x1 - (upper_bound B)) < t ; :: thesis: abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r
x1 in [.0,1.] by A33, A47, RELAT_1:62;
then A49: (Lg0 | [.0,1.]) . x1 = Lg0 . x1 by FUNCT_1:49
.= ((||.((f /. x1) - (f /. 0)).|| - ((g . x1) - (g . 0))) - ((e / 2) * x1)) - (e / 2) by A32, A46 ;
(Lg0 | [.0,1.]) . (upper_bound B) = Lg0 . (upper_bound B) by A36, FUNCT_1:49;
then (Lg0 | [.0,1.]) . (upper_bound B) = ((||.((f /. (upper_bound B)) - (f /. 0)).|| - ((g . (upper_bound B)) - (g . 0))) - ((e / 2) * (upper_bound B))) - (e / 2) by A32;
then ((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B)) = ((||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||) - ((g . x1) - (g . (upper_bound B)))) - ((e / 2) * (x1 - (upper_bound B))) by A49;
then A50: abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) <= (abs ((||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||) - ((g . x1) - (g . (upper_bound B))))) + (abs ((e / 2) * (x1 - (upper_bound B)))) by COMPLEX1:57;
abs ((||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||) - ((g . x1) - (g . (upper_bound B)))) <= (abs (||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||)) + (abs ((g . x1) - (g . (upper_bound B)))) by COMPLEX1:57;
then (abs ((||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||) - ((g . x1) - (g . (upper_bound B))))) + (abs ((e / 2) * (x1 - (upper_bound B)))) <= ((abs (||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||)) + (abs ((g . x1) - (g . (upper_bound B))))) + (abs ((e / 2) * (x1 - (upper_bound B)))) by XREAL_1:6;
then A51: abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) <= ((abs (||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||)) + (abs ((g . x1) - (g . (upper_bound B))))) + (abs ((e / 2) * (x1 - (upper_bound B)))) by A50, XXREAL_0:2;
A52: abs (||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||) <= ||.(((f /. x1) - (f /. 0)) - ((f /. (upper_bound B)) - (f /. 0))).|| by NORMSP_1:9;
((f /. x1) - (f /. 0)) - ((f /. (upper_bound B)) - (f /. 0)) = (f /. x1) - ((f /. 0) - (- ((f /. (upper_bound B)) - (f /. 0)))) by RLVECT_1:29
.= (f /. x1) - ((f /. 0) + ((f /. (upper_bound B)) - (f /. 0))) by RLVECT_1:17
.= (f /. x1) - ((f /. (upper_bound B)) - ((f /. 0) - (f /. 0))) by RLVECT_1:29
.= (f /. x1) - ((f /. (upper_bound B)) - (0. T)) by RLVECT_1:5
.= (f /. x1) - (f /. (upper_bound B)) by RLVECT_1:13 ;
then (abs (||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||)) + (abs ((g . x1) - (g . (upper_bound B)))) <= ||.((f /. x1) - (f /. (upper_bound B))).|| + (abs ((g . x1) - (g . (upper_bound B)))) by A52, XREAL_1:6;
then ((abs (||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||)) + (abs ((g . x1) - (g . (upper_bound B))))) + (abs ((e / 2) * (x1 - (upper_bound B)))) <= (||.((f /. x1) - (f /. (upper_bound B))).|| + (abs ((g . x1) - (g . (upper_bound B))))) + (abs ((e / 2) * (x1 - (upper_bound B)))) by XREAL_1:6;
then A53: abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) <= (||.((f /. x1) - (f /. (upper_bound B))).|| + (abs ((g . x1) - (g . (upper_bound B))))) + (abs ((e / 2) * (x1 - (upper_bound B)))) by A51, XXREAL_0:2;
abs (x1 - (upper_bound B)) < t2 by A48, A45, XXREAL_0:2;
then abs ((g . x1) - (g . (upper_bound B))) < r / 3 by A47, A34, A39;
then A54: ||.((f /. x1) - (f /. (upper_bound B))).|| + (abs ((g . x1) - (g . (upper_bound B)))) < ||.((f /. x1) - (f /. (upper_bound B))).|| + (r / 3) by XREAL_1:8;
abs (x1 - (upper_bound B)) < ((r / 3) / (e / 2)) / 2 by A48, A42, XXREAL_0:2;
then (abs (x1 - (upper_bound B))) * (e / 2) <= (((r / 3) / (e / 2)) / 2) * (e / 2) by A2, XREAL_1:64;
then (abs (x1 - (upper_bound B))) * (abs (e / 2)) <= (((r / 3) / (e / 2)) / 2) * (e / 2) by A2, ABSVALUE:def 1;
then abs ((e / 2) * (x1 - (upper_bound B))) <= (((r / 3) / (e / 2)) / 2) * (e / 2) by COMPLEX1:65;
then A55: abs ((e / 2) * (x1 - (upper_bound B))) < r / 3 by A40, XXREAL_0:2;
abs (x1 - (upper_bound B)) < t1 by A48, A44, XXREAL_0:2;
then ||.((f /. x1) - (f /. (upper_bound B))).|| < r / 3 by A47, A34, A38;
then ||.((f /. x1) - (f /. (upper_bound B))).|| + (r / 3) < (r / 3) + (r / 3) by XREAL_1:8;
then ||.((f /. x1) - (f /. (upper_bound B))).|| + (abs ((g . x1) - (g . (upper_bound B)))) < (r / 3) + (r / 3) by A54, XXREAL_0:2;
then (||.((f /. x1) - (f /. (upper_bound B))).|| + (abs ((g . x1) - (g . (upper_bound B))))) + (abs ((e / 2) * (x1 - (upper_bound B)))) < ((r / 3) + (r / 3)) + (r / 3) by A55, XREAL_1:8;
hence abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r by A53, XXREAL_0:2; :: thesis: verum
end;
end;
then Lg0 | [.0,1.] is_continuous_in upper_bound B by FCONT_1:3;
then A56: ( (Lg0 | [.0,1.]) /* sq is convergent & (Lg0 | [.0,1.]) . (upper_bound B) = lim ((Lg0 | [.0,1.]) /* sq) ) by A29, A30, A35, FCONT_1:def 1;
A57: for n being Element of NAT holds 0 <= (- ((Lg0 | [.0,1.]) /* sq)) . n
proof
let n be Element of NAT ; :: thesis: 0 <= (- ((Lg0 | [.0,1.]) /* sq)) . n
(- ((Lg0 | [.0,1.]) /* sq)) . n = - (((Lg0 | [.0,1.]) /* sq) . n) by SEQ_1:10;
then A58: (- ((Lg0 | [.0,1.]) /* sq)) . n = - ((Lg0 | [.0,1.]) . (sq . n)) by A35, FUNCT_2:108;
S1[n,sq . n] by A22;
then A59: ex x being Real st
( sq . n = x & x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) ;
then Lg0 . (sq . n) <= 0 by A32;
then (Lg0 | [.0,1.]) . (sq . n) <= 0 by A59, FUNCT_1:49;
hence 0 <= (- ((Lg0 | [.0,1.]) /* sq)) . n by A58; :: thesis: verum
end;
- ((Lg0 | [.0,1.]) /* sq) is convergent by A56, SEQ_2:9;
then 0 <= lim (- ((Lg0 | [.0,1.]) /* sq)) by A57, SEQ_2:17;
then 0 <= - (lim ((Lg0 | [.0,1.]) /* sq)) by A56, SEQ_2:10;
then (Lg0 | [.0,1.]) . (upper_bound B) <= 0 by A56;
then Lg0 . (upper_bound B) <= 0 by A36, FUNCT_1:49;
then A60: ((||.((f /. (upper_bound B)) - (f /. 0)).|| - ((g . (upper_bound B)) - (g . 0))) - ((e / 2) * (upper_bound B))) - (e / 2) <= 0 by A32;
A61: upper_bound B = 1
proof
assume upper_bound B <> 1 ; :: thesis: contradiction
then upper_bound B < 1 by A18, XXREAL_0:1;
then A62: upper_bound B in ].0,1.[ by A17;
then f is_differentiable_in upper_bound B by A1, NDIFF_3:10;
then consider N1 being Neighbourhood of upper_bound B such that
A63: ( N1 c= dom f & ex L1 being LinearFunc of T ex R1 being RestFunc of T st
( diff (f,(upper_bound B)) = L1 . 1 & ( for x being Real st x in N1 holds
(f /. x) - (f /. (upper_bound B)) = (L1 . (x - (upper_bound B))) + (R1 /. (x - (upper_bound B))) ) ) ) by NDIFF_3:def 4;
consider L1 being LinearFunc of T, R1 being RestFunc of T such that
A64: ( diff (f,(upper_bound B)) = L1 . 1 & ( for x being Real st x in N1 holds
(f /. x) - (f /. (upper_bound B)) = (L1 . (x - (upper_bound B))) + (R1 /. (x - (upper_bound B))) ) ) by A63;
g is_differentiable_in upper_bound B by A1, A62, FDIFF_1:9;
then consider N2 being Neighbourhood of upper_bound B such that
A65: ( N2 c= dom g & ex L2 being LinearFunc ex R2 being RestFunc st
( diff (g,(upper_bound B)) = L2 . 1 & ( for x being Real st x in N2 holds
(g . x) - (g . (upper_bound B)) = (L2 . (x - (upper_bound B))) + (R2 . (x - (upper_bound B))) ) ) ) by FDIFF_1:def 5;
consider L2 being LinearFunc, R2 being RestFunc such that
A66: ( diff (g,(upper_bound B)) = L2 . 1 & ( for x being Real st x in N2 holds
(g . x) - (g . (upper_bound B)) = (L2 . (x - (upper_bound B))) + (R2 . (x - (upper_bound B))) ) ) by A65;
consider NN3 being Neighbourhood of upper_bound B such that
A67: ( NN3 c= N1 & NN3 c= N2 ) by RCOMP_1:17;
consider g0 being real number such that
A68: ( 0 < g0 & ].((upper_bound B) - g0),((upper_bound B) + g0).[ c= ].0,1.[ ) by A62, RCOMP_1:19;
reconsider NN4 = ].((upper_bound B) - g0),((upper_bound B) + g0).[ as Neighbourhood of upper_bound B by A68, RCOMP_1:def 6;
consider N3 being Neighbourhood of upper_bound B such that
A69: ( N3 c= NN3 & N3 c= NN4 ) by RCOMP_1:17;
A70: ( N3 c= N1 & N3 c= N2 & N3 c= ].0,1.[ ) by A69, A67, A68, XBOOLE_1:1;
consider d1 being real number such that
A71: ( 0 < d1 & N3 = ].((upper_bound B) - d1),((upper_bound B) + d1).[ ) by RCOMP_1:def 6;
set e2 = (e / 2) / 2;
( R1 is total & R1 is RestFunc-like ) by NDIFF_3:def 1;
then consider d2 being Real such that
A72: ( 0 < d2 & ( for t being Real st t <> 0 & abs t < d2 holds
||.(R1 /. t).|| / (abs t) < (e / 2) / 2 ) ) by A2, Th17;
( R2 is total & R2 is RestFunc-like ) by FDIFF_1:def 2;
then consider d3 being Real such that
A73: ( 0 < d3 & ( for t being Real st t <> 0 & abs t < d3 holds
(abs (R2 . t)) / (abs t) < (e / 2) / 2 ) ) by A2, Th18;
A74: ( min (d1,d2) <= d1 & min (d1,d2) <= d2 & 0 < min (d1,d2) ) by A71, A72, XXREAL_0:17, XXREAL_0:21;
set d40 = min ((min (d1,d2)),d3);
A75: ( min ((min (d1,d2)),d3) <= min (d1,d2) & min ((min (d1,d2)),d3) <= d3 & 0 < min ((min (d1,d2)),d3) ) by A73, A74, XXREAL_0:17, XXREAL_0:21;
set d4 = (min ((min (d1,d2)),d3)) / 2;
A76: ( min ((min (d1,d2)),d3) <= d1 & min ((min (d1,d2)),d3) <= d2 ) by A74, A75, XXREAL_0:2;
(min ((min (d1,d2)),d3)) / 2 < min ((min (d1,d2)),d3) by A75, XREAL_1:216;
then A77: ( 0 < (min ((min (d1,d2)),d3)) / 2 & (min ((min (d1,d2)),d3)) / 2 < d1 & (min ((min (d1,d2)),d3)) / 2 < d2 & (min ((min (d1,d2)),d3)) / 2 < d3 ) by A75, A76, XXREAL_0:2;
then ( (upper_bound B) - d1 < (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) & (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) < (upper_bound B) + d1 ) by XREAL_1:8;
then A78: (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) in N3 by A71;
then A79: (f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B)) = (L1 . (((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)) - (upper_bound B))) + (R1 /. (((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)) - (upper_bound B))) by A64, A70;
A80: (g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B)) = (L2 . (((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)) - (upper_bound B))) + (R2 . (((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)) - (upper_bound B))) by A70, A78, A66;
consider df1 being Point of T such that
A81: for p being Real holds L1 . p = p * df1 by NDIFF_3:def 2;
L1 . 1 = 1 * df1 by A81;
then L1 . 1 = df1 by RLVECT_1:def 8;
then A82: L1 . ((min ((min (d1,d2)),d3)) / 2) = ((min ((min (d1,d2)),d3)) / 2) * (diff (f,(upper_bound B))) by A64, A81;
consider df2 being Real such that
A83: for p being Real holds L2 . p = df2 * p by FDIFF_1:def 3;
L2 . 1 = df2 * 1 by A83;
then A84: L2 . ((min ((min (d1,d2)),d3)) / 2) = ((min ((min (d1,d2)),d3)) / 2) * (diff (g,(upper_bound B))) by A66, A83;
A85: ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| <= ||.(L1 . ((min ((min (d1,d2)),d3)) / 2)).|| + ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| by A79, NORMSP_1:def 1;
A86: ||.(L1 . ((min ((min (d1,d2)),d3)) / 2)).|| = (abs ((min ((min (d1,d2)),d3)) / 2)) * ||.(diff (f,(upper_bound B))).|| by A82, NORMSP_1:def 1
.= ||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2) by A75, ABSVALUE:def 1 ;
A87: 0 < abs ((min ((min (d1,d2)),d3)) / 2) by A75, ABSVALUE:def 1;
abs ((min ((min (d1,d2)),d3)) / 2) < d2 by A77, ABSVALUE:def 1;
then ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| / (abs ((min ((min (d1,d2)),d3)) / 2)) < (e / 2) / 2 by A72, A75;
then ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| <= ((e / 2) / 2) * (abs ((min ((min (d1,d2)),d3)) / 2)) by A87, XREAL_1:81;
then ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| <= ((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2) by A75, ABSVALUE:def 1;
then ||.(L1 . ((min ((min (d1,d2)),d3)) / 2)).|| + ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| <= (||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by A86, XREAL_1:6;
then A88: ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| <= (||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by A85, XXREAL_0:2;
||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2) <= (diff (g,(upper_bound B))) * ((min ((min (d1,d2)),d3)) / 2) by A62, A1, A77, XREAL_1:64;
then (||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) <= ((diff (g,(upper_bound B))) * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by XREAL_1:6;
then A89: ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| <= ((diff (g,(upper_bound B))) * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by A88, XXREAL_0:2;
abs ((min ((min (d1,d2)),d3)) / 2) < d3 by A77, ABSVALUE:def 1;
then (abs (R2 . ((min ((min (d1,d2)),d3)) / 2))) / (abs ((min ((min (d1,d2)),d3)) / 2)) < (e / 2) / 2 by A73, A75;
then abs (R2 . ((min ((min (d1,d2)),d3)) / 2)) <= ((e / 2) / 2) * (abs ((min ((min (d1,d2)),d3)) / 2)) by A87, XREAL_1:81;
then abs (R2 . ((min ((min (d1,d2)),d3)) / 2)) <= ((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2) by A75, ABSVALUE:def 1;
then - (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) <= R2 . ((min ((min (d1,d2)),d3)) / 2) by ABSVALUE:5;
then (((min ((min (d1,d2)),d3)) / 2) * (diff (g,(upper_bound B)))) - (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) <= (g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B)) by A80, A84, XREAL_1:6;
then ((min ((min (d1,d2)),d3)) / 2) * (diff (g,(upper_bound B))) <= ((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B))) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by XREAL_1:20;
then ((diff (g,(upper_bound B))) * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) <= (((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B))) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2))) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by XREAL_1:6;
then ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| <= ((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B))) + ((e / 2) * ((min ((min (d1,d2)),d3)) / 2)) by A89, XXREAL_0:2;
then ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| - (((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B))) + ((e / 2) * ((min ((min (d1,d2)),d3)) / 2))) <= 0 by XREAL_1:47;
then A90: (((||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| - (g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)))) + (g . (upper_bound B))) - ((e / 2) * ((min ((min (d1,d2)),d3)) / 2))) + (((||.((f /. (upper_bound B)) - (f /. 0)).|| - ((g . (upper_bound B)) - (g . 0))) - ((e / 2) * (upper_bound B))) - (e / 2)) <= 0 + 0 by A60;
||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. 0)).|| <= ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| + ||.((f /. (upper_bound B)) - (f /. 0)).|| by NORMSP_1:10;
then ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. 0)).|| - ((((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . 0)) + ((e / 2) * (((min ((min (d1,d2)),d3)) / 2) + (upper_bound B)))) + (e / 2)) <= (||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| + ||.((f /. (upper_bound B)) - (f /. 0)).||) - ((((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . 0)) + ((e / 2) * (((min ((min (d1,d2)),d3)) / 2) + (upper_bound B)))) + (e / 2)) by XREAL_1:9;
then A91: ((||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. 0)).|| - ((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . 0))) - ((e / 2) * ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)))) - (e / 2) <= 0 by A90;
abs ((0 + 1) - (2 * ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)))) < 1 - 0 by A78, A70, RCOMP_1:3;
then (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) in [.0,1.] by RCOMP_1:2;
then A92: (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) in B by A91;
(upper_bound B) + 0 < (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) by A75, XREAL_1:8;
hence contradiction by A92, A4, SEQ_4:def 1; :: thesis: verum
end;
( 0 in dom g & 1 in dom g ) by A1;
then ( g /. 1 = g . 1 & g /. 0 = g . 0 ) by PARTFUN1:def 6;
then ((||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0))) - e) + e <= 0 + e by A61, A60, XREAL_1:6;
hence ||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0)) <= e ; :: thesis: verum
end;
then ||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0)) <= 0 by Lm3;
then (||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0))) + ((g /. 1) - (g /. 0)) <= 0 + ((g /. 1) - (g /. 0)) by XREAL_1:6;
hence ||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0) ; :: thesis: verum