let S, T be non trivial RealNormSpace; :: thesis: for f being PartFunc of S,T
for p, q being Point of S
for M being Real st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) holds
||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||
let f be PartFunc of S,T; :: thesis: for p, q being Point of S
for M being Real st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) holds
||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||
let p, q be Point of S; :: thesis: for M being Real st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) holds
||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||
let M be Real; :: thesis: ( [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) implies ||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).|| )
assume A1: ( [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) ) ; :: thesis: ||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||
deffunc H1( Element of REAL ) -> Element of the carrier of S = ($1 * (q - p)) + p;
consider pt0 being Function of REAL, the carrier of S such that
A2: for t being Element of REAL holds pt0 . t = H1(t) from FUNCT_2:sch 4();
 set pt = pt0 | [.0,1.];
A3: dom pt0 = REAL by FUNCT_2:def 1;
then A4: dom (pt0 | [.0,1.]) = [.0,1.] by RELAT_1:62;
now :: thesis: for t being real number st t in [.0,1.] holds
pt0 /. t = (t * (q - p)) + p
let t be real number ; :: thesis: ( t in [.0,1.] implies pt0 /. t = (t * (q - p)) + p )
assume t in [.0,1.] ; :: thesis: pt0 /. t = (t * (q - p)) + p
A5: t is Element of REAL by XREAL_0:def 1;
then pt0 /. t = pt0 . t by A3, PARTFUN1:def 6;
hence pt0 /. t = (t * (q - p)) + p by A2, A5; :: thesis: verum
end;
then A6: pt0 | [.0,1.] is continuous by NFCONT_3:33;
A7: ].0,1.[ c= [.0,1.] by XXREAL_1:25;
A8: now :: thesis: for t being Real st t in ].0,1.[ holds
(pt0 | [.0,1.]) /. t = (t * (q - p)) + p
let t be Real; :: thesis: ( t in ].0,1.[ implies (pt0 | [.0,1.]) /. t = (t * (q - p)) + p )
assume t in ].0,1.[ ; :: thesis: (pt0 | [.0,1.]) /. t = (t * (q - p)) + p
hence (pt0 | [.0,1.]) /. t = pt0 /. t by A4, A7, PARTFUN2:15
.= (t * (q - p)) + p by A2 ;
:: thesis: verum
end;
then A9: ( pt0 | [.0,1.] is_differentiable_on ].0,1.[ & ( for t being Real st t in ].0,1.[ holds
((pt0 | [.0,1.]) `| ].0,1.[) . t = q - p ) ) by A4, A7, NDIFF_3:21;
reconsider phi = f * (pt0 | [.0,1.]) as PartFunc of REAL,T ;
A10: rng (pt0 | [.0,1.]) c= [.p,q.]
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (pt0 | [.0,1.]) or y in [.p,q.] )
assume y in rng (pt0 | [.0,1.]) ; :: thesis: y in [.p,q.]
then consider x being set such that
A11: ( x in dom (pt0 | [.0,1.]) & y = (pt0 | [.0,1.]) . x ) by FUNCT_1:def 3;
A12: y = pt0 . x by A11, FUNCT_1:47;
reconsider x = x as Element of REAL by A11;
consider r being Real such that
A13: ( x = r & 0 <= r & r <= 1 ) by A11, A4;
y = p + (x * (q - p)) by A2, A12
.= ((1 - x) * p) + (x * q) by Lm2 ;
then y in { (((1 - r1) * p) + (r1 * q)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by A13;
hence y in [.p,q.] by RLTOPSP1:def 2; :: thesis: verum
end;
then rng (pt0 | [.0,1.]) c= dom f by A1, XBOOLE_1:1;
then A14: dom phi = [.0,1.] by A4, RELAT_1:27;
A15: for t being real number st t in [.0,1.] holds
phi /. t = f /. (p + (t * (q - p)))
proof
let t be real number ; :: thesis: ( t in [.0,1.] implies phi /. t = f /. (p + (t * (q - p))) )
assume A16: t in [.0,1.] ; :: thesis: phi /. t = f /. (p + (t * (q - p)))
then A17: phi /. t = phi . t by A14, PARTFUN1:def 6
.= f . ((pt0 | [.0,1.]) . t) by A16, A14, FUNCT_1:12 ;
(pt0 | [.0,1.]) . t in rng (pt0 | [.0,1.]) by A16, A4, FUNCT_1:def 3;
then A18: (pt0 | [.0,1.]) . t in [.p,q.] by A10;
(pt0 | [.0,1.]) . t = pt0 . t by A16, A4, FUNCT_1:47
.= p + (t * (q - p)) by A2, A16 ;
hence phi /. t = f /. (p + (t * (q - p))) by A17, A18, A1, PARTFUN1:def 6; :: thesis: verum
end;
now :: thesis: for x0 being real number st x0 in dom phi holds
phi is_continuous_in x0
let x0 be real number ; :: thesis: ( x0 in dom phi implies phi is_continuous_in x0 )
assume A19: x0 in dom phi ; :: thesis: phi is_continuous_in x0
then A20: pt0 | [.0,1.] is_continuous_in x0 by A4, A6, A14, NFCONT_3:def 2;
(pt0 | [.0,1.]) . x0 in rng (pt0 | [.0,1.]) by A4, A19, A14, FUNCT_1:def 3;
then (pt0 | [.0,1.]) . x0 in [.p,q.] by A10;
then (pt0 | [.0,1.]) /. x0 in [.p,q.] by A19, A14, A4, PARTFUN1:def 6;
hence phi is_continuous_in x0 by A1, A19, A20, NFCONT_3:15; :: thesis: verum
end;
then phi is continuous by NFCONT_3:def 2;
then A21: phi | [.0,1.] is continuous ;
A22: now :: thesis: for x being Real st x in ].0,1.[ holds
( phi is_differentiable_in x & diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p) )
let x be Real; :: thesis: ( x in ].0,1.[ implies ( phi is_differentiable_in x & diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p) ) )
assume A23: x in ].0,1.[ ; :: thesis: ( phi is_differentiable_in x & diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p) )
then A24: pt0 | [.0,1.] is_differentiable_in x by A9, NDIFF_3:10;
((pt0 | [.0,1.]) `| ].0,1.[) . x = q - p by A23, A8, A4, A7, NDIFF_3:21;
then A25: diff ((pt0 | [.0,1.]),x) = q - p by A9, A23, NDIFF_3:def 6;
A26: (pt0 | [.0,1.]) . x = (pt0 | [.0,1.]) /. x by A23, A7, A4, PARTFUN1:def 6;
A27: ex r being Real st
( x = r & 0 < r & r < 1 ) by A23;
A28: (pt0 | [.0,1.]) . x = pt0 . x by A23, A7, A4, FUNCT_1:47;
A29: pt0 . x = p + (x * (q - p)) by A2;
then (pt0 | [.0,1.]) . x in ].p,q.[ by A27, A28;
then A30: f is_differentiable_in (pt0 | [.0,1.]) /. x by A26, A1;
hence phi is_differentiable_in x by A24, Th6; :: thesis: diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p)
thus diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p) by A25, A26, A28, A29, A30, A24, Th6; :: thesis: verum
end;
then ( ].0,1.[ c= dom phi & ( for x being Real st x in ].0,1.[ holds
phi is_differentiable_in x ) ) by A14, XXREAL_1:25;
then A31: phi is_differentiable_on ].0,1.[ by NDIFF_3:10;
deffunc H2( Element of REAL ) -> Element of REAL = (M * ||.(q - p).||) * $1;
consider g0 being Function of REAL,REAL such that
A32: for t being Element of REAL holds g0 . t = H2(t) from FUNCT_2:sch 4();
 set g = g0 | [.0,1.];
for t being real number st t in [.0,1.] holds
g0 . t = ((M * ||.(q - p).||) * t) + 0 by A32;
then A33: g0 | [.0,1.] is continuous by FCONT_1:41;
dom g0 = REAL by FUNCT_2:def 1;
then A34: dom (g0 | [.0,1.]) = [.0,1.] by RELAT_1:62;
A35: (g0 | [.0,1.]) | [.0,1.] is continuous by A33;
A36: now :: thesis: for t being Real st t in ].0,1.[ holds
(g0 | [.0,1.]) . t = ((M * ||.(q - p).||) * t) + 0
let t be Real; :: thesis: ( t in ].0,1.[ implies (g0 | [.0,1.]) . t = ((M * ||.(q - p).||) * t) + 0 )
assume t in ].0,1.[ ; :: thesis: (g0 | [.0,1.]) . t = ((M * ||.(q - p).||) * t) + 0
hence (g0 | [.0,1.]) . t = g0 . t by A34, A7, FUNCT_1:47
.= ((M * ||.(q - p).||) * t) + 0 by A32 ;
:: thesis: verum
end;
then A37: ( g0 | [.0,1.] is_differentiable_on ].0,1.[ & ( for t being Real st t in ].0,1.[ holds
((g0 | [.0,1.]) `| ].0,1.[) . t = M * ||.(q - p).|| ) ) by A34, A7, FDIFF_1:23;
for t being real number st t in ].0,1.[ holds
||.(diff (phi,t)).|| <= diff ((g0 | [.0,1.]),t)
proof
let t be real number ; :: thesis: ( t in ].0,1.[ implies ||.(diff (phi,t)).|| <= diff ((g0 | [.0,1.]),t) )
assume A38: t in ].0,1.[ ; :: thesis: ||.(diff (phi,t)).|| <= diff ((g0 | [.0,1.]),t)
then A39: ||.(diff (phi,t)).|| = ||.((diff (f,(p + (t * (q - p))))) . (q - p)).|| by A22;
reconsider L = diff (f,(p + (t * (q - p)))) as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;
A40: ||.(L . (q - p)).|| <= ||.(diff (f,(p + (t * (q - p))))).|| * ||.(q - p).|| by LOPBAN_1:32;
ex r being Real st
( t = r & 0 < r & r < 1 ) by A38;
then p + (t * (q - p)) in ].p,q.[ ;
then A41: ||.(diff (f,(p + (t * (q - p))))).|| * ||.(q - p).|| <= M * ||.(q - p).|| by A1, XREAL_1:64;
diff ((g0 | [.0,1.]),t) = ((g0 | [.0,1.]) `| ].0,1.[) . t by A38, A37, FDIFF_1:def 7;
then diff ((g0 | [.0,1.]),t) = M * ||.(q - p).|| by A38, A36, A34, A7, FDIFF_1:23;
hence ||.(diff (phi,t)).|| <= diff ((g0 | [.0,1.]),t) by A41, A40, A39, XXREAL_0:2; :: thesis: verum
end;
then A42: ||.((phi /. 1) - (phi /. 0)).|| <= ((g0 | [.0,1.]) /. 1) - ((g0 | [.0,1.]) /. 0) by Lm4, A14, A21, A31, A34, A35, A37;
A43: ( 1 in [.0,1.] & 0 in [.0,1.] ) ;
then A44: (g0 | [.0,1.]) /. 1 = (g0 | [.0,1.]) . 1 by A34, PARTFUN1:def 6
.= g0 . 1 by A34, A43, FUNCT_1:47
.= (M * ||.(q - p).||) * 1 by A32 ;
A45: (g0 | [.0,1.]) /. 0 = (g0 | [.0,1.]) . 0 by A34, A43, PARTFUN1:def 6
.= g0 . 0 by A34, A43, FUNCT_1:47
.= (M * ||.(q - p).||) * 0 by A32 ;
A46: phi /. 1 = f /. (p + (1 * (q - p))) by A15, A43
.= f /. (p + (q - p)) by RLVECT_1:def 8
.= f /. (q - (p - p)) by RLVECT_1:29
.= f /. (q - (0. S)) by RLVECT_1:15
.= f /. q by RLVECT_1:13 ;
phi /. 0 = f /. (p + (0 * (q - p))) by A15, A43
.= f /. (p + (0. S)) by RLVECT_1:10
.= f /. p by RLVECT_1:4 ;
hence ||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).|| by A42, A44, A45, A46; :: thesis: verum