let S, T be non trivial RealNormSpace; :: thesis: for f being PartFunc of S,T
for x0 being Point of S
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 sequence of S
for c being V8() sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let f be PartFunc of S,T; :: thesis: for x0 being Point of S
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 sequence of S
for c being V8() sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let x0 be Point of S; :: thesis: for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 sequence of S
for c being V8() sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let N be Neighbourhood of x0; :: thesis: ( f is_differentiable_in x0 & N c= dom f implies for h being convergent_to_0 sequence of S
for c being V8() sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) )
assume A1: ( f is_differentiable_in x0 & N c= dom f ) ; :: thesis: for h being convergent_to_0 sequence of S
for c being V8() sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let h be convergent_to_0 sequence of S; :: thesis: for c being V8() sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let c be V8() sequence of S; :: thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) )
assume A2: ( rng c = {x0} & rng (h + c) c= N ) ; :: thesis: ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
consider N1 being Neighbourhood of x0 such that
A3: ( N1 c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,T) ex R being REST of S,T st
for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by A1, Def6;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators S,T), R being REST of S,T such that
A4: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3;
consider N2 being Neighbourhood of x0 such that
A5: ( N2 c= N & N2 c= N1 ) by Th1;
consider g being Real such that
A6: ( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= N2 ) by NFCONT_1:def 3;
A7: x0 in N2 by NFCONT_1:4;
ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
proof
A8: c is convergent by Th21;
c . 0 in rng c by NFCONT_1:6;
then c . 0 = x0 by A2, TARSKI:def 1;
then A9: lim c = x0 by Th21;
A10: ( h is convergent & lim h = 0. S ) by Def4;
then A11: lim (h + c) = (0. S) + x0 by A8, A9, NORMSP_1:42
.= x0 by RLVECT_1:10 ;
h + c is convergent by A8, A10, NORMSP_1:34;
then consider n being Element of NAT such that
A12: for m being Element of NAT st n <= m holds
||.(((h + c) . m) - x0).|| < g by A6, A11, NORMSP_1:def 11;
A13: rng (c ^\ n) = {x0} by A2, VALUED_0:26;
take n ; :: thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
thus rng (c ^\ n) c= N2 :: thesis: rng ((h + c) ^\ n) c= N2
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in N2 )
assume y in rng (c ^\ n) ; :: thesis: y in N2
hence y in N2 by A7, A13, TARSKI:def 1; :: thesis: verum
end;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )
assume y in rng ((h + c) ^\ n) ; :: thesis: y in N2
then consider m being Element of NAT such that
A14: y = ((h + c) ^\ n) . m by NFCONT_1:6;
0 <= m by NAT_1:2;
then n + 0 <= n + m by XREAL_1:9;
then ||.(((h + c) . (n + m)) - x0).|| < g by A12;
then A15: ||.((((h + c) ^\ n) . m) - x0).|| < g by NAT_1:def 3;
reconsider y1 = y as Point of S by A14;
y1 in { z where z is Point of S : ||.(z - x0).|| < g } by A14, A15;
hence y in N2 by A6; :: thesis: verum
end;
then consider n being Element of NAT such that
A16: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) ;
A17: rng (c ^\ n) c= dom f
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in dom f )
A18: rng (c ^\ n) = rng c by VALUED_0:26;
assume y in rng (c ^\ n) ; :: thesis: y in dom f
then y = x0 by A2, A18, TARSKI:def 1;
then y in N by NFCONT_1:4;
hence y in dom f by A1; :: thesis: verum
end;
A19: rng ((h + c) ^\ n) c= dom f
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in dom f )
assume y in rng ((h + c) ^\ n) ; :: thesis: y in dom f
then y in N2 by A16;
then y in N by A5;
hence y in dom f by A1; :: thesis: verum
end;
A20: rng c c= dom f
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in dom f )
assume y in rng c ; :: thesis: y in dom f
then y = x0 by A2, TARSKI:def 1;
then y in N by NFCONT_1:4;
hence y in dom f by A1; :: thesis: verum
end;
A21: rng (h + c) c= dom f
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (h + c) or y in dom f )
assume y in rng (h + c) ; :: thesis: y in dom f
then y in N by A2;
hence y in dom f by A1; :: thesis: verum
end;
A22: for k being Element of NAT holds (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
proof
let k be Element of NAT ; :: thesis: (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
((h + c) ^\ n) . k in rng ((h + c) ^\ n) by NFCONT_1:6;
then A23: ((h + c) ^\ n) . k in N2 by A16;
A24: (((h + c) ^\ n) . k) - ((c ^\ n) . k) = ((h + c) . (k + n)) - ((c ^\ n) . k) by NAT_1:def 3
.= ((h . (k + n)) + (c . (k + n))) - ((c ^\ n) . k) by NORMSP_1:def 5
.= (((h ^\ n) . k) + (c . (k + n))) - ((c ^\ n) . k) by NAT_1:def 3
.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by NAT_1:def 3
.= ((h ^\ n) . k) + (((c ^\ n) . k) - ((c ^\ n) . k)) by RLVECT_1:def 6
.= ((h ^\ n) . k) + (0. S) by RLVECT_1:28
.= (h ^\ n) . k by RLVECT_1:10 ;
A25: (c ^\ n) . k in rng (c ^\ n) by NFCONT_1:6;
rng (c ^\ n) = rng c by VALUED_0:26;
then (c ^\ n) . k = x0 by A2, A25, TARSKI:def 1;
hence (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A4, A5, A23, A24; :: thesis: verum
end;
R_NormSpace_of_BoundedLinearOperators S,T = NORMSTR(# (BoundedLinearOperators S,T),(Zero_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(Add_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(Mult_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(BoundedLinearOperatorsNorm S,T) #) by LOPBAN_1:def 15;
then reconsider L = L as Element of BoundedLinearOperators S,T ;
A26: dom (modetrans L,S,T) = the carrier of S by FUNCT_2:def 1;
then A27: rng (h ^\ n) c= dom (modetrans L,S,T) ;
R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def 4;
then A28: rng (h ^\ n) c= dom R ;
reconsider LP = modetrans L,S,T as PartFunc of S,T ;
A29: (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (LP /* (h ^\ n)) + (R /* (h ^\ n))
proof
now
let k be Element of NAT ; :: thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k
thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by NORMSP_1:def 6
.= (f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A19, FUNCT_2:186
.= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A17, FUNCT_2:186
.= (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A22
.= ((modetrans L,S,T) . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by LOPBAN_1:def 12
.= (LP /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A26, PARTFUN1:def 8
.= ((LP /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by A27, FUNCT_2:186
.= ((LP /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A28, FUNCT_2:186
.= ((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k by NORMSP_1:def 5 ; :: thesis: verum
end;
hence (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (LP /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:113; :: thesis: verum
end;
A30: ( R /* (h ^\ n) is convergent & lim (R /* (h ^\ n)) = 0. T ) by Th27;
A31: dom (modetrans L,S,T) = the carrier of S by FUNCT_2:def 1;
then A32: LP /. (0. S) = (modetrans L,S,T) . (0. S) by PARTFUN1:def 8
.= (modetrans L,S,T) . (0 * (0. S)) by RLVECT_1:23
.= 0 * ((modetrans L,S,T) . (0. S)) by LOPBAN_1:def 6
.= 0. T by RLVECT_1:23 ;
LP is_Lipschitzian_on the carrier of S
proof
set LL = modetrans L,S,T;
thus the carrier of S c= dom LP by FUNCT_2:def 1; :: according to NFCONT_1:def 13 :: thesis: ex b1 being Element of REAL st
( not b1 <= 0 & ( for b2, b3 being Element of the carrier of S holds
( not b2 in the carrier of S or not b3 in the carrier of S or ||.((LP /. b2) - (LP /. b3)).|| <= b1 * ||.(b2 - b3).|| ) ) )
consider K being Real such that
A33: ( 0 <= K & ( for x being VECTOR of S holds ||.((modetrans L,S,T) . x).|| <= K * ||.x.|| ) ) by LOPBAN_1:def 9;
A34: 0 + K < 1 + K by XREAL_1:10;
A35: 0 + 0 < 1 + K by A33;
take K + 1 ; :: thesis: ( not K + 1 <= 0 & ( for b1, b2 being Element of the carrier of S holds
( not b1 in the carrier of S or not b2 in the carrier of S or ||.((LP /. b1) - (LP /. b2)).|| <= (K + 1) * ||.(b1 - b2).|| ) ) )
now
let x1, x2 be Point of S; :: thesis: ( x1 in the carrier of S & x2 in the carrier of S implies ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| )
assume ( x1 in the carrier of S & x2 in the carrier of S ) ; :: thesis: ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).||
A36: ||.((modetrans L,S,T) . (x1 - x2)).|| <= K * ||.(x1 - x2).|| by A33;
0 <= ||.(x1 - x2).|| by NORMSP_1:8;
then A37: K * ||.(x1 - x2).|| <= (K + 1) * ||.(x1 - x2).|| by A34, XREAL_1:66;
||.((LP /. x1) - (LP /. x2)).|| = ||.(((modetrans L,S,T) . x1) - (LP /. x2)).|| by A31, PARTFUN1:def 8
.= ||.(((modetrans L,S,T) . x1) + (- ((modetrans L,S,T) . x2))).|| by A31, PARTFUN1:def 8
.= ||.(((modetrans L,S,T) . x1) + ((- 1) * ((modetrans L,S,T) . x2))).|| by RLVECT_1:29
.= ||.(((modetrans L,S,T) . x1) + ((modetrans L,S,T) . ((- 1) * x2))).|| by LOPBAN_1:def 6
.= ||.((modetrans L,S,T) . (x1 + ((- 1) * x2))).|| by LOPBAN_1:def 5
.= ||.((modetrans L,S,T) . (x1 - x2)).|| by RLVECT_1:29 ;
hence ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| by A36, A37, XXREAL_0:2; :: thesis: verum
end;
hence ( not K + 1 <= 0 & ( for b1, b2 being Element of the carrier of S holds
( not b1 in the carrier of S or not b2 in the carrier of S or ||.((LP /. b1) - (LP /. b2)).|| <= (K + 1) * ||.(b1 - b2).|| ) ) ) by A35; :: thesis: verum
end;
then A38: LP is_continuous_on the carrier of S by NFCONT_1:52;
( h ^\ n is convergent & rng (h ^\ n) c= the carrier of S & lim (h ^\ n) = 0. S ) by Def4;
then ( LP /* (h ^\ n) is convergent & lim (LP /* (h ^\ n)) = 0. T ) by A32, A38, NFCONT_1:25;
then ( (LP /* (h ^\ n)) + (R /* (h ^\ n)) is convergent & lim ((LP /* (h ^\ n)) + (R /* (h ^\ n))) = (0. T) + (0. T) ) by A30, NORMSP_1:34, NORMSP_1:42;
then A39: ( (LP /* (h ^\ n)) + (R /* (h ^\ n)) is convergent & lim ((LP /* (h ^\ n)) + (R /* (h ^\ n))) = 0. T ) by RLVECT_1:10;
(f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = ((f /* (h + c)) ^\ n) - (f /* (c ^\ n)) by A21, VALUED_0:27
.= ((f /* (h + c)) ^\ n) - ((f /* c) ^\ n) by A20, VALUED_0:27
.= ((f /* (h + c)) - (f /* c)) ^\ n by Th16 ;
hence ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) by A29, A39, LOPBAN_3:15, LOPBAN_3:16; :: thesis: verum