let G be RealNormSpace-Sequence; :: thesis: for S being RealNormSpace
for f being PartFunc of (product G),S
for x being Point of (product G) ex L being Lipschitzian LinearOperator of (product G),S st
for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & L . h = Sum w )
let S be RealNormSpace; :: thesis: for f being PartFunc of (product G),S
for x being Point of (product G) ex L being Lipschitzian LinearOperator of (product G),S st
for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & L . h = Sum w )
let f be PartFunc of (product G),S; :: thesis: for x being Point of (product G) ex L being Lipschitzian LinearOperator of (product G),S st
for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & L . h = Sum w )
let x be Point of (product G); :: thesis: ex L being Lipschitzian LinearOperator of (product G),S st
for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & L . h = Sum w )
set m = len G;
defpred S1[ set , set ] means ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . $1) ) & $2 = Sum w );
A1: for v being Element of (product G) ex y being Element of S st S1[v,y]
proof
let v be Element of (product G); :: thesis: ex y being Element of S st S1[v,y]
defpred S2[ set , set ] means ex i being Element of NAT st
( i = $1 & $2 = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . v) );
A2: for i being Nat st i in Seg (len G) holds
ex r being Element of S st S2[i,r]
proof
let i be Nat; :: thesis: ( i in Seg (len G) implies ex r being Element of S st S2[i,r] )
assume i in Seg (len G) ; :: thesis: ex r being Element of S st S2[i,r]
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
(partdiff (f,x,i0)) . ((proj (In (i0,(dom G)))) . v) in the carrier of S ;
hence ex r being Element of S st S2[i,r] ; :: thesis: verum
end;
consider w being FinSequence of S such that
A3: ( dom w = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S2[i,w . i] ) ) from FINSEQ_1:sch 5(A2);
A4: now :: thesis: for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . v)
let i be Element of NAT ; :: thesis: ( i in Seg (len G) implies w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . v) )
assume i in Seg (len G) ; :: thesis: w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . v)
then S2[i,w . i] by A3;
hence w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . v) ; :: thesis: verum
end;
reconsider w0 = Sum w as Element of S ;
ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . v) ) & w0 = Sum w ) by A4, A3;
hence ex y0 being Element of S st S1[v,y0] ; :: thesis: verum
end;
consider L being Function of (product G),S such that
A5: for h being Element of (product G) holds S1[h,L . h] from FUNCT_2:sch 3(A1);
 A6: for s, t being Element of (product G) holds L . (s + t) = (L . s) + (L . t)
