let S, T be RealNormSpace; for f being PartFunc of S,T
for p, q being Point of S
for M being Real
for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) 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)) - L).|| <= M ) holds
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
let f be PartFunc of S,T; for p, q being Point of S
for M being Real
for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) 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)) - L).|| <= M ) holds
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
let p, q be Point of S; for M being Real
for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) 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)) - L).|| <= M ) holds
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
let M be Real; for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) 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)) - L).|| <= M ) holds
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
let L be Point of (R_NormSpace_of_BoundedLinearOperators (S,T)); ( [.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)) - L).|| <= M ) implies ||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).|| )
assume that
A1:
[.p,q.] c= dom f
and
A2:
( ( 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)) - L).|| <= M ) )
; ||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
reconsider LP = L as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;
deffunc H1( Point of S) -> Element of the carrier of T = L . ($1 - p);
consider L0 being Function of the carrier of S, the carrier of T such that
A3:
for t being Element of the carrier of S holds L0 . t = H1(t)
from FUNCT_2:sch 4();
A4:
dom L0 = the carrier of S
by FUNCT_2:def 1;
then A6:
L0 is_continuous_on dom L0
by NFCONT_1:45, NFCONT_1:def 9;
reconsider R = the carrier of S --> (0. T) as PartFunc of S,T ;
A7:
dom R = the carrier of S
;
then reconsider R = R as RestFunc of S,T by NDIFF_1:def 5;
set g = f - L0;
A16: dom (f - L0) =
(dom f) /\ (dom L0)
by VFUNCT_1:def 2
.=
dom f
by A4, XBOOLE_1:28
;
A17:
for x being Point of S st x in dom (f - L0) holds
(f - L0) /. x = (f /. x) - (L . (x - p))
A18:
for x being Point of S st x in [.p,q.] holds
f - L0 is_continuous_in x
A20:
for x being Point of S st x in ].p,q.[ holds
f - L0 is_differentiable_in x
for x being Point of S st x in ].p,q.[ holds
||.(diff ((f - L0),x)).|| <= M
proof
let x be
Point of
S;
( x in ].p,q.[ implies ||.(diff ((f - L0),x)).|| <= M )
assume A21:
x in ].p,q.[
;
||.(diff ((f - L0),x)).|| <= M
then A22:
f is_differentiable_in x
by A2;
(
L0 is_differentiable_in x &
diff (
L0,
x)
= L )
by A13;
then
diff (
(f - L0),
x)
= (diff (f,x)) - L
by A22, NDIFF_1:36;
hence
||.(diff ((f - L0),x)).|| <= M
by A2, A21;
verum
end;
then A23:
||.(((f - L0) /. q) - ((f - L0) /. p)).|| <= M * ||.(q - p).||
by Th19, A1, A16, A18, A20;
p in [.p,q.]
by RLTOPSP1:68;
then
(f - L0) /. p = (f /. p) - (L . (p - p))
by A1, A16, A17;
then A24: (f - L0) /. p =
(f /. p) - (LP . (0. S))
by RLVECT_1:15
.=
(f /. p) - (LP . (0 * p))
by RLVECT_1:10
.=
(f /. p) - (0 * (LP . p))
by LOPBAN_1:def 5
.=
(f /. p) - (0. T)
by RLVECT_1:10
.=
f /. p
by RLVECT_1:13
;
q in [.p,q.]
by RLTOPSP1:68;
then
(f - L0) /. q = (f /. q) - (L . (q - p))
by A1, A16, A17;
then
(f /. q) - ((L . (q - p)) + (f /. p)) = ((f - L0) /. q) - ((f - L0) /. p)
by A24, RLVECT_1:27;
hence
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
by A23, RLVECT_1:27; verum