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 AS1: ( [.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
D0: for t being Element of REAL holds pt0 . t = H1(t) from FUNCT_2:sch 4();
 set pt = pt0 | [.0,1.];
D1: dom pt0 = REAL by FUNCT_2:def 1;
then D3: dom (pt0 | [.0,1.]) = [.0,1.] by RELAT_1:62;
now
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
D11: t is Element of REAL by XREAL_0:def 1;
then pt0 /. t = pt0 . t by D1, PARTFUN1:def 6;
hence pt0 /. t = (t * (q - p)) + p by D0, D11; :: thesis: verum
end;
then D2: pt0 | [.0,1.] is continuous by NFCONT_3:33;
D4: ].0,1.[ c= [.0,1.] by XXREAL_1:25;
D5: now
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 D3, D4, PARTFUN2:15
.= (t * (q - p)) + p by D0 ;
:: thesis: verum
end;
then D6: ( 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 D3, D4, NDIFF_3:21;
reconsider phi = f * (pt0 | [.0,1.]) as PartFunc of REAL,T ;
D7: 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
X1: ( x in dom (pt0 | [.0,1.]) & y = (pt0 | [.0,1.]) . x ) by FUNCT_1:def 3;
X2: y = pt0 . x by X1, FUNCT_1:47;
reconsider x = x as Element of REAL by X1;
consider r being Real such that
X3: ( x = r & 0 <= r & r <= 1 ) by X1, D3;
y = p + (x * (q - p)) by D0, X2
.= ((1 - x) * p) + (x * q) by LmX ;
then y in { (((1 - r1) * p) + (r1 * q)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by X3;
hence y in [.p,q.] by RLTOPSP1:def 2; :: thesis: verum
end;
then rng (pt0 | [.0,1.]) c= dom f by AS1, XBOOLE_1:1;
then P1A: dom phi = [.0,1.] by D3, RELAT_1:27;
P1B: 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 X1: t in [.0,1.] ; :: thesis: phi /. t = f /. (p + (t * (q - p)))
then X2: phi /. t = phi . t by P1A, PARTFUN1:def 6
.= f . ((pt0 | [.0,1.]) . t) by X1, P1A, FUNCT_1:12 ;
(pt0 | [.0,1.]) . t in rng (pt0 | [.0,1.]) by X1, D3, FUNCT_1:def 3;
then X3: (pt0 | [.0,1.]) . t in [.p,q.] by D7;
(pt0 | [.0,1.]) . t = pt0 . t by X1, D3, FUNCT_1:47
.= p + (t * (q - p)) by D0, X1 ;
hence phi /. t = f /. (p + (t * (q - p))) by X2, X3, AS1, PARTFUN1:def 6; :: thesis: verum
end;
now
let x0 be real number ; :: thesis: ( x0 in dom phi implies phi is_continuous_in x0 )
assume X1: x0 in dom phi ; :: thesis: phi is_continuous_in x0
then X3: pt0 | [.0,1.] is_continuous_in x0 by D3, D2, P1A, NFCONT_3:def 2;
(pt0 | [.0,1.]) . x0 in rng (pt0 | [.0,1.]) by D3, X1, P1A, FUNCT_1:def 3;
then (pt0 | [.0,1.]) . x0 in [.p,q.] by D7;
then (pt0 | [.0,1.]) /. x0 in [.p,q.] by X1, P1A, D3, PARTFUN1:def 6;
hence phi is_continuous_in x0 by AS1, X1, X3, NFCONT_3:15; :: thesis: verum
end;
then phi is continuous by NFCONT_3:def 2;
then P2: phi | [.0,1.] is continuous ;
P40: now
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 X1: x in ].0,1.[ ; :: thesis: ( phi is_differentiable_in x & diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p) )
then X2: pt0 | [.0,1.] is_differentiable_in x by D6, NDIFF_3:10;
((pt0 | [.0,1.]) `| ].0,1.[) . x = q - p by X1, D5, D3, D4, NDIFF_3:21;
then X3: diff ((pt0 | [.0,1.]),x) = q - p by D6, X1, NDIFF_3:def 6;
X5: (pt0 | [.0,1.]) . x = (pt0 | [.0,1.]) /. x by X1, D4, D3, PARTFUN1:def 6;
Y3: ex r being Real st
( x = r & 0 < r & r < 1 ) by X1;
Y4: (pt0 | [.0,1.]) . x = pt0 . x by X1, D4, D3, FUNCT_1:47;
Y5: pt0 . x = p + (x * (q - p)) by D0;
then (pt0 | [.0,1.]) . x in ].p,q.[ by Y3, Y4;
then X6: f is_differentiable_in (pt0 | [.0,1.]) /. x by X5, AS1;
hence phi is_differentiable_in x by X2, NDIFF213; :: 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 X3, X5, Y4, Y5, X6, X2, NDIFF213; :: 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 P1A, XXREAL_1:25;
then P3: 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
Q0: 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 Q0;
then Q9: g0 | [.0,1.] is continuous by FCONT_1:41;
dom g0 = REAL by FUNCT_2:def 1;
then Q3: dom (g0 | [.0,1.]) = [.0,1.] by RELAT_1:62;
then Q2: (g0 | [.0,1.]) | [.0,1.] is continuous by Q9, RELAT_1:68;
Q5: now
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 Q3, D4, FUNCT_1:47
.= ((M * ||.(q - p).||) * t) + 0 by Q0 ;
:: thesis: verum
end;
then Q6: ( 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 Q3, D4, 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 X1: t in ].0,1.[ ; :: thesis: ||.(diff (phi,t)).|| <= diff ((g0 | [.0,1.]),t)
then X2: ||.(diff (phi,t)).|| = ||.((diff (f,(p + (t * (q - p))))) . (q - p)).|| by P40;
reconsider L = diff (f,(p + (t * (q - p)))) as bounded LinearOperator of S,T by LOPBAN_1:def 9;
X3: ||.(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 X1;
then p + (t * (q - p)) in ].p,q.[ ;
then Y3: ||.(diff (f,(p + (t * (q - p))))).|| * ||.(q - p).|| <= M * ||.(q - p).|| by AS1, XREAL_1:64;
diff ((g0 | [.0,1.]),t) = ((g0 | [.0,1.]) `| ].0,1.[) . t by X1, Q6, FDIFF_1:def 7;
then diff ((g0 | [.0,1.]),t) = M * ||.(q - p).|| by X1, Q5, Q3, D4, FDIFF_1:23;
hence ||.(diff (phi,t)).|| <= diff ((g0 | [.0,1.]),t) by Y3, X3, X2, XXREAL_0:2; :: thesis: verum
end;
then R2: ||.((phi /. 1) - (phi /. 0)).|| <= ((g0 | [.0,1.]) /. 1) - ((g0 | [.0,1.]) /. 0) by LMFDAF10, P1A, P2, P3, Q3, Q2, Q6;
R31: ( 1 in [.0,1.] & 0 in [.0,1.] ) ;
then R3: (g0 | [.0,1.]) /. 1 = (g0 | [.0,1.]) . 1 by Q3, PARTFUN1:def 6
.= g0 . 1 by Q3, R31, FUNCT_1:47
.= (M * ||.(q - p).||) * 1 by Q0 ;
R4: (g0 | [.0,1.]) /. 0 = (g0 | [.0,1.]) . 0 by Q3, R31, PARTFUN1:def 6
.= g0 . 0 by Q3, R31, FUNCT_1:47
.= (M * ||.(q - p).||) * 0 by Q0 ;
R5: phi /. 1 = f /. (p + (1 * (q - p))) by P1B, R31
.= 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 P1B, R31
.= f /. (p + (0. S)) by RLVECT_1:10
.= f /. p by RLVECT_1:4 ;
hence ||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).|| by R2, R3, R4, R5; :: thesis: verum