proof
let s, t be Element of (product G); :: thesis: L . (s + t) = (L . s) + (L . t)
consider w being FinSequence of S such that
A7: ( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . s) ) & L . s = Sum w ) by A5;
consider v being FinSequence of S such that
A8: ( dom v = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
v . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . t) ) & L . t = Sum v ) by A5;
consider u being FinSequence of S such that
A9: ( dom u = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
u . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . (s + t)) ) & L . (s + t) = Sum u ) by A5;
A10: len w = len G by A7, FINSEQ_1:def 3;
A11: len v = len G by A8, FINSEQ_1:def 3;
A12: len u = len G by A9, FINSEQ_1:def 3;
now :: thesis: for i being Nat st i in dom w holds
u . i = (w /. i) + (v /. i)
let i be Nat; :: thesis: ( i in dom w implies u . i = (w /. i) + (v /. i) )
assume A13: i in dom w ; :: thesis: u . i = (w /. i) + (v /. i)
then A14: ( 1 <= i & i <= len G ) by A7, FINSEQ_1:1;
then w /. i = w . i by A10, FINSEQ_4:15;
then A15: w /. i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . s) by A7, A13;
v /. i = v . i by A14, A11, FINSEQ_4:15;
then A16: v /. i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . t) by A7, A8, A13;
A17: partdiff (f,x,i) is Lipschitzian LinearOperator of (G . (In (i,(dom G)))),S by LOPBAN_1:def 9;
u . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . (s + t)) by A7, A9, A13;
then u . i = (partdiff (f,x,i)) . (((proj (In (i,(dom G)))) . s) + ((proj (In (i,(dom G)))) . t)) by Th35;
hence u . i = (w /. i) + (v /. i) by A15, A16, A17, VECTSP_1:def 20; :: thesis: verum
end;
hence L . (s + t) = (L . s) + (L . t) by A9, A7, A8, A10, A11, A12, RLVECT_2:2; :: thesis: verum
end;
for s being Element of (product G)
for r being Real holds L . (r * s) = r * (L . s)
proof
let s be Element of (product G); :: thesis: for r being Real holds L . (r * s) = r * (L . s)
let r be Real; :: thesis: L . (r * s) = r * (L . s)
consider w being FinSequence of S such that
A18: ( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . s) ) & L . s = Sum w ) by A5;
consider u being FinSequence of S such that
A19: ( dom u = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
u . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . (r * s)) ) & L . (r * s) = Sum u ) by A5;
A20: ( len w = len G & len u = len G ) by A18, A19, FINSEQ_1:def 3;
now :: thesis: for i being Nat st i in dom w holds
u . i = r * (w /. i)
let i be Nat; :: thesis: ( i in dom w implies u . i = r * (w /. i) )
assume A21: i in dom w ; :: thesis: u . i = r * (w /. i)
then ( 1 <= i & i <= len G ) by A18, FINSEQ_1:1;
then w /. i = w . i by A20, FINSEQ_4:15;
then A22: w /. i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . s) by A18, A21;
A23: partdiff (f,x,i) is Lipschitzian LinearOperator of (G . (In (i,(dom G)))),S by LOPBAN_1:def 9;
u . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . (r * s)) by A18, A19, A21;
then u . i = (partdiff (f,x,i)) . (r * ((proj (In (i,(dom G)))) . s)) by Th40;
hence u . i = r * (w /. i) by A22, A23, LOPBAN_1:def 5; :: thesis: verum
end;
hence L . (r * s) = r * (L . s) by A18, A19, A20, RLVECT_2:3; :: thesis: verum
end;
then reconsider L = L as LinearOperator of (product G),S by A6, LOPBAN_1:def 5, VECTSP_1:def 20;
defpred S2[ set , set ] means ex i being Element of NAT st
( i = $1 & $2 = ||.(partdiff (f,x,i)).|| );
A24: for i being Nat st i in Seg (len G) holds
ex r being Element of REAL st S2[i,r]
proof
let i be Nat; :: thesis: ( i in Seg (len G) implies ex r being Element of REAL st S2[i,r] )
assume i in Seg (len G) ; :: thesis: ex r being Element of REAL st S2[i,r]
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
reconsider r = ||.(partdiff (f,x,i0)).|| as Element of REAL ;
S2[i,r] ;
hence ex r being Element of REAL st S2[i,r] ; :: thesis: verum
end;
consider Kw being FinSequence of REAL such that
A25: ( dom Kw = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S2[i,Kw . i] ) ) from FINSEQ_1:sch 5(A24);
A26: now :: thesis: for i being Element of NAT st i in Seg (len G) holds
Kw . i = ||.(partdiff (f,x,i)).||
let i be Element of NAT ; :: thesis: ( i in Seg (len G) implies Kw . i = ||.(partdiff (f,x,i)).|| )
assume i in Seg (len G) ; :: thesis: Kw . i = ||.(partdiff (f,x,i)).||
then S2[i,Kw . i] by A25;
hence Kw . i = ||.(partdiff (f,x,i)).|| ; :: thesis: verum
end;
A27: now :: thesis: for i being Nat st i in dom Kw holds
0 <= Kw . i
let i be Nat; :: thesis: ( i in dom Kw implies 0 <= Kw . i )
assume i in dom Kw ; :: thesis: 0 <= Kw . i
then Kw . i = ||.(partdiff (f,x,i)).|| by A26, A25;
hence 0 <= Kw . i ; :: thesis: verum
end;
set LK = Sum Kw;
for s being Element of (product G) holds ||.(L . s).|| <= (Sum Kw) * ||.s.||
proof
let s be Element of (product G); :: thesis: ||.(L . s).|| <= (Sum Kw) * ||.s.||
consider w being FinSequence of S such that
A29: ( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . s) ) & L . s = Sum w ) by A5;
defpred S3[ set , set ] means ex i being Element of NAT st
( i = $1 & $2 = ||.(partdiff (f,x,i)).|| * ||.s.|| );
A30: for i being Nat st i in Seg (len G) holds
ex r being Element of REAL st S3[i,r]
proof
let i be Nat; :: thesis: ( i in Seg (len G) implies ex r being Element of REAL st S3[i,r] )
assume i in Seg (len G) ; :: thesis: ex r being Element of REAL st S3[i,r]
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
reconsider r = ||.(partdiff (f,x,i0)).|| * ||.s.|| as Element of REAL by XREAL_0:def 1;
S3[i,r] ;
hence ex r being Element of REAL st S3[i,r] ; :: thesis: verum
end;
consider Dw being FinSequence of REAL such that
A31: ( dom Dw = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S3[i,Dw . i] ) ) from FINSEQ_1:sch 5(A30);
A32: now :: thesis: for i being Element of NAT st i in Seg (len G) holds
Dw . i = ||.(partdiff (f,x,i)).|| * ||.s.||
let i be Element of NAT ; :: thesis: ( i in Seg (len G) implies Dw . i = ||.(partdiff (f,x,i)).|| * ||.s.|| )
assume i in Seg (len G) ; :: thesis: Dw . i = ||.(partdiff (f,x,i)).|| * ||.s.||
then S3[i,Dw . i] by A31;
hence Dw . i = ||.(partdiff (f,x,i)).|| * ||.s.|| ; :: thesis: verum
end;
defpred S4[ set , set ] means ex i being Element of NAT st
( i = $1 & $2 = ||.(w /. i).|| );
A33: for i being Nat st i in Seg (len G) holds
ex r being Element of REAL st S4[i,r]
proof
let i be Nat; :: thesis: ( i in Seg (len G) implies ex r being Element of REAL st S4[i,r] )
assume i in Seg (len G) ; :: thesis: ex r being Element of REAL st S4[i,r]
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
reconsider r = ||.(w /. i0).|| as Element of REAL ;
S4[i,r] ;
hence ex r being Element of REAL st S4[i,r] ; :: thesis: verum
end;
consider yseq being FinSequence of REAL such that
A34: ( dom yseq = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S4[i,yseq . i] ) ) from FINSEQ_1:sch 5(A33);
A35: now :: thesis: for i being Element of NAT st i in Seg (len G) holds
yseq . i = ||.(w /. i).||
let i be Element of NAT ; :: thesis: ( i in Seg (len G) implies yseq . i = ||.(w /. i).|| )
assume i in Seg (len G) ; :: thesis: yseq . i = ||.(w /. i).||
then S4[i,yseq . i] by A34;
hence yseq . i = ||.(w /. i).|| ; :: thesis: verum
end;
len w = len yseq by A29, A34, FINSEQ_3:29;
then A36: ||.(L . s).|| <= Sum yseq by A29, A35, Th7;
len G = len yseq by A34, FINSEQ_1:def 3;
then A37: yseq is Element of (len G) -tuples_on REAL by FINSEQ_2:92;
len Dw = len G by A31, FINSEQ_1:def 3;
then A38: Dw is Element of (len G) -tuples_on REAL by FINSEQ_2:92;
now :: thesis: for i being Nat st i in Seg (len G) holds
yseq . i <= Dw . i
let i be Nat; :: thesis: ( i in Seg (len G) implies yseq . i <= Dw . i )
assume A39: i in Seg (len G) ; :: thesis: yseq . i <= Dw . i
then A40: yseq . i = ||.(w /. i).|| by A35;
w /. i = w . i by A39, A29, PARTFUN1:def 6;
then A41: ||.(w /. i).|| = ||.((partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . s)).|| by A29, A39;
reconsider DF1 = partdiff (f,x,i) as Lipschitzian LinearOperator of (G . (In (i,(dom G)))),S by LOPBAN_1:def 9;
A42: ||.(DF1 . ((proj (In (i,(dom G)))) . s)).|| <= ||.(partdiff (f,x,i)).|| * ||.((proj (In (i,(dom G)))) . s).|| by LOPBAN_1:32;
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
then reconsider ss = s as Element of product (carr G) ;
reconsider xi = (proj (In (i,(dom G)))) . s as Point of (G . (In (i,(dom G)))) ;
xi = ss . (In (i,(dom G))) by Def3;
then ||.(partdiff (f,x,i)).|| * ||.((proj (In (i,(dom G)))) . s).|| <= ||.(partdiff (f,x,i)).|| * ||.s.|| by PRVECT_2:10, XREAL_1:64;
then ||.(w /. i).|| <= ||.(partdiff (f,x,i)).|| * ||.s.|| by A41, A42, XXREAL_0:2;
hence yseq . i <= Dw . i by A32, A39, A40; :: thesis: verum
end;
then A43: Sum yseq <= Sum Dw by A37, A38, RVSUM_1:82;
len Kw = len G by A25, FINSEQ_1:def 3;
then reconsider KKw = Kw as Element of (len G) -tuples_on REAL by FINSEQ_2:92;
||.s.|| * KKw in (len G) -tuples_on REAL ;
then ex t being Element of REAL * st
( t = ||.s.|| * KKw & len t = len G ) ;
then A44: dom Dw = dom (||.s.|| * Kw) by A31, FINSEQ_1:def 3;
now :: thesis: for k being Nat st k in dom Dw holds
Dw . k = (||.s.|| * Kw) . k
let k be Nat; :: thesis: ( k in dom Dw implies Dw . k = (||.s.|| * Kw) . k )
assume A45: k in dom Dw ; :: thesis: Dw . k = (||.s.|| * Kw) . k
then Dw . k = ||.(partdiff (f,x,k)).|| * ||.s.|| by A32, A31;
then Dw . k = ||.s.|| * (Kw . k) by A26, A45, A31;
hence Dw . k = (||.s.|| * Kw) . k by RVSUM_1:45; :: thesis: verum
end;
then Dw = ||.s.|| * Kw by A44, FINSEQ_1:13;
then Sum Dw = (Sum Kw) * ||.s.|| by RVSUM_1:87;
hence ||.(L . s).|| <= (Sum Kw) * ||.s.|| by A36, A43, XXREAL_0:2; :: thesis: verum
end;
then reconsider L = L as Lipschitzian LinearOperator of (product G),S by A27, RVSUM_1:84, LOPBAN_1:def 8;
take L ; :: thesis: for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & L . h = Sum w )
thus for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & L . h = Sum w ) by A5; :: thesis: verum