let m, n be non zero Nat; for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m ex L being Lipschitzian LinearOperator of m,n st
for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
let f be PartFunc of (REAL m),(REAL n); for x being Element of REAL m ex L being Lipschitzian LinearOperator of m,n st
for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
let x be Element of REAL m; ex L being Lipschitzian LinearOperator of m,n st
for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
defpred S1[ set , set ] means ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . $1) * (partdiff (f,x,i)) ) & $2 = Sum w );
A1:
for v being Element of REAL m ex y being Element of REAL n st S1[v,y]
proof
let v be
Element of
REAL m;
ex y being Element of REAL n st S1[v,y]
defpred S2[
set ,
set ]
means ex
i being
Nat st
(
i = $1 & $2
= ((proj (i,m)) . v) * (partdiff (f,x,i)) );
A2:
for
i being
Nat st
i in Seg m holds
ex
r being
Element of
REAL n st
S2[
i,
r]
consider w being
FinSequence of
REAL n such that A3:
(
dom w = Seg m & ( for
i being
Nat st
i in Seg m holds
S2[
i,
w . i] ) )
from FINSEQ_1:sch 5(A2);
A4:
now for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . v) * (partdiff (f,x,i))let i be
Nat;
( i in Seg m implies w . i = ((proj (i,m)) . v) * (partdiff (f,x,i)) )assume
i in Seg m
;
w . i = ((proj (i,m)) . v) * (partdiff (f,x,i))then
S2[
i,
w . i]
by A3;
hence
w . i = ((proj (i,m)) . v) * (partdiff (f,x,i))
;
verum end;
reconsider w0 =
Sum w as
Element of
REAL n ;
ex
w being
FinSequence of
REAL n st
(
dom w = Seg m & ( for
i being
Nat st
i in Seg m holds
w . i = ((proj (i,m)) . v) * (partdiff (f,x,i)) ) &
w0 = Sum w )
by A4, A3;
hence
ex
y0 being
Element of
REAL n st
S1[
v,
y0]
;
verum
end;
consider L being Function of (REAL m),(REAL n) such that
A5:
for h being Element of REAL m holds S1[h,L . h]
from FUNCT_2:sch 3(A1);
A6:
for s, t being Element of REAL m holds L . (s + t) = (L . s) + (L . t)
proof
let s,
t be
Element of
REAL m;
L . (s + t) = (L . s) + (L . t)
consider w being
FinSequence of
REAL n such that A7:
(
dom w = Seg m & ( for
i being
Nat st
i in Seg m holds
w . i = ((proj (i,m)) . s) * (partdiff (f,x,i)) ) &
L . s = Sum w )
by A5;
consider v being
FinSequence of
REAL n such that A8:
(
dom v = Seg m & ( for
i being
Nat st
i in Seg m holds
v . i = ((proj (i,m)) . t) * (partdiff (f,x,i)) ) &
L . t = Sum v )
by A5;
consider u being
FinSequence of
REAL n such that A9:
(
dom u = Seg m & ( for
i being
Nat st
i in Seg m holds
u . i = ((proj (i,m)) . (s + t)) * (partdiff (f,x,i)) ) &
L . (s + t) = Sum u )
by A5;
A10:
w + v = w <++> v
by INTEGR15:def 9;
A11:
dom u = (dom w) /\ (dom v)
by A7, A8, A9;
now for j being object st j in dom u holds
u . j = (w . j) + (v . j)let j be
object ;
( j in dom u implies u . j = (w . j) + (v . j) )assume A12:
j in dom u
;
u . j = (w . j) + (v . j)then reconsider i =
j as
Nat ;
A13:
w . i = ((proj (i,m)) . s) * (partdiff (f,x,i))
by A7, A9, A12;
A14:
v . i = ((proj (i,m)) . t) * (partdiff (f,x,i))
by A8, A9, A12;
thus u . j =
((proj (i,m)) . (s + t)) * (partdiff (f,x,i))
by A9, A12
.=
((s + t) . i) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
((s . i) + (t . i)) * (partdiff (f,x,i))
by RVSUM_1:11
.=
(((proj (i,m)) . s) + (t . i)) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
(((proj (i,m)) . s) + ((proj (i,m)) . t)) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
(w . j) + (v . j)
by A13, A14, RVSUM_1:50
;
verum end;
then
u = w + v
by A10, A11, VALUED_2:def 45;
hence
L . (s + t) = (L . s) + (L . t)
by A9, A7, A8, Th24;
verum
end;
for s being Element of REAL m
for r being Real holds L . (r * s) = r * (L . s)
proof
let s be
Element of
REAL m;
for r being Real holds L . (r * s) = r * (L . s)let r be
Real;
L . (r * s) = r * (L . s)
consider w being
FinSequence of
REAL n such that A15:
(
dom w = Seg m & ( for
i being
Nat st
i in Seg m holds
w . i = ((proj (i,m)) . s) * (partdiff (f,x,i)) ) &
L . s = Sum w )
by A5;
consider u being
FinSequence of
REAL n such that A16:
(
dom u = Seg m & ( for
i being
Nat st
i in Seg m holds
u . i = ((proj (i,m)) . (r * s)) * (partdiff (f,x,i)) ) &
L . (r * s) = Sum u )
by A5;
A17:
r (#) w = w [#] r
by INTEGR15:def 11;
now for j being object st j in dom u holds
u . j = r (#) (w . j)let j be
object ;
( j in dom u implies u . j = r (#) (w . j) )assume A18:
j in dom u
;
u . j = r (#) (w . j)then reconsider i =
j as
Nat ;
A19:
w . i = ((proj (i,m)) . s) * (partdiff (f,x,i))
by A15, A16, A18;
thus u . j =
((proj (i,m)) . (r * s)) * (partdiff (f,x,i))
by A16, A18
.=
((r * s) . i) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
(r * (s . i)) * (partdiff (f,x,i))
by RVSUM_1:45
.=
(r * ((proj (i,m)) . s)) * (partdiff (f,x,i))
by PDIFF_1:def 1
.=
r (#) (w . j)
by A19, RVSUM_1:49
;
verum end;
then
u = r (#) w
by A17, A15, A16, VALUED_2:def 39;
hence
L . (r * s) = r * (L . s)
by A15, A16, Th25;
verum
end;
then reconsider L = L as LinearOperator of m,n by A6, PDIFF_6:def 1, PDIFF_6:def 2;
take
L
; for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
thus
for h being Element of REAL m ex w being FinSequence of REAL n st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w )
by A5; verum