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
let e be Real; :: thesis: ( 0 < e implies ||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0)) <= e )
assume P1: 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
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
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 P10: ex t being Real st
( r = t & 0 <= t & t <= 1 ) ;
then abs r = r by ABSVALUE:def 1;
hence abs r < 2 by P10, XXREAL_0:2; :: thesis: verum
end;
then Q1: B is bounded by SEQ_4:4;
set s = upper_bound B;
Q2: ex d being real number st
( 0 < d & d in B )
proof
0 in [.0,1.] ;
then consider d1 being real number such that
Q21: ( 0 < d1 & ( for x1 being real number st x1 in [.0,1.] & abs (x1 - 0) < d1 holds
||.((f /. x1) - (f /. 0)).|| < e / 2 ) ) by P1, A1, NFCONT_3:17;
set d2 = d1 / 2;
Q23: d1 / 2 < d1 by Q21, XREAL_1:216;
take d = min ((d1 / 2),1); :: thesis: ( 0 < d & d in B )
thus Q26: 0 < d by Q21, XXREAL_0:21; :: thesis: d in B
Q24: d <= 1 by XXREAL_0:17;
then Q27: d in [.0,1.] by Q26;
V24: d <= d1 / 2 by XXREAL_0:17;
abs (d - 0) = d by Q26, ABSVALUE:def 1;
then abs (d - 0) < d1 by V24, Q23, XXREAL_0:2;
then Q28: ||.((f /. d) - (f /. 0)).|| < e / 2 by Q21, Q27;
Q35: [.0,d.] c= dom g by A1, Q24, XXREAL_1:34;
Q30: g | [.0,d.] is continuous by A1, Q24, FCONT_1:16, XXREAL_1:34;
Q31: ].0,d.[ c= ].0,1.[ by Q24, XXREAL_1:46;
then consider x0 being Real such that
Q33: ( x0 in ].0,d.[ & diff (g,x0) = ((g . d) - (g . 0)) / (d - 0) ) by A1, Q26, Q35, Q30, FDIFF_1:26, ROLLE:3;
||.(diff (f,x0)).|| <= diff (g,x0) by A1, Q33, Q31;
then 0 <= (g . d) - (g . 0) by Q26, Q33;
then 0 + ||.((f /. d) - (f /. 0)).|| <= ((g . d) - (g . 0)) + (e / 2) by Q28, XREAL_1:7;
then 0 + ||.((f /. d) - (f /. 0)).|| <= (((g . d) - (g . 0)) + (e / 2)) + ((e / 2) * d) by Q26, P1, 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 Q27; :: thesis: verum
end;
then Q3: 0 < upper_bound B by Q1, SEQ_4:def 1;
now
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 Q4: upper_bound B <= 1 by Q2, SEQ_4:45;
defpred S1[ Element of NAT , Element of REAL ] means ( $2 in B & abs ((upper_bound B) - $2) <= 1 / ($1 + 1) );
WQ0: now
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
WQ3: ( r in B & (upper_bound B) - t < r ) by Q1, Q2, 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 WQ3, XREAL_1:8;
then WQ4: (upper_bound B) - r < (t + r) - r by XREAL_1:14;
r <= upper_bound B by Q1, WQ3, SEQ_4:def 1;
then 0 <= (upper_bound B) - r by XREAL_1:48;
hence S1[x,r] by WQ3, WQ4, SEQ_2:1; :: thesis: verum
end;
consider sq being Function of NAT,REAL such that
WQ1: for x being Element of NAT holds S1[x,sq . x] from FUNCT_2:sch 10(WQ0);
reconsider sq = sq as Real_Sequence ;
XX: now
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 AS: 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
U10: 1 / (p1 / 2) < n by SEQ_4:3;
(1 / (p1 / 2)) + 0 < n + 1 by U10, XREAL_1:8;
then U1: 1 / (n + 1) <= 1 / (1 / (p1 / 2)) by AS, 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 U3: 1 / (m + 1) <= p1 / 2 by U1, XXREAL_0:2;
( sq . m in B & abs ((upper_bound B) - (sq . m)) <= 1 / (m + 1) ) by WQ1;
then abs ((sq . m) - (upper_bound B)) <= 1 / (1 + m) by COMPLEX1:60;
then U4: abs ((sq . m) - (upper_bound B)) <= p1 / 2 by U3, XXREAL_0:2;
p1 / 2 < p1 by AS, XREAL_1:216;
hence abs ((sq . m) - (upper_bound B)) < p1 by U4, XXREAL_0:2; :: thesis: verum
end;
end;
then WQ2: sq is convergent by SEQ_2:def 6;
then WQ2A: lim sq = upper_bound B by XX, SEQ_2:def 7;
deffunc H1( Real) -> Element of REAL = ((||.((f /. $1) - (f /. 0)).|| - ((g . $1) - (g . 0))) - ((e / 2) * $1)) - (e / 2);
WQ3: for x being Element of REAL holds H1(x) in REAL ;
consider Lg0 being Function of REAL,REAL such that
WQ4: for x being Element of REAL holds Lg0 . x = H1(x) from FUNCT_2:sch 8(WQ3);
set Lg = Lg0 | [.0,1.];
W5: dom Lg0 = REAL by FUNCT_2:def 1;
then WQ50A: dom (Lg0 | [.0,1.]) = [.0,1.] by RELAT_1:62;
now
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 WQ1;
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 WQ50: rng sq c= dom (Lg0 | [.0,1.]) by WQ50A, TARSKI:def 3;
AQ2: upper_bound B in [.0,1.] by Q4, Q3;
now
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 AQ10: 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
AQ3: ( 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, AQ2, NFCONT_3:17;
consider t2 being real number such that
AQ4: ( 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 AQ10, AQ2, 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 P1, AQ10, XREAL_1:216;
then (e / 2) * (((r / 3) / (e / 2)) / 2) < ((r / 3) / (e / 2)) * (e / 2) by P1, XREAL_1:97;
then BQ5: (e / 2) * (((r / 3) / (e / 2)) / 2) < r / 3 by P1, 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 ) )
W2: ( min (t1,t2) <= t1 & min (t1,t2) <= t2 & 0 < min (t1,t2) ) by AQ3, AQ4, XXREAL_0:17, XXREAL_0:21;
hence 0 < t by P1, AQ10, 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
W4a: t <= ((r / 3) / (e / 2)) / 2 by XXREAL_0:17;
W4: t <= min (t1,t2) by XXREAL_0:17;
then X4: t <= t1 by W2, XXREAL_0:2;
X4a: t <= t2 by W2, W4, 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 )
V1: x1 is Element of REAL by XREAL_0:def 1;
assume that
AQ10A: x1 in dom (Lg0 | [.0,1.]) and
AQ10B: abs (x1 - (upper_bound B)) < t ; :: thesis: abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r
x1 in [.0,1.] by W5, AQ10A, RELAT_1:62;
then AQ11: (Lg0 | [.0,1.]) . x1 = Lg0 . x1 by FUNCT_1:49
.= ((||.((f /. x1) - (f /. 0)).|| - ((g . x1) - (g . 0))) - ((e / 2) * x1)) - (e / 2) by WQ4, V1 ;
(Lg0 | [.0,1.]) . (upper_bound B) = Lg0 . (upper_bound B) by AQ2, 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 WQ4;
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 AQ11;
then AQ13: 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 AQ14: 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 AQ13, XXREAL_0:2;
AQ15: 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 AQ15, 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 AQ17: 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 AQ14, XXREAL_0:2;
abs (x1 - (upper_bound B)) < t2 by AQ10B, X4a, XXREAL_0:2;
then abs ((g . x1) - (g . (upper_bound B))) < r / 3 by AQ10A, WQ50A, AQ4;
then AQ20: ||.((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 AQ10B, W4a, XXREAL_0:2;
then (abs (x1 - (upper_bound B))) * (e / 2) <= (((r / 3) / (e / 2)) / 2) * (e / 2) by P1, XREAL_1:64;
then (abs (x1 - (upper_bound B))) * (abs (e / 2)) <= (((r / 3) / (e / 2)) / 2) * (e / 2) by P1, ABSVALUE:def 1;
then abs ((e / 2) * (x1 - (upper_bound B))) <= (((r / 3) / (e / 2)) / 2) * (e / 2) by COMPLEX1:65;
then AQ19: abs ((e / 2) * (x1 - (upper_bound B))) < r / 3 by BQ5, XXREAL_0:2;
abs (x1 - (upper_bound B)) < t1 by AQ10B, X4, XXREAL_0:2;
then ||.((f /. x1) - (f /. (upper_bound B))).|| < r / 3 by AQ10A, WQ50A, AQ3;
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 AQ20, 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 AQ19, XREAL_1:8;
hence abs (((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))) < r by AQ17, XXREAL_0:2; :: thesis: verum
end;
end;
then Lg0 | [.0,1.] is_continuous_in upper_bound B by FCONT_1:3;
then WQ6: ( (Lg0 | [.0,1.]) /* sq is convergent & (Lg0 | [.0,1.]) . (upper_bound B) = lim ((Lg0 | [.0,1.]) /* sq) ) by WQ2, WQ2A, WQ50, FCONT_1:def 1;
WQ8: 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 G1: (- ((Lg0 | [.0,1.]) /* sq)) . n = - ((Lg0 | [.0,1.]) . (sq . n)) by WQ50, FUNCT_2:108;
S1[n,sq . n] by WQ1;
then XX1: 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 WQ4;
then (Lg0 | [.0,1.]) . (sq . n) <= 0 by XX1, FUNCT_1:49;
hence 0 <= (- ((Lg0 | [.0,1.]) /* sq)) . n by G1; :: thesis: verum
end;
- ((Lg0 | [.0,1.]) /* sq) is convergent by WQ6, SEQ_2:9;
then 0 <= lim (- ((Lg0 | [.0,1.]) /* sq)) by WQ8, SEQ_2:17;
then 0 <= - (lim ((Lg0 | [.0,1.]) /* sq)) by WQ6, SEQ_2:10;
then (Lg0 | [.0,1.]) . (upper_bound B) <= 0 by WQ6;
then Lg0 . (upper_bound B) <= 0 by AQ2, FUNCT_1:49;
then WQ7: ((||.((f /. (upper_bound B)) - (f /. 0)).|| - ((g . (upper_bound B)) - (g . 0))) - ((e / 2) * (upper_bound B))) - (e / 2) <= 0 by WQ4;
W5: upper_bound B = 1
proof
assume upper_bound B <> 1 ; :: thesis: contradiction
then upper_bound B < 1 by Q4, XXREAL_0:1;
then Q6: upper_bound B in ].0,1.[ by Q3;
then f is_differentiable_in upper_bound B by A1, NDIFF_3:10;
then consider N1 being Neighbourhood of upper_bound B such that
Q9: ( N1 c= dom f & ex L1 being LINEAR of T ex R1 being REST 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 LINEAR of T, R1 being REST of T such that
Q10: ( 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 Q9;
g is_differentiable_in upper_bound B by A1, Q6, FDIFF_1:9;
then consider N2 being Neighbourhood of upper_bound B such that
Q11: ( N2 c= dom g & ex L2 being LINEAR ex R2 being REST 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 LINEAR, R2 being REST such that
Q12: ( 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 Q11;
consider NN3 being Neighbourhood of upper_bound B such that
Q141: ( NN3 c= N1 & NN3 c= N2 ) by RCOMP_1:17;
consider g0 being real number such that
Q140: ( 0 < g0 & ].((upper_bound B) - g0),((upper_bound B) + g0).[ c= ].0,1.[ ) by Q6, RCOMP_1:19;
reconsider NN4 = ].((upper_bound B) - g0),((upper_bound B) + g0).[ as Neighbourhood of upper_bound B by Q140, RCOMP_1:def 6;
consider N3 being Neighbourhood of upper_bound B such that
Q143: ( N3 c= NN3 & N3 c= NN4 ) by RCOMP_1:17;
Q14: ( N3 c= N1 & N3 c= N2 & N3 c= ].0,1.[ ) by Q143, Q141, Q140, XBOOLE_1:1;
consider d1 being real number such that
Q15: ( 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 REST-like ) by NDIFF_3:def 1;
then consider d2 being Real such that
Q17: ( 0 < d2 & ( for t being Real st t <> 0 & abs t < d2 holds
||.(R1 /. t).|| / (abs t) < (e / 2) / 2 ) ) by P1, NDIFF126A;
( R2 is total & R2 is REST-like ) by FDIFF_1:def 2;
then consider d3 being Real such that
Q18: ( 0 < d3 & ( for t being Real st t <> 0 & abs t < d3 holds
(abs (R2 . t)) / (abs t) < (e / 2) / 2 ) ) by P1, NDIFF126B;
W2: ( min (d1,d2) <= d1 & min (d1,d2) <= d2 & 0 < min (d1,d2) ) by Q15, Q17, XXREAL_0:17, XXREAL_0:21;
set d40 = min ((min (d1,d2)),d3);
W3: ( min ((min (d1,d2)),d3) <= min (d1,d2) & min ((min (d1,d2)),d3) <= d3 & 0 < min ((min (d1,d2)),d3) ) by Q18, W2, XXREAL_0:17, XXREAL_0:21;
set d4 = (min ((min (d1,d2)),d3)) / 2;
W5: ( min ((min (d1,d2)),d3) <= d1 & min ((min (d1,d2)),d3) <= d2 ) by W2, W3, XXREAL_0:2;
(min ((min (d1,d2)),d3)) / 2 < min ((min (d1,d2)),d3) by W3, XREAL_1:216;
then R19: ( 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 W3, W5, 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 Q20: (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) in N3 by Q15;
then Q21: (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 Q10, Q14;
Q22: (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 Q14, Q20, Q12;
consider df1 being Point of T such that
Y1: for p being Real holds L1 . p = p * df1 by NDIFF_3:def 2;
L1 . 1 = 1 * df1 by Y1;
then L1 . 1 = df1 by RLVECT_1:def 8;
then Q23: L1 . ((min ((min (d1,d2)),d3)) / 2) = ((min ((min (d1,d2)),d3)) / 2) * (diff (f,(upper_bound B))) by Q10, Y1;
consider df2 being Real such that
Y3: for p being Real holds L2 . p = df2 * p by FDIFF_1:def 3;
L2 . 1 = df2 * 1 by Y3;
then Q24: L2 . ((min ((min (d1,d2)),d3)) / 2) = ((min ((min (d1,d2)),d3)) / 2) * (diff (g,(upper_bound B))) by Q12, Y3;
Q25: ||.((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 Q21, NORMSP_1:def 1;
Q26: ||.(L1 . ((min ((min (d1,d2)),d3)) / 2)).|| = (abs ((min ((min (d1,d2)),d3)) / 2)) * ||.(diff (f,(upper_bound B))).|| by Q23, NORMSP_1:def 1
.= ||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2) by W3, ABSVALUE:def 1 ;
X1: 0 < abs ((min ((min (d1,d2)),d3)) / 2) by W3, ABSVALUE:def 1;
abs ((min ((min (d1,d2)),d3)) / 2) < d2 by R19, ABSVALUE:def 1;
then ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| / (abs ((min ((min (d1,d2)),d3)) / 2)) < (e / 2) / 2 by Q17, W3;
then ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| <= ((e / 2) / 2) * (abs ((min ((min (d1,d2)),d3)) / 2)) by X1, XREAL_1:81;
then ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| <= ((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2) by W3, 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 Q26, XREAL_1:6;
then Q27: ||.((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 Q25, 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 Q6, A1, R19, 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 Q28: ||.((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 Q27, XXREAL_0:2;
abs ((min ((min (d1,d2)),d3)) / 2) < d3 by R19, ABSVALUE:def 1;
then (abs (R2 . ((min ((min (d1,d2)),d3)) / 2))) / (abs ((min ((min (d1,d2)),d3)) / 2)) < (e / 2) / 2 by Q18, W3;
then abs (R2 . ((min ((min (d1,d2)),d3)) / 2)) <= ((e / 2) / 2) * (abs ((min ((min (d1,d2)),d3)) / 2)) by X1, XREAL_1:81;
then abs (R2 . ((min ((min (d1,d2)),d3)) / 2)) <= ((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2) by W3, 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 Q22, Q24, 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 Q28, 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 Q45: (((||.((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 WQ7;
||.((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 Q47: ((||.((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 Q45;
abs ((0 + 1) - (2 * ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)))) < 1 - 0 by Q20, Q14, RCOMP_1:3;
then (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) in [.0,1.] by RCOMP_1:2;
then Q48: (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) in B by Q47;
(upper_bound B) + 0 < (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) by W3, XREAL_1:8;
hence contradiction by Q48, Q1, 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 W5, WQ7, 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 LMFDAF10A;
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