:: PDIFF_6 semantic presentation
begin
theorem Th1: :: PDIFF_6:1
for m, n being Element of NAT
for f being set holds
( f is PartFunc of (REAL m),(REAL n) iff f is PartFunc of (REAL-NS m),(REAL-NS n) )
proof
let m, n be Element of NAT ; ::_thesis: for f being set holds
( f is PartFunc of (REAL m),(REAL n) iff f is PartFunc of (REAL-NS m),(REAL-NS n) )
let f be set ; ::_thesis: ( f is PartFunc of (REAL m),(REAL n) iff f is PartFunc of (REAL-NS m),(REAL-NS n) )
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4;
hence ( f is PartFunc of (REAL m),(REAL n) iff f is PartFunc of (REAL-NS m),(REAL-NS n) ) ; ::_thesis: verum
end;
theorem Th2: :: PDIFF_6:2
for n, m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y holds
( f is_differentiable_in x iff g is_differentiable_in y )
proof
let n, m be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y holds
( f is_differentiable_in x iff g is_differentiable_in y )
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y holds
( f is_differentiable_in x iff g is_differentiable_in y )
let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y holds
( f is_differentiable_in x iff g is_differentiable_in y )
let x be Element of REAL m; ::_thesis: for y being Point of (REAL-NS m) st f = g & x = y holds
( f is_differentiable_in x iff g is_differentiable_in y )
let y be Point of (REAL-NS m); ::_thesis: ( f = g & x = y implies ( f is_differentiable_in x iff g is_differentiable_in y ) )
assume A1: ( f = g & x = y ) ; ::_thesis: ( f is_differentiable_in x iff g is_differentiable_in y )
hereby ::_thesis: ( g is_differentiable_in y implies f is_differentiable_in x )
assume f is_differentiable_in x ; ::_thesis: g is_differentiable_in y
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_differentiable_in y ) by PDIFF_1:def_7;
hence g is_differentiable_in y by A1; ::_thesis: verum
end;
assume g is_differentiable_in y ; ::_thesis: f is_differentiable_in x
hence f is_differentiable_in x by A1, PDIFF_1:def_7; ::_thesis: verum
end;
theorem Th3: :: PDIFF_6:3
for n, m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff (f,x) = diff (g,y)
proof
let n, m be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff (f,x) = diff (g,y)
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff (f,x) = diff (g,y)
let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff (f,x) = diff (g,y)
let x be Element of REAL m; ::_thesis: for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff (f,x) = diff (g,y)
let y be Point of (REAL-NS m); ::_thesis: ( f = g & x = y & f is_differentiable_in x implies diff (f,x) = diff (g,y) )
assume A1: ( f = g & x = y & f is_differentiable_in x ) ; ::_thesis: diff (f,x) = diff (g,y)
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & diff (f,x) = diff (g,y) ) by PDIFF_1:def_8;
hence diff (f,x) = diff (g,y) by A1; ::_thesis: verum
end;
theorem Th4: :: PDIFF_6:4
for m, n being Element of NAT
for f1, f2 being PartFunc of (REAL m),(REAL n)
for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
proof
let m, n be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of (REAL m),(REAL n)
for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let f1, f2 be PartFunc of (REAL m),(REAL n); ::_thesis: for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let g1, g2 be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 + f2 = g1 + g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 + f2 = g1 + g2
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4;
then reconsider g12 = g1 + g2 as PartFunc of (REAL m),(REAL n) ;
A2: (dom f1) /\ (dom f2) = dom g12 by A1, VFUNCT_1:def_1;
A3: f1 <++> f2 = f1 + f2 by INTEGR15:def_9;
for c being set st c in dom g12 holds
(g1 + g2) . c = (f1 . c) + (f2 . c)
proof
let c be set ; ::_thesis: ( c in dom g12 implies (g1 + g2) . c = (f1 . c) + (f2 . c) )
assume A4: c in dom g12 ; ::_thesis: (g1 + g2) . c = (f1 . c) + (f2 . c)
then A5: c in dom (g1 + g2) ;
( c in dom f1 & c in dom f2 ) by A2, A4, XBOOLE_0:def_4;
then A6: ( f1 /. c = f1 . c & f2 /. c = f2 . c ) by PARTFUN1:def_6;
A7: ( f1 /. c = g1 /. c & f2 /. c = g2 /. c ) by A1, REAL_NS1:def_4;
g12 . c = (g1 + g2) /. c by A4, PARTFUN1:def_6
.= (g1 /. c) + (g2 /. c) by A5, VFUNCT_1:def_1 ;
hence (g1 + g2) . c = (f1 . c) + (f2 . c) by A6, A7, REAL_NS1:2; ::_thesis: verum
end;
hence f1 + f2 = g1 + g2 by A2, A3, VALUED_2:def_45; ::_thesis: verum
end;
theorem Th5: :: PDIFF_6:5
for m, n being Element of NAT
for f1, f2 being PartFunc of (REAL m),(REAL n)
for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
proof
let m, n be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of (REAL m),(REAL n)
for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let f1, f2 be PartFunc of (REAL m),(REAL n); ::_thesis: for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let g1, g2 be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 - f2 = g1 - g2
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4;
then reconsider g12 = g1 - g2 as PartFunc of (REAL m),(REAL n) ;
A2: (dom f1) /\ (dom f2) = dom g12 by A1, VFUNCT_1:def_2;
A3: f1 <--> f2 = f1 - f2 by INTEGR15:def_10;
for c being set st c in dom g12 holds
(g1 - g2) . c = (f1 . c) - (f2 . c)
proof
let c be set ; ::_thesis: ( c in dom g12 implies (g1 - g2) . c = (f1 . c) - (f2 . c) )
assume A4: c in dom g12 ; ::_thesis: (g1 - g2) . c = (f1 . c) - (f2 . c)
then A5: c in dom (g1 - g2) ;
( c in dom f1 & c in dom f2 ) by A2, A4, XBOOLE_0:def_4;
then A6: ( f1 /. c = f1 . c & f2 /. c = f2 . c ) by PARTFUN1:def_6;
A7: ( f1 /. c = g1 /. c & f2 /. c = g2 /. c ) by A1, REAL_NS1:def_4;
g12 . c = (g1 - g2) /. c by A4, PARTFUN1:def_6
.= (g1 /. c) - (g2 /. c) by A5, VFUNCT_1:def_2 ;
hence (g1 - g2) . c = (f1 . c) - (f2 . c) by A6, A7, REAL_NS1:5; ::_thesis: verum
end;
hence f1 - f2 = g1 - g2 by A2, A3, VALUED_2:def_46; ::_thesis: verum
end;
theorem Th6: :: PDIFF_6:6
for m, n being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for a being Real st f = g holds
a (#) f = a (#) g
proof
let m, n be Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for a being Real st f = g holds
a (#) f = a (#) g
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for a being Real st f = g holds
a (#) f = a (#) g
let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for a being Real st f = g holds
a (#) f = a (#) g
let a be Real; ::_thesis: ( f = g implies a (#) f = a (#) g )
assume A1: f = g ; ::_thesis: a (#) f = a (#) g
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4;
then reconsider aG = a (#) g as PartFunc of (REAL m),(REAL n) ;
A2: dom f = dom aG by A1, VFUNCT_1:def_4;
A3: a (#) f = f [#] a by INTEGR15:def_11;
for c being set st c in dom aG holds
aG . c = a (#) (f . c)
proof
let c be set ; ::_thesis: ( c in dom aG implies aG . c = a (#) (f . c) )
assume A4: c in dom aG ; ::_thesis: aG . c = a (#) (f . c)
then A5: c in dom (a (#) g) ;
A6: f /. c = g /. c by A1, REAL_NS1:def_4;
A7: f /. c = f . c by A2, A4, PARTFUN1:def_6;
aG . c = (a (#) g) /. c by A4, PARTFUN1:def_6
.= a * (g /. c) by A5, VFUNCT_1:def_4 ;
hence aG . c = a (#) (f . c) by A6, A7, REAL_NS1:3; ::_thesis: verum
end;
hence a (#) f = a (#) g by A2, A3, VALUED_2:def_39; ::_thesis: verum
end;
theorem Th7: :: PDIFF_6:7
for m, n being Element of NAT
for f1, f2 being Function of (REAL m),(REAL n)
for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
proof
let m, n be Element of NAT ; ::_thesis: for f1, f2 being Function of (REAL m),(REAL n)
for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let f1, f2 be Function of (REAL m),(REAL n); ::_thesis: for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let g1, g2 be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 + f2 = g1 + g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 + f2 = g1 + g2
A2: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4;
then reconsider g12 = g1 + g2 as Function of (REAL m),(REAL n) by LOPBAN_1:def_9;
( g1 is LinearOperator of (REAL-NS m),(REAL-NS n) & g2 is LinearOperator of (REAL-NS m),(REAL-NS n) ) by LOPBAN_1:def_9;
then ( dom g1 = REAL m & dom g2 = REAL m ) by A2, FUNCT_2:def_1;
then A3: (dom f1) /\ (dom f2) = dom g12 by A1, FUNCT_2:def_1;
A4: f1 <++> f2 = f1 + f2 by INTEGR15:def_9;
for c being set st c in dom g12 holds
g12 . c = (f1 . c) + (f2 . c)
proof
let c be set ; ::_thesis: ( c in dom g12 implies g12 . c = (f1 . c) + (f2 . c) )
assume A5: c in dom g12 ; ::_thesis: g12 . c = (f1 . c) + (f2 . c)
then reconsider x = c as VECTOR of (REAL-NS m) by REAL_NS1:def_4;
reconsider c1 = c as Element of REAL m by A5;
g12 . x = (g1 . x) + (g2 . x) by LOPBAN_1:35;
hence g12 . c = (f1 /. c1) + (f2 /. c1) by A1, REAL_NS1:2
.= (f1 . c) + (f2 . c) ;
::_thesis: verum
end;
hence f1 + f2 = g1 + g2 by A3, A4, VALUED_2:def_45; ::_thesis: verum
end;
theorem Th8: :: PDIFF_6:8
for m, n being Element of NAT
for f1, f2 being Function of (REAL m),(REAL n)
for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
proof
let m, n be Element of NAT ; ::_thesis: for f1, f2 being Function of (REAL m),(REAL n)
for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let f1, f2 be Function of (REAL m),(REAL n); ::_thesis: for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let g1, g2 be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 - f2 = g1 - g2
A2: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4;
then reconsider g12 = g1 - g2 as Function of (REAL m),(REAL n) by LOPBAN_1:def_9;
( g1 is LinearOperator of (REAL-NS m),(REAL-NS n) & g2 is LinearOperator of (REAL-NS m),(REAL-NS n) ) by LOPBAN_1:def_9;
then ( dom g1 = REAL m & dom g2 = REAL m ) by A2, FUNCT_2:def_1;
then A3: (dom f1) /\ (dom f2) = dom g12 by A1, FUNCT_2:def_1;
A4: f1 <--> f2 = f1 - f2 by INTEGR15:def_10;
for c being set st c in dom g12 holds
g12 . c = (f1 . c) - (f2 . c)
proof
let c be set ; ::_thesis: ( c in dom g12 implies g12 . c = (f1 . c) - (f2 . c) )
assume A5: c in dom g12 ; ::_thesis: g12 . c = (f1 . c) - (f2 . c)
then reconsider x = c as VECTOR of (REAL-NS m) by REAL_NS1:def_4;
reconsider c1 = c as Element of REAL m by A5;
g12 . x = (g1 . x) - (g2 . x) by LOPBAN_1:40;
hence g12 . c = (f1 /. c1) - (f2 /. c1) by A1, REAL_NS1:5
.= (f1 . c) - (f2 . c) ;
::_thesis: verum
end;
hence f1 - f2 = g1 - g2 by A3, A4, VALUED_2:def_46; ::_thesis: verum
end;
theorem Th9: :: PDIFF_6:9
for m, n being Element of NAT
for f being Function of (REAL m),(REAL n)
for g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for r being Real st f = g holds
r (#) f = r * g
proof
let m, n be Element of NAT ; ::_thesis: for f being Function of (REAL m),(REAL n)
for g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for r being Real st f = g holds
r (#) f = r * g
let f be Function of (REAL m),(REAL n); ::_thesis: for g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for r being Real st f = g holds
r (#) f = r * g
let g be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); ::_thesis: for r being Real st f = g holds
r (#) f = r * g
let r be Real; ::_thesis: ( f = g implies r (#) f = r * g )
assume A1: f = g ; ::_thesis: r (#) f = r * g
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4;
then reconsider rG = r * g as Function of (REAL m),(REAL n) by LOPBAN_1:def_9;
dom f = REAL m by FUNCT_2:def_1;
then A2: dom f = dom rG by FUNCT_2:def_1;
A3: r (#) f = f [#] r by INTEGR15:def_11;
for c being set st c in dom rG holds
rG . c = r (#) (f . c)
proof
let c be set ; ::_thesis: ( c in dom rG implies rG . c = r (#) (f . c) )
assume A4: c in dom rG ; ::_thesis: rG . c = r (#) (f . c)
then reconsider x = c as VECTOR of (REAL-NS m) by REAL_NS1:def_4;
reconsider c1 = c as Element of REAL m by A4;
rG . x = r * (g . x) by LOPBAN_1:36;
hence rG . c = r * (f /. c1) by A1, REAL_NS1:3
.= r (#) (f . c) ;
::_thesis: verum
end;
hence r (#) f = r * g by A2, A3, VALUED_2:def_39; ::_thesis: verum
end;
theorem Th10: :: PDIFF_6:10
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
proof
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
let x be Element of REAL m; ::_thesis: ( f is_differentiable_in x implies diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) )
assume f is_differentiable_in x ; ::_thesis: diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & diff (f,x) = diff (g,y) ) by PDIFF_1:def_8;
hence diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) ; ::_thesis: verum
end;
definition
let n, m be Nat;
let IT be Function of (REAL m),(REAL n);
attrIT is additive means :Def1: :: PDIFF_6:def 1
for x, y being Element of REAL m holds IT . (x + y) = (IT . x) + (IT . y);
attrIT is homogeneous means :Def2: :: PDIFF_6:def 2
for x being Element of REAL m
for r being Real holds IT . (r * x) = r * (IT . x);
end;
:: deftheorem Def1 defines additive PDIFF_6:def_1_:_
for n, m being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is additive iff for x, y being Element of REAL m holds IT . (x + y) = (IT . x) + (IT . y) );
:: deftheorem Def2 defines homogeneous PDIFF_6:def_2_:_
for n, m being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is homogeneous iff for x being Element of REAL m
for r being Real holds IT . (r * x) = r * (IT . x) );
theorem Th11: :: PDIFF_6:11
for m, n being Element of NAT
for IT being Function of (REAL m),(REAL n) st IT is additive holds
IT . (0* m) = 0* n
proof
let m, n be Element of NAT ; ::_thesis: for IT being Function of (REAL m),(REAL n) st IT is additive holds
IT . (0* m) = 0* n
let IT be Function of (REAL m),(REAL n); ::_thesis: ( IT is additive implies IT . (0* m) = 0* n )
assume A1: IT is additive ; ::_thesis: IT . (0* m) = 0* n
IT . (0* m) = IT . ((0* m) + (0* m)) by RVSUM_1:16;
then IT . (0* m) = (IT . (0* m)) + (IT . (0* m)) by A1, Def1;
then 0* n = ((IT . (0* m)) + (IT . (0* m))) - (IT . (0* m)) by RVSUM_1:37;
hence 0* n = IT . (0* m) by RVSUM_1:42; ::_thesis: verum
end;
theorem Th12: :: PDIFF_6:12
for m, n being Element of NAT
for f being Function of (REAL m),(REAL n)
for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is additive iff g is additive )
proof
let m, n be Element of NAT ; ::_thesis: for f being Function of (REAL m),(REAL n)
for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is additive iff g is additive )
let f be Function of (REAL m),(REAL n); ::_thesis: for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is additive iff g is additive )
let g be Function of (REAL-NS m),(REAL-NS n); ::_thesis: ( f = g implies ( f is additive iff g is additive ) )
assume A1: f = g ; ::_thesis: ( f is additive iff g is additive )
hereby ::_thesis: ( g is additive implies f is additive )
assume A2: f is additive ; ::_thesis: g is additive
now__::_thesis:_for_x,_y_being_Point_of_(REAL-NS_m)_holds_g_._(x_+_y)_=_(g_._x)_+_(g_._y)
let x, y be Point of (REAL-NS m); ::_thesis: g . (x + y) = (g . x) + (g . y)
reconsider x1 = x, y1 = y as Element of REAL m by REAL_NS1:def_4;
g . (x + y) = f . (x1 + y1) by A1, REAL_NS1:2
.= (f . x1) + (f . y1) by A2, Def1 ;
hence g . (x + y) = (g . x) + (g . y) by A1, REAL_NS1:2; ::_thesis: verum
end;
hence g is additive by VECTSP_1:def_20; ::_thesis: verum
end;
assume A3: g is additive ; ::_thesis: f is additive
now__::_thesis:_for_x,_y_being_Element_of_REAL_m_holds_f_._(x_+_y)_=_(f_._x)_+_(f_._y)
let x, y be Element of REAL m; ::_thesis: f . (x + y) = (f . x) + (f . y)
reconsider x1 = x, y1 = y as Point of (REAL-NS m) by REAL_NS1:def_4;
f . (x + y) = g . (x1 + y1) by A1, REAL_NS1:2
.= (g . x1) + (g . y1) by A3, VECTSP_1:def_20 ;
hence f . (x + y) = (f . x) + (f . y) by A1, REAL_NS1:2; ::_thesis: verum
end;
hence f is additive by Def1; ::_thesis: verum
end;
theorem Th13: :: PDIFF_6:13
for m, n being Element of NAT
for f being Function of (REAL m),(REAL n)
for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is homogeneous iff g is homogeneous )
proof
let m, n be Element of NAT ; ::_thesis: for f being Function of (REAL m),(REAL n)
for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is homogeneous iff g is homogeneous )
let f be Function of (REAL m),(REAL n); ::_thesis: for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is homogeneous iff g is homogeneous )
let g be Function of (REAL-NS m),(REAL-NS n); ::_thesis: ( f = g implies ( f is homogeneous iff g is homogeneous ) )
assume A1: f = g ; ::_thesis: ( f is homogeneous iff g is homogeneous )
hereby ::_thesis: ( g is homogeneous implies f is homogeneous )
assume A2: f is homogeneous ; ::_thesis: g is homogeneous
now__::_thesis:_for_x_being_Point_of_(REAL-NS_m)
for_r_being_Real_holds_g_._(r_*_x)_=_r_*_(g_._x)
let x be Point of (REAL-NS m); ::_thesis: for r being Real holds g . (r * x) = r * (g . x)
let r be Real; ::_thesis: g . (r * x) = r * (g . x)
reconsider x1 = x as Element of REAL m by REAL_NS1:def_4;
g . (r * x) = f . (r * x1) by A1, REAL_NS1:3
.= r * (f . x1) by A2, Def2 ;
hence g . (r * x) = r * (g . x) by A1, REAL_NS1:3; ::_thesis: verum
end;
hence g is homogeneous by LOPBAN_1:def_5; ::_thesis: verum
end;
assume A3: g is homogeneous ; ::_thesis: f is homogeneous
now__::_thesis:_for_x_being_Element_of_REAL_m
for_r_being_Real_holds_f_._(r_*_x)_=_r_*_(f_._x)
let x be Element of REAL m; ::_thesis: for r being Real holds f . (r * x) = r * (f . x)
let r be Real; ::_thesis: f . (r * x) = r * (f . x)
reconsider x1 = x as Point of (REAL-NS m) by REAL_NS1:def_4;
f . (r * x) = g . (r * x1) by A1, REAL_NS1:3
.= r * (g . x1) by A3, LOPBAN_1:def_5 ;
hence f . (r * x) = r * (f . x) by A1, REAL_NS1:3; ::_thesis: verum
end;
hence f is homogeneous by Def2; ::_thesis: verum
end;
registration
let n, m be Nat;
cluster(REAL m) --> (0* n) -> additive homogeneous for Function of (REAL m),(REAL n);
coherence
for b1 being Function of (REAL m),(REAL n) st b1 = (REAL m) --> (0* n) holds
( b1 is additive & b1 is homogeneous )
proof
let f be Function of (REAL m),(REAL n); ::_thesis: ( f = (REAL m) --> (0* n) implies ( f is additive & f is homogeneous ) )
assume A1: f = (REAL m) --> (0* n) ; ::_thesis: ( f is additive & f is homogeneous )
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
hereby :: according to PDIFF_6:def_1 ::_thesis: f is homogeneous
let x, y be Element of REAL m; ::_thesis: f . (x + y) = (f . x) + (f . y)
A2: 0. (REAL-NS n1) = 0* n by REAL_NS1:def_4;
f . (x + y) = 0* n by A1, FUNCOP_1:7
.= 0. (REAL-NS n1) by REAL_NS1:def_4
.= (0. (REAL-NS n1)) + (0. (REAL-NS n1)) by RLVECT_1:4
.= (0* n) + (0* n) by A2, REAL_NS1:2
.= (f . x) + (0* n) by A1, FUNCOP_1:7 ;
hence f . (x + y) = (f . x) + (f . y) by A1, FUNCOP_1:7; ::_thesis: verum
end;
hereby :: according to PDIFF_6:def_2 ::_thesis: verum
let x be Element of REAL m; ::_thesis: for r being Real holds f . (r * x) = r * (f . x)
let r be Real; ::_thesis: f . (r * x) = r * (f . x)
A3: 0. (REAL-NS n1) = 0* n by REAL_NS1:def_4;
f . (r * x) = 0* n by A1, FUNCOP_1:7
.= 0. (REAL-NS n1) by REAL_NS1:def_4
.= r * (0. (REAL-NS n1)) by RLVECT_1:10
.= r * (0* n) by A3, REAL_NS1:3 ;
hence f . (r * x) = r * (f . x) by A1, FUNCOP_1:7; ::_thesis: verum
end;
end;
end;
registration
let n, m be Nat;
cluster non empty Relation-like REAL m -defined REAL n -valued Function-like total V30( REAL m, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued additive homogeneous for Element of K6(K7((REAL m),(REAL n)));
existence
ex b1 being Function of (REAL m),(REAL n) st
( b1 is additive & b1 is homogeneous )
proof
take (REAL m) --> (0* n) ; ::_thesis: ( (REAL m) --> (0* n) is additive & (REAL m) --> (0* n) is homogeneous )
thus ( (REAL m) --> (0* n) is additive & (REAL m) --> (0* n) is homogeneous ) ; ::_thesis: verum
end;
end;
definition
let m, n be Nat;
mode LinearOperator of m,n is additive homogeneous Function of (REAL m),(REAL n);
end;
theorem Th14: :: PDIFF_6:14
for m, n being Element of NAT
for f being set holds
( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) )
proof
let m, n be Element of NAT ; ::_thesis: for f being set holds
( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) )
let f be set ; ::_thesis: ( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) )
( REAL m = the carrier of (REAL-NS m) & REAL n = the carrier of (REAL-NS n) ) by REAL_NS1:def_4;
hence ( f is additive homogeneous Function of (REAL m),(REAL n) iff f is additive homogeneous Function of (REAL-NS m),(REAL-NS n) ) by Th12, Th13; ::_thesis: verum
end;
definition
let m, n be Nat;
let IT be Function of (REAL m),(REAL n);
let x be Element of REAL m;
:: original: .
redefine funcIT . x -> Element of REAL n;
coherence
IT . x is Element of REAL n
proof
IT . x is Element of REAL n ;
hence IT . x is Element of REAL n ; ::_thesis: verum
end;
end;
definition
let m, n be Nat;
let IT be Function of (REAL m),(REAL n);
attrIT is Lipschitzian means :Def3: :: PDIFF_6:def 3
ex K being Real st
( 0 <= K & ( for x being Element of REAL m holds |.(IT . x).| <= K * |.x.| ) );
end;
:: deftheorem Def3 defines Lipschitzian PDIFF_6:def_3_:_
for m, n being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is Lipschitzian iff ex K being Real st
( 0 <= K & ( for x being Element of REAL m holds |.(IT . x).| <= K * |.x.| ) ) );
theorem Th15: :: PDIFF_6:15
for m being Element of NAT
for xseq, yseq being FinSequence of REAL m st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds
ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
proof
let m be Element of NAT ; ::_thesis: for xseq, yseq being FinSequence of REAL m st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds
ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
let xseq, yseq be FinSequence of REAL m; ::_thesis: ( len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq implies ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) )
assume A1: ( len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq ) ; ::_thesis: ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
A2: ( len xseq = len (accum xseq) & xseq . 1 = (accum xseq) . 1 & ( for k being Nat st 1 <= k & k < len xseq holds
(accum xseq) . (k + 1) = ((accum xseq) /. k) + (xseq /. (k + 1)) ) ) by EUCLID_7:def_10;
A3: Sum xseq = (accum xseq) . (len xseq) by A1, EUCLID_7:def_11;
set g = accum xseq;
set i = len yseq;
percases ( len yseq = 0 or len yseq <> 0 ) ;
supposeA4: len yseq = 0 ; ::_thesis: ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
then reconsider v = xseq . (len xseq) as Element of REAL m by A1, A3, EUCLID_7:def_10;
take v ; ::_thesis: ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
Sum yseq = 0* m by A4, EUCLID_7:def_11;
hence ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) by A1, A2, A3, A4, RVSUM_1:16; ::_thesis: verum
end;
supposeA5: len yseq <> 0 ; ::_thesis: ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
A6: ( len yseq = len (accum yseq) & yseq . 1 = (accum yseq) . 1 & ( for k being Nat st 1 <= k & k < len yseq holds
(accum yseq) . (k + 1) = ((accum yseq) /. k) + (yseq /. (k + 1)) ) ) by EUCLID_7:def_10;
A7: Sum yseq = (accum yseq) . (len yseq) by A5, EUCLID_7:def_11;
set g0 = accum yseq;
A8: len yseq <= len (accum xseq) by A1, A2, NAT_1:11;
then A9: len ((accum xseq) | (len yseq)) = len yseq by FINSEQ_1:59;
A10: for k being Nat st 1 <= k & k <= len ((accum xseq) | (len yseq)) holds
((accum xseq) | (len yseq)) . k = (accum yseq) . k
proof
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len ((accum xseq) | (len yseq)) implies ((accum xseq) | (len yseq)) . $1 = (accum yseq) . $1 );
A11: S1[ 0 ] ;
A12: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A13: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_1_<=_k_+_1_&_k_+_1_<=_len_((accum_xseq)_|_(len_yseq))_implies_((accum_xseq)_|_(len_yseq))_._(k_+_1)_=_(accum_yseq)_._(k_+_1)_)
assume A14: ( 1 <= k + 1 & k + 1 <= len ((accum xseq) | (len yseq)) ) ; ::_thesis: ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1)
then A15: k + 1 <= len yseq by A8, FINSEQ_1:59;
then k + 1 in Seg (len yseq) by A14;
then A16: ( ((accum xseq) | (len yseq)) . (k + 1) = (accum xseq) . (k + 1) & xseq . (k + 1) = (xseq | (Seg (len yseq))) . (k + 1) ) by FUNCT_1:49;
A17: k < len yseq by A15, NAT_1:13;
now__::_thesis:_(_k_<>_0_implies_((accum_xseq)_|_(len_yseq))_._(k_+_1)_=_(accum_yseq)_._(k_+_1)_)
assume A18: k <> 0 ; ::_thesis: ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1)
then A19: 1 <= k by NAT_1:14;
then A20: k in Seg (len yseq) by A17, FINSEQ_1:1;
len yseq <= len xseq by A1, NAT_1:12;
then A21: k < len xseq by A17, XXREAL_0:2;
then (accum xseq) /. k = (accum xseq) . k by A2, A19, FINSEQ_4:15;
then (accum xseq) /. k = ((accum xseq) | (len yseq)) . k by A20, FUNCT_1:49;
then A22: (accum xseq) /. k = (accum yseq) /. k by A6, A17, A19, A13, A14, FINSEQ_4:15, NAT_1:13;
k + 1 <= len xseq by A15, A1, NAT_1:12;
then xseq /. (k + 1) = xseq . (k + 1) by A14, FINSEQ_4:15;
then xseq /. (k + 1) = yseq /. (k + 1) by A1, A14, A9, A16, FINSEQ_4:15;
then ((accum xseq) /. k) + (xseq /. (k + 1)) = (accum yseq) . (k + 1) by A6, A17, A18, A22, NAT_1:14;
hence ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) by A2, A16, A18, A21, NAT_1:14; ::_thesis: verum
end;
hence ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) by A1, A6, A16, EUCLID_7:def_10; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
thus for k being Nat holds S1[k] from NAT_1:sch_2(A11, A12); ::_thesis: verum
end;
1 <= len yseq by A5, NAT_1:14;
then len yseq in Seg (len yseq) ;
then A23: len yseq in dom ((accum xseq) | (len yseq)) by A9, FINSEQ_1:def_3;
then len yseq in dom (accum xseq) by RELAT_1:57;
then (accum xseq) . (len yseq) = (accum xseq) /. (len yseq) by PARTFUN1:def_6;
then ((accum xseq) | (len yseq)) . (len yseq) = (accum xseq) /. (len yseq) by A23, FUNCT_1:47;
then A24: (accum yseq) . (len yseq) = (accum xseq) /. (len yseq) by A6, A9, A10, FINSEQ_1:14;
dom xseq = Seg ((len yseq) + 1) by A1, FINSEQ_1:def_3;
then xseq . (len xseq) in rng xseq by A1, FINSEQ_1:4, FUNCT_1:3;
then reconsider v = xseq . (len xseq) as Element of REAL m ;
take v ; ::_thesis: ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
thus v = xseq . (len xseq) ; ::_thesis: Sum xseq = (Sum yseq) + v
A25: len yseq < len xseq by A1, NAT_1:13;
1 <= (len yseq) + 1 by NAT_1:11;
then ((accum xseq) /. (len yseq)) + (xseq /. ((len yseq) + 1)) = (Sum yseq) + v by A7, A24, A1, FINSEQ_4:15;
hence Sum xseq = (Sum yseq) + v by A1, A25, A2, A3, A5, NAT_1:14; ::_thesis: verum
end;
end;
end;
theorem Th16: :: PDIFF_6:16
for m, n being Element of NAT
for f being LinearOperator of m,n
for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)
proof
let m, n be Element of NAT ; ::_thesis: for f being LinearOperator of m,n
for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)
let f be LinearOperator of m,n; ::_thesis: for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)
defpred S1[ Nat] means for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL n st $1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq);
A1: S1[ 0 ]
proof
let xseq be FinSequence of REAL m; ::_thesis: for yseq being FinSequence of REAL n st 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)
let yseq be FinSequence of REAL n; ::_thesis: ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) implies Sum yseq = f . (Sum xseq) )
assume ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) ) ; ::_thesis: Sum yseq = f . (Sum xseq)
then ( Sum xseq = 0* m & Sum yseq = 0* n ) by EUCLID_7:def_11;
hence Sum yseq = f . (Sum xseq) by Th11; ::_thesis: verum
end;
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A3: S1[i] ; ::_thesis: S1[i + 1]
now__::_thesis:_for_xseq_being_FinSequence_of_REAL_m
for_yseq_being_FinSequence_of_REAL_n_st_i_+_1_=_len_xseq_&_len_xseq_=_len_yseq_&_(_for_k_being_Element_of_NAT_st_k_in_dom_xseq_holds_
yseq_._k_=_f_._(xseq_._k)_)_holds_
Sum_yseq_=_f_._(Sum_xseq)
let xseq be FinSequence of REAL m; ::_thesis: for yseq being FinSequence of REAL n st i + 1 = len xseq & len xseq = len yseq & ( for k being Element of NAT st k in dom xseq holds
yseq . k = f . (xseq . k) ) holds
Sum yseq = f . (Sum xseq)
let yseq be FinSequence of REAL n; ::_thesis: ( i + 1 = len xseq & len xseq = len yseq & ( for k being Element of NAT st k in dom xseq holds
yseq . k = f . (xseq . k) ) implies Sum yseq = f . (Sum xseq) )
assume A4: ( i + 1 = len xseq & len xseq = len yseq & ( for k being Element of NAT st k in dom xseq holds
yseq . k = f . (xseq . k) ) ) ; ::_thesis: Sum yseq = f . (Sum xseq)
set xseq0 = xseq | i;
set yseq0 = yseq | i;
A5: i = len (xseq | i) by A4, FINSEQ_1:59, NAT_1:11;
then A6: len (xseq | i) = len (yseq | i) by A4, FINSEQ_1:59, NAT_1:11;
for k being Element of NAT st k in dom (xseq | i) holds
(yseq | i) . k = f . ((xseq | i) . k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom (xseq | i) implies (yseq | i) . k = f . ((xseq | i) . k) )
assume A7: k in dom (xseq | i) ; ::_thesis: (yseq | i) . k = f . ((xseq | i) . k)
then A8: k in Seg i by RELAT_1:57;
k in dom xseq by A7, RELAT_1:57;
then A9: yseq . k = f . (xseq . k) by A4;
xseq . k = (xseq | i) . k by A8, FUNCT_1:49;
hence (yseq | i) . k = f . ((xseq | i) . k) by A8, A9, FUNCT_1:49; ::_thesis: verum
end;
then A10: Sum (yseq | i) = f . (Sum (xseq | i)) by A5, A6, A3;
consider v being Element of REAL m such that
A11: ( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by A4, A5, Th15;
consider w being Element of REAL n such that
A12: ( w = yseq . (len yseq) & Sum yseq = (Sum (yseq | i)) + w ) by A4, A5, A6, Th15;
dom xseq = Seg (i + 1) by A4, FINSEQ_1:def_3;
then w = f . v by A4, A12, A11, FINSEQ_1:4;
hence Sum yseq = f . (Sum xseq) by A10, A11, A12, Def1; ::_thesis: verum
end;
hence S1[i + 1] ; ::_thesis: verum
end;
A13: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A2);
let xseq be FinSequence of REAL m; ::_thesis: for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)
let yseq be FinSequence of REAL n; ::_thesis: ( len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) implies Sum yseq = f . (Sum xseq) )
assume ( len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) ) ; ::_thesis: Sum yseq = f . (Sum xseq)
hence Sum yseq = f . (Sum xseq) by A13; ::_thesis: verum
end;
theorem Th17: :: PDIFF_6:17
for m being Element of NAT
for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq
proof
let m be Element of NAT ; ::_thesis: for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq
defpred S1[ Nat] means for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st $1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq;
A1: S1[ 0 ]
proof
let xseq be FinSequence of REAL m; ::_thesis: for yseq being FinSequence of REAL st 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq
let yseq be FinSequence of REAL ; ::_thesis: ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) implies |.(Sum xseq).| <= Sum yseq )
assume ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) ) ; ::_thesis: |.(Sum xseq).| <= Sum yseq
then ( Sum xseq = 0* m & <*> REAL = yseq ) by EUCLID_7:def_11;
hence |.(Sum xseq).| <= Sum yseq by EUCLID:7, RVSUM_1:72; ::_thesis: verum
end;
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A3: S1[i] ; ::_thesis: S1[i + 1]
now__::_thesis:_for_xseq_being_FinSequence_of_REAL_m
for_yseq_being_FinSequence_of_REAL_st_i_+_1_=_len_xseq_&_len_xseq_=_len_yseq_&_(_for_i_being_Element_of_NAT_st_i_in_dom_xseq_holds_
ex_v_being_Element_of_REAL_m_st_
(_v_=_xseq_._i_&_yseq_._i_=_|.v.|_)_)_holds_
|.(Sum_xseq).|_<=_Sum_yseq
let xseq be FinSequence of REAL m; ::_thesis: for yseq being FinSequence of REAL st i + 1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq
let yseq be FinSequence of REAL ; ::_thesis: ( i + 1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) implies |.(Sum xseq).| <= Sum yseq )
set xseq0 = xseq | i;
set yseq0 = yseq | i;
assume A4: ( i + 1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) ) ; ::_thesis: |.(Sum xseq).| <= Sum yseq
A5: for k being Element of NAT st k in dom (xseq | i) holds
ex v being Element of REAL m st
( v = (xseq | i) . k & (yseq | i) . k = |.v.| )
proof
let k be Element of NAT ; ::_thesis: ( k in dom (xseq | i) implies ex v being Element of REAL m st
( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) )
assume k in dom (xseq | i) ; ::_thesis: ex v being Element of REAL m st
( v = (xseq | i) . k & (yseq | i) . k = |.v.| )
then A6: ( k in Seg i & k in dom xseq ) by RELAT_1:57;
then consider v being Element of REAL m such that
A7: ( v = xseq . k & yseq . k = |.v.| ) by A4;
take v ; ::_thesis: ( v = (xseq | i) . k & (yseq | i) . k = |.v.| )
thus ( v = (xseq | i) . k & (yseq | i) . k = |.v.| ) by A6, A7, FUNCT_1:49; ::_thesis: verum
end;
dom xseq = Seg (i + 1) by A4, FINSEQ_1:def_3;
then consider w being Element of REAL m such that
A8: ( w = xseq . (i + 1) & yseq . (i + 1) = |.w.| ) by A4, FINSEQ_1:4;
A9: ( 1 <= i + 1 & i + 1 <= len yseq ) by A4, NAT_1:11;
yseq = (yseq | i) ^ <*(yseq /. (i + 1))*> by A4, FINSEQ_5:21;
then yseq = (yseq | i) ^ <*(yseq . (i + 1))*> by A9, FINSEQ_4:15;
then A10: Sum yseq = (Sum (yseq | i)) + (yseq . (i + 1)) by RVSUM_1:74;
A11: i = len (xseq | i) by A4, FINSEQ_1:59, NAT_1:11;
then A12: ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by A4, Th15;
A13: |.((Sum (xseq | i)) + w).| <= |.(Sum (xseq | i)).| + |.w.| by EUCLID:12;
len (xseq | i) = len (yseq | i) by A4, A11, FINSEQ_1:59, NAT_1:11;
then |.(Sum (xseq | i)).| <= Sum (yseq | i) by A3, A5, A11;
then |.(Sum (xseq | i)).| + |.w.| <= (Sum (yseq | i)) + (yseq . (i + 1)) by A8, XREAL_1:6;
hence |.(Sum xseq).| <= Sum yseq by A4, A8, A10, A12, A13, XXREAL_0:2; ::_thesis: verum
end;
hence S1[i + 1] ; ::_thesis: verum
end;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A1, A2);
hence for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq ; ::_thesis: verum
end;
registration
let m, n be Nat;
cluster Function-like V30( REAL m, REAL n) additive homogeneous -> Lipschitzian for Element of K6(K7((REAL m),(REAL n)));
coherence
for b1 being LinearOperator of m,n holds b1 is Lipschitzian
proof
let f be LinearOperator of m,n; ::_thesis: f is Lipschitzian
A1: ( m in NAT & n in NAT ) by ORDINAL1:def_12;
defpred S1[ Nat, set ] means n = |.(f . (Base_FinSeq (m,m))).|;
A2: for k0 being Nat st k0 in Seg m holds
ex v being Element of REAL st S1[k0,v] ;
consider KS being FinSequence of REAL such that
A3: ( dom KS = Seg m & ( for i being Nat st i in Seg m holds
S1[i,KS . i] ) ) from FINSEQ_1:sch_5(A2);
set K = (Sum KS) + 1;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_KS_holds_
0_<=_KS_._j
let j be Nat; ::_thesis: ( j in dom KS implies 0 <= KS . j )
assume j in dom KS ; ::_thesis: 0 <= KS . j
then KS . j = |.(f . (Base_FinSeq (m,j))).| by A3;
hence 0 <= KS . j ; ::_thesis: verum
end;
then A4: 0 <= Sum KS by RVSUM_1:84;
reconsider m0 = m as Nat ;
now__::_thesis:_for_x_being_Element_of_REAL_m_holds_|.(f_._x).|_<=_((Sum_KS)_+_1)_*_|.x.|
let x be Element of REAL m; ::_thesis: |.(f . x).| <= ((Sum KS) + 1) * |.x.|
A5: len (ProjFinSeq x) = m by EUCLID_7:def_12;
defpred S2[ set , set ] means n = f . ((ProjFinSeq x) . m);
A6: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_m_holds_
ex_x_being_Element_of_REAL_n_st_S2[k,x]
let k be Nat; ::_thesis: ( k in Seg m implies ex x being Element of REAL n st S2[k,x] )
assume k in Seg m ; ::_thesis: ex x being Element of REAL n st S2[k,x]
then k in dom (ProjFinSeq x) by A5, FINSEQ_1:def_3;
then reconsider v = (ProjFinSeq x) . k as Element of REAL m by PARTFUN1:4;
f . v is Element of REAL n ;
hence ex x being Element of REAL n st S2[k,x] ; ::_thesis: verum
end;
consider fx being FinSequence of REAL n such that
A7: ( dom fx = Seg m & ( for i being Nat st i in Seg m holds
S2[i,fx . i] ) ) from FINSEQ_1:sch_5(A6);
A8: ( x = Sum (ProjFinSeq x) & len fx = m ) by A1, A7, EUCLID_7:31, FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(ProjFinSeq_x)_holds_
fx_._i_=_f_._((ProjFinSeq_x)_._i)
let i be Element of NAT ; ::_thesis: ( i in dom (ProjFinSeq x) implies fx . i = f . ((ProjFinSeq x) . i) )
assume i in dom (ProjFinSeq x) ; ::_thesis: fx . i = f . ((ProjFinSeq x) . i)
then i in Seg m by A5, FINSEQ_1:def_3;
hence fx . i = f . ((ProjFinSeq x) . i) by A7; ::_thesis: verum
end;
then A9: Sum fx = f . x by A1, A5, A8, Th16;
reconsider x0 = x as Element of REAL m ;
A10: for i being Nat st 1 <= i & i <= m holds
ex v being Element of REAL n st
( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| )
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= m implies ex v being Element of REAL n st
( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| ) )
assume A11: ( 1 <= i & i <= m ) ; ::_thesis: ex v being Element of REAL n st
( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| )
then A12: (ProjFinSeq x) . i = |(x,(Base_FinSeq (m,i)))| * (Base_FinSeq (m,i)) by EUCLID_7:def_12;
A13: i in Seg m by A11, FINSEQ_1:1;
then reconsider v = fx . i as Element of REAL n by A7, PARTFUN1:4;
take v ; ::_thesis: ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| )
v = f . ((ProjFinSeq x) . i) by A7, A13;
then v = |(x,(Base_FinSeq (m,i)))| * (f . (Base_FinSeq (m,i))) by A12, Def2;
then v = (x0 . i) * (f . (Base_FinSeq (m,i))) by A11, EUCLID_7:30;
then |.v.| = |.(x0 . i).| * |.(f . (Base_FinSeq (m,i))).| by EUCLID:11;
hence ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| ) by A13, REAL_NS1:8, XREAL_1:64; ::_thesis: verum
end;
defpred S3[ set , set ] means ex v being Element of REAL n st
( v = fx . m & n = |.v.| );
A14: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_m_holds_
ex_x_being_Element_of_REAL_st_S3[k,x]
let k be Nat; ::_thesis: ( k in Seg m implies ex x being Element of REAL st S3[k,x] )
assume k in Seg m ; ::_thesis: ex x being Element of REAL st S3[k,x]
then reconsider v = fx . k as Element of REAL n by A7, PARTFUN1:4;
|.v.| in REAL ;
hence ex x being Element of REAL st S3[k,x] ; ::_thesis: verum
end;
consider zfx being FinSequence of REAL such that
A15: ( dom zfx = Seg m & ( for i being Nat st i in Seg m holds
S3[i,zfx . i] ) ) from FINSEQ_1:sch_5(A14);
A16: len zfx = m by A1, A15, FINSEQ_1:def_3;
then A17: len fx = len zfx by A7, FINSEQ_1:def_3;
for i being Element of NAT st i in dom fx holds
ex v being Element of REAL n st
( v = fx . i & zfx . i = |.v.| ) by A7, A15;
then A18: |.(f . x).| <= Sum zfx by A1, A9, A17, Th17;
A19: now__::_thesis:_for_j_being_Nat_st_j_in_Seg_m_holds_
zfx_._j_<=_(|.x.|_*_KS)_._j
let j be Nat; ::_thesis: ( j in Seg m implies zfx . j <= (|.x.| * KS) . j )
assume A20: j in Seg m ; ::_thesis: zfx . j <= (|.x.| * KS) . j
then A21: ex v being Element of REAL n st
( v = fx . j & zfx . j = |.v.| ) by A15;
( 1 <= j & j <= m ) by A20, FINSEQ_1:1;
then ex v being Element of REAL n st
( v = fx . j & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,j))).| ) by A10;
then zfx . j <= |.x.| * (KS . j) by A3, A20, A21;
hence zfx . j <= (|.x.| * KS) . j by VALUED_1:6; ::_thesis: verum
end;
A22: zfx is Element of m -tuples_on REAL by A16, FINSEQ_2:92;
len KS = m by A1, A3, FINSEQ_1:def_3;
then reconsider KS0 = KS as Element of REAL m0 by FINSEQ_2:92;
|.x.| * KS0 is Element of m0 -tuples_on REAL ;
then Sum zfx <= Sum (|.x.| * KS) by A19, A22, RVSUM_1:82;
then Sum zfx <= |.x.| * (Sum KS) by RVSUM_1:87;
then A23: |.(f . x).| <= |.x.| * (Sum KS) by A18, XXREAL_0:2;
0 + (Sum KS) <= 1 + (Sum KS) by XREAL_1:6;
then |.x.| * (Sum KS) <= |.x.| * (1 + (Sum KS)) by XREAL_1:64;
hence |.(f . x).| <= ((Sum KS) + 1) * |.x.| by A23, XXREAL_0:2; ::_thesis: verum
end;
hence f is Lipschitzian by A4, Def3; ::_thesis: verum
end;
end;
registration
let m, n be Element of NAT ;
cluster Function-like V30( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) additive homogeneous -> Lipschitzian for Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)));
coherence
for b1 being LinearOperator of (REAL-NS m),(REAL-NS n) holds b1 is Lipschitzian
proof
let f be LinearOperator of (REAL-NS m),(REAL-NS n); ::_thesis: f is Lipschitzian
reconsider g = f as LinearOperator of m,n by Th14;
consider K being Real such that
A1: ( 0 <= K & ( for x being Element of REAL m holds |.(g . x).| <= K * |.x.| ) ) by Def3;
take K ; :: according to LOPBAN_1:def_8 ::_thesis: ( 0 <= K & ( for b1 being Element of the carrier of (REAL-NS m) holds ||.(f . b1).|| <= K * ||.b1.|| ) )
thus 0 <= K by A1; ::_thesis: for b1 being Element of the carrier of (REAL-NS m) holds ||.(f . b1).|| <= K * ||.b1.||
let x be Point of (REAL-NS m); ::_thesis: ||.(f . x).|| <= K * ||.x.||
reconsider x1 = x as Element of REAL m by REAL_NS1:def_4;
reconsider y = g . x1 as Element of REAL n ;
||.(f . x).|| = |.y.| by REAL_NS1:1;
then ||.(f . x).|| <= K * |.x1.| by A1;
hence ||.(f . x).|| <= K * ||.x.|| by REAL_NS1:1; ::_thesis: verum
end;
end;
theorem Th18: :: PDIFF_6:18
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n)
proof
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n)
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n)
let x be Element of REAL m; ::_thesis: ( f is_differentiable_in x implies diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) )
assume f is_differentiable_in x ; ::_thesis: diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n)
then diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) by Th10;
hence diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9; ::_thesis: verum
end;
theorem :: PDIFF_6:19
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of m,n
proof
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of m,n
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of m,n
let x be Element of REAL m; ::_thesis: ( f is_differentiable_in x implies diff (f,x) is LinearOperator of m,n )
assume f is_differentiable_in x ; ::_thesis: diff (f,x) is LinearOperator of m,n
then diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) by Th18;
hence diff (f,x) is LinearOperator of m,n by Th14; ::_thesis: verum
end;
theorem :: PDIFF_6:20
for n, m being non empty Element of NAT
for g1, g2 being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) )
proof
let n, m be non empty Element of NAT ; ::_thesis: for g1, g2 being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) )
let g1, g2 be PartFunc of (REAL m),(REAL n); ::_thesis: for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) )
let y0 be Element of REAL m; ::_thesis: ( g1 is_differentiable_in y0 & g2 is_differentiable_in y0 implies ( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) ) )
assume A1: ( g1 is_differentiable_in y0 & g2 is_differentiable_in y0 ) ; ::_thesis: ( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) )
reconsider f1 = g1 as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider f2 = g2 as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider x0 = y0 as Point of (REAL-NS m) by REAL_NS1:def_4;
( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A1, Th2;
then A2: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) by NDIFF_1:35;
f1 + f2 = g1 + g2 by Th4;
hence g1 + g2 is_differentiable_in y0 by A2, Th2; ::_thesis: diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0))
then A3: diff ((g1 + g2),y0) = diff ((f1 + f2),x0) by Th4, Th3;
( diff (f1,x0) = diff (g1,y0) & diff (f2,x0) = diff (g2,y0) ) by Th3, A1;
hence diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) by A2, A3, Th7; ::_thesis: verum
end;
theorem :: PDIFF_6:21
for n, m being non empty Element of NAT
for g1, g2 being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
( g1 - g2 is_differentiable_in y0 & diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) )
proof
let n, m be non empty Element of NAT ; ::_thesis: for g1, g2 being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
( g1 - g2 is_differentiable_in y0 & diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) )
let g1, g2 be PartFunc of (REAL m),(REAL n); ::_thesis: for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
( g1 - g2 is_differentiable_in y0 & diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) )
let y0 be Element of REAL m; ::_thesis: ( g1 is_differentiable_in y0 & g2 is_differentiable_in y0 implies ( g1 - g2 is_differentiable_in y0 & diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) ) )
assume A1: ( g1 is_differentiable_in y0 & g2 is_differentiable_in y0 ) ; ::_thesis: ( g1 - g2 is_differentiable_in y0 & diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) )
reconsider f1 = g1 as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider f2 = g2 as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider x0 = y0 as Point of (REAL-NS m) by REAL_NS1:def_4;
( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A1, Th2;
then A2: ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) by NDIFF_1:36;
f1 - f2 = g1 - g2 by Th5;
hence g1 - g2 is_differentiable_in y0 by A2, Th2; ::_thesis: diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0))
then A3: diff ((g1 - g2),y0) = diff ((f1 - f2),x0) by Th3, Th5;
( diff (f1,x0) = diff (g1,y0) & diff (f2,x0) = diff (g2,y0) ) by Th3, A1;
hence diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) by A2, A3, Th8; ::_thesis: verum
end;
theorem :: PDIFF_6:22
for n, m being non empty Element of NAT
for g being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m
for r being Real st g is_differentiable_in y0 holds
( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )
proof
let n, m be non empty Element of NAT ; ::_thesis: for g being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m
for r being Real st g is_differentiable_in y0 holds
( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )
let g be PartFunc of (REAL m),(REAL n); ::_thesis: for y0 being Element of REAL m
for r being Real st g is_differentiable_in y0 holds
( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )
let y0 be Element of REAL m; ::_thesis: for r being Real st g is_differentiable_in y0 holds
( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )
let r be Real; ::_thesis: ( g is_differentiable_in y0 implies ( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) ) )
assume A1: g is_differentiable_in y0 ; ::_thesis: ( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )
reconsider f = g as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider x0 = y0 as Point of (REAL-NS m) by REAL_NS1:def_4;
f is_differentiable_in x0 by A1, Th2;
then A2: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) by NDIFF_1:37;
r (#) f = r (#) g by Th6;
hence r (#) g is_differentiable_in y0 by A2, Th2; ::_thesis: diff ((r (#) g),y0) = r (#) (diff (g,y0))
then diff ((r (#) g),y0) = diff ((r (#) f),x0) by Th3, Th6;
hence diff ((r (#) g),y0) = r (#) (diff (g,y0)) by A2, Th9, Th3, A1; ::_thesis: verum
end;
theorem Th23: :: PDIFF_6:23
for m being Element of NAT
for x0 being Element of REAL m
for y0 being Point of (REAL-NS m)
for r being Real st x0 = y0 holds
{ y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r }
proof
let m be Element of NAT ; ::_thesis: for x0 being Element of REAL m
for y0 being Point of (REAL-NS m)
for r being Real st x0 = y0 holds
{ y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r }
let x0 be Element of REAL m; ::_thesis: for y0 being Point of (REAL-NS m)
for r being Real st x0 = y0 holds
{ y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r }
let y0 be Point of (REAL-NS m); ::_thesis: for r being Real st x0 = y0 holds
{ y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r }
let r be Real; ::_thesis: ( x0 = y0 implies { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } )
assume A1: x0 = y0 ; ::_thesis: { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r }
now__::_thesis:_for_w_being_set_st_w_in__{__y_where_y_is_Element_of_REAL_m_:_|.(y_-_x0).|_<_r__}__holds_
w_in__{__z1_where_z1_is_Point_of_(REAL-NS_m)_:_||.(z1_-_y0).||_<_r__}_
let w be set ; ::_thesis: ( w in { y where y is Element of REAL m : |.(y - x0).| < r } implies w in { z1 where z1 is Point of (REAL-NS m) : ||.(z1 - y0).|| < r } )
assume w in { y where y is Element of REAL m : |.(y - x0).| < r } ; ::_thesis: w in { z1 where z1 is Point of (REAL-NS m) : ||.(z1 - y0).|| < r }
then consider y being Element of REAL m such that
A2: ( y = w & |.(y - x0).| < r ) ;
reconsider z = y as Point of (REAL-NS m) by REAL_NS1:def_4;
||.(z - y0).|| < r by A1, A2, REAL_NS1:1, REAL_NS1:5;
hence w in { z1 where z1 is Point of (REAL-NS m) : ||.(z1 - y0).|| < r } by A2; ::_thesis: verum
end;
then A3: { y where y is Element of REAL m : |.(y - x0).| < r } c= { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } by TARSKI:def_3;
now__::_thesis:_for_w_being_set_st_w_in__{__z_where_z_is_Point_of_(REAL-NS_m)_:_||.(z_-_y0).||_<_r__}__holds_
w_in__{__z1_where_z1_is_Element_of_REAL_m_:_|.(z1_-_x0).|_<_r__}_
let w be set ; ::_thesis: ( w in { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } implies w in { z1 where z1 is Element of REAL m : |.(z1 - x0).| < r } )
assume w in { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } ; ::_thesis: w in { z1 where z1 is Element of REAL m : |.(z1 - x0).| < r }
then consider y being Point of (REAL-NS m) such that
A4: ( y = w & ||.(y - y0).|| < r ) ;
reconsider z = y as Element of REAL m by REAL_NS1:def_4;
|.(z - x0).| < r by A1, A4, REAL_NS1:1, REAL_NS1:5;
hence w in { z1 where z1 is Element of REAL m : |.(z1 - x0).| < r } by A4; ::_thesis: verum
end;
then { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } c= { y where y is Element of REAL m : |.(y - x0).| < r } by TARSKI:def_3;
hence { y where y is Element of REAL m : |.(y - x0).| < r } = { z where z is Point of (REAL-NS m) : ||.(z - y0).|| < r } by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th24: :: PDIFF_6:24
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m
for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) holds
( f is_differentiable_in x0 & diff (f,x0) = L )
proof
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m
for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) holds
( f is_differentiable_in x0 & diff (f,x0) = L )
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for x0 being Element of REAL m
for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) holds
( f is_differentiable_in x0 & diff (f,x0) = L )
let x0 be Element of REAL m; ::_thesis: for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) holds
( f is_differentiable_in x0 & diff (f,x0) = L )
let L, R be Function of (REAL m),(REAL n); ::_thesis: ( L is LinearOperator of m,n & ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) implies ( f is_differentiable_in x0 & diff (f,x0) = L ) )
reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def_4;
assume A1: ( L is LinearOperator of m,n & ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ; ::_thesis: ( f is_differentiable_in x0 & diff (f,x0) = L )
then consider r0 being Real such that
A2: ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ;
L is LinearOperator of (REAL-NS m),(REAL-NS n) by A1, Th14;
then reconsider GL = L as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) by LOPBAN_1:def_9;
( REAL m = the carrier of (REAL-NS m) & REAL n = the carrier of (REAL-NS n) ) by REAL_NS1:def_4;
then reconsider GR = R as Function of (REAL-NS m),(REAL-NS n) ;
the carrier of (REAL-NS m) = REAL m by REAL_NS1:def_4;
then A3: dom R = the carrier of (REAL-NS m) by FUNCT_2:def_1;
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_d_being_Real_st_
(_d_>_0_&_(_for_z_being_Point_of_(REAL-NS_m)_st_z_<>_0._(REAL-NS_m)_&_||.z.||_<_d_holds_
(||.z.||_")_*_||.(GR_/._z).||_<_r_)_)
let r be Real; ::_thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(GR /. z).|| < r ) ) )
assume r > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(GR /. z).|| < r ) )
then consider d being Real such that
A4: ( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) by A2;
take d = d; ::_thesis: ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(GR /. z).|| < r ) )
thus d > 0 by A4; ::_thesis: for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(GR /. z).|| < r
thus for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(GR /. z).|| < r ::_thesis: verum
proof
let z be Point of (REAL-NS m); ::_thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < d implies (||.z.|| ") * ||.(GR /. z).|| < r )
assume A5: ( z <> 0. (REAL-NS m) & ||.z.|| < d ) ; ::_thesis: (||.z.|| ") * ||.(GR /. z).|| < r
reconsider s = z as Element of REAL m by REAL_NS1:def_4;
reconsider w = R . s as Element of REAL n ;
A6: s <> 0* m by A5, REAL_NS1:def_4;
|.s.| < d by A5, REAL_NS1:1;
then (|.s.| ") * |.w.| < r by A4, A6;
then (||.z.|| ") * |.w.| < r by REAL_NS1:1;
hence (||.z.|| ") * ||.(GR /. z).|| < r by REAL_NS1:1; ::_thesis: verum
end;
end;
then reconsider GR = GR as RestFunc of (REAL-NS m),(REAL-NS n) by NDIFF_1:23;
set N = { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } ;
reconsider N = { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } as Neighbourhood of y0 by A2, NFCONT_1:3;
A7: N c= dom g by A2, Th23;
A8: for y being Point of (REAL-NS m) st y in N holds
(g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0))
proof
let y be Point of (REAL-NS m); ::_thesis: ( y in N implies (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) )
assume A9: y in N ; ::_thesis: (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0))
reconsider x = y as Element of REAL m by REAL_NS1:def_4;
x in { s where s is Element of REAL m : |.(s - x0).| < r0 } by A9, Th23;
then ex s being Element of REAL m st
( s = x & |.(s - x0).| < r0 ) ;
then A10: (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) by A2;
A11: y0 in N by NFCONT_1:4;
then ( f /. x = f . x & f /. x0 = f . x0 ) by A9, A7, PARTFUN1:def_6;
then A12: ( f /. x = g /. y & f /. x0 = g /. y0 ) by A9, A11, A7, PARTFUN1:def_6;
x - x0 = y - y0 by REAL_NS1:5;
then ( L . (x - x0) = GL . (y - y0) & R . (x - x0) = GR /. (y - y0) ) by A3, PARTFUN1:def_6;
then (L . (x - x0)) + (R . (x - x0)) = (GL . (y - y0)) + (GR /. (y - y0)) by REAL_NS1:2;
hence (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) by A10, A12, REAL_NS1:5; ::_thesis: verum
end;
then A13: g is_differentiable_in y0 by A7, NDIFF_1:def_6;
hence A14: f is_differentiable_in x0 by Th2; ::_thesis: diff (f,x0) = L
diff (g,y0) = GL by A13, A8, A7, NDIFF_1:def_7;
hence diff (f,x0) = L by Th3, A14; ::_thesis: verum
end;
theorem :: PDIFF_6:25
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m holds
( f is_differentiable_in x0 iff ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
proof
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m holds
( f is_differentiable_in x0 iff ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for x0 being Element of REAL m holds
( f is_differentiable_in x0 iff ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
let x0 be Element of REAL m; ::_thesis: ( f is_differentiable_in x0 iff ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def_4;
hereby ::_thesis: ( ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) implies f is_differentiable_in x0 )
assume f is_differentiable_in x0 ; ::_thesis: ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
then g is_differentiable_in y0 by Th2;
then consider N being Neighbourhood of y0 such that
A1: ( N c= dom g & ex GL being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) ex GR being RestFunc of (REAL-NS m),(REAL-NS n) st
for y being Point of (REAL-NS m) st y in N holds
(g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) ) by NDIFF_1:def_6;
consider GL being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))), GR being RestFunc of (REAL-NS m),(REAL-NS n) such that
A2: for y being Point of (REAL-NS m) st y in N holds
(g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) by A1;
consider r0 being Real such that
A3: ( 0 < r0 & { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } c= N ) by NFCONT_1:def_1;
take r0 = r0; ::_thesis: ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
thus 0 < r0 by A3; ::_thesis: ( { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
{ y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } c= dom g by A3, A1, XBOOLE_1:1;
hence { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f by Th23; ::_thesis: ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) )
A4: GR is total by NDIFF_1:def_5;
then A5: dom GR = the carrier of (REAL-NS m) by PARTFUN1:def_2;
A6: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4;
then reconsider L = GL as Function of (REAL m),(REAL n) by LOPBAN_1:def_9;
reconsider R = GR as Function of (REAL m),(REAL n) by A6, A4;
take L = L; ::_thesis: ex R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) )
take R = R; ::_thesis: ( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) )
GL is LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9;
hence L is LinearOperator of m,n by Th14; ::_thesis: ( ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) )
thus for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ::_thesis: for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0))
proof
let r be Real; ::_thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) )
assume r > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) )
then consider d being Real such that
A7: ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(GR /. z).|| < r ) ) by A4, NDIFF_1:23;
take d ; ::_thesis: ( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) )
thus d > 0 by A7; ::_thesis: for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r
let z be Element of REAL m; ::_thesis: for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r
let w be Element of REAL n; ::_thesis: ( z <> 0* m & |.z.| < d & w = R . z implies (|.z.| ") * |.w.| < r )
assume A8: ( z <> 0* m & |.z.| < d & w = R . z ) ; ::_thesis: (|.z.| ") * |.w.| < r
reconsider s = z as Element of (REAL-NS m) by REAL_NS1:def_4;
A9: s <> 0. (REAL-NS m) by A8, REAL_NS1:def_4;
||.s.|| < d by A8, REAL_NS1:1;
then (||.s.|| ") * ||.(GR /. s).|| < r by A7, A9;
then (|.z.| ") * ||.(GR /. s).|| < r by REAL_NS1:1;
hence (|.z.| ") * |.w.| < r by A5, A8, PARTFUN1:def_6, REAL_NS1:1; ::_thesis: verum
end;
thus for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ::_thesis: verum
proof
let x be Element of REAL m; ::_thesis: ( |.(x - x0).| < r0 implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) )
assume |.(x - x0).| < r0 ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0))
then x in { s where s is Element of REAL m : |.(s - x0).| < r0 } ;
then A10: x in { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } by Th23;
reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def_4;
A11: (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) by A3, A10, A2;
A12: ( y in N & y0 in N ) by A3, A10, NFCONT_1:4;
then ( f /. x = f . x & f /. x0 = f . x0 ) by A1, PARTFUN1:def_6;
then A13: ( f /. x = g /. y & f /. x0 = g /. y0 ) by A12, A1, PARTFUN1:def_6;
x - x0 = y - y0 by REAL_NS1:5;
then ( L . (x - x0) = GL . (y - y0) & R . (x - x0) = GR /. (y - y0) ) by A5, PARTFUN1:def_6;
then (L . (x - x0)) + (R . (x - x0)) = (GL . (y - y0)) + (GR /. (y - y0)) by REAL_NS1:2;
hence (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) by A11, A13, REAL_NS1:5; ::_thesis: verum
end;
end;
assume ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ; ::_thesis: f is_differentiable_in x0
hence f is_differentiable_in x0 by Th24; ::_thesis: verum
end;
begin
theorem Th26: :: PDIFF_6:26
for n, i being Element of NAT
for y1, y2 being Point of (REAL-NS n) holds (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2)
proof
let n, i be Element of NAT ; ::_thesis: for y1, y2 being Point of (REAL-NS n) holds (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2)
let y1, y2 be Point of (REAL-NS n); ::_thesis: (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2)
reconsider yy1 = y1, yy2 = y2 as Element of REAL n by REAL_NS1:def_4;
reconsider ry1 = yy1 . i as Element of REAL ;
reconsider ry2 = yy2 . i as Element of REAL ;
( (Proj (i,n)) . y1 = <*((proj (i,n)) . y1)*> & (Proj (i,n)) . y2 = <*((proj (i,n)) . y2)*> ) by PDIFF_1:def_4;
then A1: ( (Proj (i,n)) . y1 = <*ry1*> & (Proj (i,n)) . y2 = <*ry2*> ) by PDIFF_1:def_1;
A2: ( <*ry1*> is Element of REAL 1 & <*ry2*> is Element of REAL 1 ) by FINSEQ_2:98;
(Proj (i,n)) . (y1 + y2) = <*((proj (i,n)) . (y1 + y2))*> by PDIFF_1:def_4
.= <*((proj (i,n)) . (yy1 + yy2))*> by REAL_NS1:2
.= <*((yy1 + yy2) . i)*> by PDIFF_1:def_1
.= <*((yy1 . i) + (yy2 . i))*> by RVSUM_1:11
.= <*ry1*> + <*ry2*> by RVSUM_1:13 ;
hence (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2) by A1, A2, REAL_NS1:2; ::_thesis: verum
end;
theorem Th27: :: PDIFF_6:27
for n, i being Element of NAT
for y1 being Point of (REAL-NS n)
for r being Real holds (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1)
proof
let n, i be Element of NAT ; ::_thesis: for y1 being Point of (REAL-NS n)
for r being Real holds (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1)
let y1 be Point of (REAL-NS n); ::_thesis: for r being Real holds (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1)
let r be Real; ::_thesis: (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1)
reconsider yy1 = y1 as Element of REAL n by REAL_NS1:def_4;
reconsider y1i = yy1 . i as Element of REAL ;
(Proj (i,n)) . y1 = <*((proj (i,n)) . y1)*> by PDIFF_1:def_4;
then A1: (Proj (i,n)) . y1 = <*y1i*> by PDIFF_1:def_1;
A2: <*y1i*> is Element of REAL 1 by FINSEQ_2:98;
(Proj (i,n)) . (r * y1) = <*((proj (i,n)) . (r * y1))*> by PDIFF_1:def_4
.= <*((proj (i,n)) . (r * yy1))*> by REAL_NS1:3
.= <*((r * yy1) . i)*> by PDIFF_1:def_1
.= <*(r * (yy1 . i))*> by RVSUM_1:44
.= r * <*y1i*> by RVSUM_1:47 ;
hence (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1) by A1, A2, REAL_NS1:3; ::_thesis: verum
end;
theorem Th28: :: PDIFF_6:28
for m, n being non empty Element of NAT
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m)
for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds
( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
proof
let m, n be non empty Element of NAT ; ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m)
for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds
( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x0 being Point of (REAL-NS m)
for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds
( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
let x0 be Point of (REAL-NS m); ::_thesis: for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds
( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n & g is_differentiable_in x0 implies ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) ) )
assume A1: ( 1 <= i & i <= n & g is_differentiable_in x0 ) ; ::_thesis: ( (Proj (i,n)) * g is_differentiable_in x0 & (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
then consider N being Neighbourhood of x0 such that
A2: ( N c= dom g & ex GR being RestFunc of (REAL-NS m),(REAL-NS n) st
for x being Point of (REAL-NS m) st x in N holds
(g /. x) - (g /. x0) = ((diff (g,x0)) . (x - x0)) + (GR /. (x - x0)) ) by NDIFF_1:def_7;
consider GR being RestFunc of (REAL-NS m),(REAL-NS n) such that
A3: for x being Point of (REAL-NS m) st x in N holds
(g /. x) - (g /. x0) = ((diff (g,x0)) . (x - x0)) + (GR /. (x - x0)) by A2;
set RLB0 = R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1));
reconsider DFG = diff (g,x0) as LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def_9;
reconsider PG = Proj (i,n) as Function of the carrier of (REAL-NS n), the carrier of (REAL-NS 1) ;
PG * DFG is Function of the carrier of (REAL-NS m), the carrier of (REAL-NS 1) ;
then reconsider L = (Proj (i,n)) * (diff (g,x0)) as Function of (REAL-NS m),(REAL-NS 1) ;
A4: for x, y being VECTOR of (REAL-NS m) holds L . (x + y) = (L . x) + (L . y)
proof
let x, y be VECTOR of (REAL-NS m); ::_thesis: L . (x + y) = (L . x) + (L . y)
A5: dom L = the carrier of (REAL-NS m) by FUNCT_2:def_1;
A6: DFG . (x + y) = (DFG . x) + (DFG . y) by VECTSP_1:def_20;
L . (x + y) = (Proj (i,n)) . (DFG . (x + y)) by A5, FUNCT_1:12
.= ((Proj (i,n)) . (DFG . x)) + ((Proj (i,n)) . (DFG . y)) by A6, Th26
.= ((Proj (i,n)) . (DFG . x)) + (L . y) by A5, FUNCT_1:12 ;
hence L . (x + y) = (L . x) + (L . y) by A5, FUNCT_1:12; ::_thesis: verum
end;
for x being VECTOR of (REAL-NS m)
for r being Real holds L . (r * x) = r * (L . x)
proof
let x be VECTOR of (REAL-NS m); ::_thesis: for r being Real holds L . (r * x) = r * (L . x)
let r be Real; ::_thesis: L . (r * x) = r * (L . x)
A7: dom L = the carrier of (REAL-NS m) by FUNCT_2:def_1;
DFG . (r * x) = r * (DFG . x) by LOPBAN_1:def_5;
then (Proj (i,n)) . (DFG . (r * x)) = r * ((Proj (i,n)) . (DFG . x)) by Th27;
then L . (r * x) = r * ((Proj (i,n)) . (DFG . x)) by A7, FUNCT_1:12;
hence L . (r * x) = r * (L . x) by A7, FUNCT_1:12; ::_thesis: verum
end;
then reconsider L = L as LinearOperator of (REAL-NS m),(REAL-NS 1) by A4, VECTSP_1:def_20, LOPBAN_1:def_5;
reconsider L = L as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) by LOPBAN_1:def_9;
A8: GR is total by NDIFF_1:def_5;
then reconsider FGR = GR as Function of the carrier of (REAL-NS m), the carrier of (REAL-NS n) ;
A9: (Proj (i,n)) * FGR is Function of the carrier of (REAL-NS m), the carrier of (REAL-NS 1) ;
(Proj (i,n)) * GR is RestFunc of (REAL-NS m),(REAL-NS 1)
proof
A10: dom GR = the carrier of (REAL-NS m) by A8, PARTFUN1:def_2;
reconsider R = (Proj (i,n)) * GR as PartFunc of (REAL-NS m),(REAL-NS 1) ;
for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) )
proof
let r be Real; ::_thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) )
assume r > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) )
then consider d being Real such that
A11: ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(GR /. z).|| < r ) ) by A8, NDIFF_1:23;
take d ; ::_thesis: ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) )
thus d > 0 by A11; ::_thesis: for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r
let z be Point of (REAL-NS m); ::_thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < d implies (||.z.|| ") * ||.(R /. z).|| < r )
assume A12: ( z <> 0. (REAL-NS m) & ||.z.|| < d ) ; ::_thesis: (||.z.|| ") * ||.(R /. z).|| < r
A13: GR /. z = GR . z by A10, PARTFUN1:def_6;
A14: i in Seg n by A1;
reconsider GRz = GR /. z as Point of (REAL-NS n) ;
reconsider GRz1 = GRz as Element of REAL n by REAL_NS1:def_4;
reconsider GRzi = GRz1 . i as Element of REAL ;
dom (Proj (i,n)) = the carrier of (REAL-NS n) by PARTFUN1:def_2;
then A15: z in dom ((Proj (i,n)) * GR) by A10, A13, FUNCT_1:11;
then ((Proj (i,n)) * GR) . z = (Proj (i,n)) . (GR . z) by FUNCT_1:12
.= <*((proj (i,n)) . GRz1)*> by A13, PDIFF_1:def_4 ;
then A16: ((Proj (i,n)) * GR) . z = <*GRzi*> by PDIFF_1:def_1;
A17: abs GRzi <= ||.(GR /. z).|| by A14, REAL_NS1:9;
A18: 0 <= ||.z.|| by NORMSP_1:4;
0 <= abs GRzi by COMPLEX1:46;
then A19: (||.z.|| ") * (abs GRzi) <= (||.z.|| ") * ||.(GR /. z).|| by A17, A18, XREAL_1:66;
(||.z.|| ") * ||.(GR /. z).|| < r by A11, A12;
then A20: (||.z.|| ") * (abs GRzi) < r by A19, XXREAL_0:2;
((Proj (i,n)) * GR) . z in rng ((Proj (i,n)) * GR) by A15, FUNCT_1:3;
then reconsider Rz = ((Proj (i,n)) * GR) . z as VECTOR of (REAL-NS 1) ;
set VGRzi = <*GRzi*>;
<*GRzi*> is Element of REAL 1 by FINSEQ_2:98;
then ||.Rz.|| = |.<*GRzi*>.| by A16, REAL_NS1:1;
then (||.z.|| ") * ||.Rz.|| < r by A20, JORDAN2C:10;
hence (||.z.|| ") * ||.(R /. z).|| < r by A15, PARTFUN1:def_6; ::_thesis: verum
end;
hence (Proj (i,n)) * GR is RestFunc of (REAL-NS m),(REAL-NS 1) by A9, NDIFF_1:23; ::_thesis: verum
end;
then reconsider R = (Proj (i,n)) * GR as RestFunc of (REAL-NS m),(REAL-NS 1) ;
set pg = (Proj (i,n)) * g;
A21: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1;
then rng g c= dom (Proj (i,n)) ;
then A22: dom g = dom ((Proj (i,n)) * g) by RELAT_1:27;
A23: dom (Proj (i,n)) = REAL n by A21, REAL_NS1:def_4;
A24: for x being Point of (REAL-NS m) st x in N holds
(((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Point of (REAL-NS m); ::_thesis: ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
now__::_thesis:_(_x_in_N_&_x_in_N_implies_(((Proj_(i,n))_*_g)_/._x)_-_(((Proj_(i,n))_*_g)_/._x0)_=_(L_._(x_-_x0))_+_(R_/._(x_-_x0))_)
assume A25: x in N ; ::_thesis: ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
then A26: (g /. x) - (g /. x0) = ((diff (g,x0)) . (x - x0)) + (GR /. (x - x0)) by A3;
A27: x0 in N by NFCONT_1:4;
then A28: ( ((Proj (i,n)) * g) /. x = ((Proj (i,n)) * g) . x & ((Proj (i,n)) * g) /. x0 = ((Proj (i,n)) * g) . x0 ) by A2, A22, A25, PARTFUN1:def_6;
A29: ( g /. x = g . x & g /. x0 = g . x0 ) by A2, A25, A27, PARTFUN1:def_6;
reconsider PGSx = (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) as Element of REAL 1 by REAL_NS1:def_4;
((Proj (i,n)) * g) . x in rng ((Proj (i,n)) * g) by A2, A22, A25, FUNCT_1:3;
then reconsider PGdx = ((Proj (i,n)) * g) . x as Element of REAL 1 by REAL_NS1:def_4;
((Proj (i,n)) * g) . x0 in rng ((Proj (i,n)) * g) by A2, A22, A27, FUNCT_1:3;
then reconsider PGdx0 = ((Proj (i,n)) * g) . x0 as Element of REAL 1 by REAL_NS1:def_4;
g . x in rng g by A2, A25, FUNCT_1:3;
then reconsider Gx = g . x as Element of REAL n by REAL_NS1:def_4;
g . x0 in rng g by A2, A27, FUNCT_1:3;
then reconsider Gx0 = g . x0 as Element of REAL n by REAL_NS1:def_4;
set ProjGx = (Proj (i,n)) . (g . x);
Gx in dom (Proj (i,n)) by A23;
then (Proj (i,n)) . (g . x) in rng (Proj (i,n)) by FUNCT_1:3;
then reconsider ProjGx = (Proj (i,n)) . (g . x) as Element of REAL 1 by REAL_NS1:def_4;
set ProjGx0 = (Proj (i,n)) . (g . x0);
Gx0 in dom (Proj (i,n)) by A23;
then (Proj (i,n)) . (g . x0) in rng (Proj (i,n)) by FUNCT_1:3;
then reconsider ProjGx0 = (Proj (i,n)) . (g . x0) as Element of REAL 1 by REAL_NS1:def_4;
reconsider Gx1 = Gx as Element of (REAL-NS n) by REAL_NS1:def_4;
reconsider Gx01 = Gx0 as Element of (REAL-NS n) by REAL_NS1:def_4;
reconsider Gsx = g /. x as Element of REAL n by REAL_NS1:def_4;
reconsider Gsx0 = g /. x0 as Element of REAL n by REAL_NS1:def_4;
set dxx0 = x - x0;
reconsider Ldxx0 = L . (x - x0) as Element of (REAL-NS 1) ;
A30: dom R = the carrier of (REAL-NS m) by A9, PARTFUN1:def_2;
then A31: R /. (x - x0) = R . (x - x0) by PARTFUN1:def_6;
then reconsider Rdxx0 = R . (x - x0) as Element of (REAL-NS 1) ;
reconsider Ldiff = (diff (g,x0)) . (x - x0) as Element of REAL n by REAL_NS1:def_4;
set ProjLdiff = (Proj (i,n)) . Ldiff;
(Proj (i,n)) . Ldiff in rng (Proj (i,n)) by A21, FUNCT_1:3;
then reconsider ProjLdiff = (Proj (i,n)) . Ldiff as Element of REAL 1 by REAL_NS1:def_4;
A32: dom GR = the carrier of (REAL-NS m) by A8, PARTFUN1:def_2;
then GR . (x - x0) in rng GR by FUNCT_1:3;
then reconsider Rdiff = GR . (x - x0) as Element of REAL n by REAL_NS1:def_4;
A33: Rdiff = GR /. (x - x0) by A32, PARTFUN1:def_6;
set ProjRdiff = (Proj (i,n)) . Rdiff;
(Proj (i,n)) . Rdiff in rng (Proj (i,n)) by A23, FUNCT_1:3;
then reconsider ProjRdiff = (Proj (i,n)) . Rdiff as Element of REAL 1 by REAL_NS1:def_4;
dom L = the carrier of (REAL-NS m) by FUNCT_2:def_1;
then ( L . (x - x0) = (Proj (i,n)) . Ldiff & R . (x - x0) = (Proj (i,n)) . Rdiff ) by A30, FUNCT_1:12;
then A34: Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff by REAL_NS1:2;
(Proj (i,n)) . Ldiff = <*((proj (i,n)) . Ldiff)*> by PDIFF_1:def_4;
then A35: (Proj (i,n)) . Ldiff = <*(Ldiff . i)*> by PDIFF_1:def_1;
Rdiff in dom (Proj (i,n)) by A23;
then (Proj (i,n)) . Rdiff = <*((proj (i,n)) . Rdiff)*> by PDIFF_1:def_4;
then A36: (Proj (i,n)) . Rdiff = <*(Rdiff . i)*> by PDIFF_1:def_1;
reconsider diffGR = ((diff (g,x0)) . (x - x0)) + (GR /. (x - x0)) as Element of REAL n by REAL_NS1:def_4;
reconsider Rsdiff = GR /. (x - x0) as Element of REAL n by REAL_NS1:def_4;
PGSx = PGdx - PGdx0 by A28, REAL_NS1:5
.= ProjGx - PGdx0 by A2, A22, A25, FUNCT_1:12
.= ProjGx - ProjGx0 by A2, A22, A27, FUNCT_1:12
.= <*((proj (i,n)) . Gx1)*> - ProjGx0 by PDIFF_1:def_4
.= <*((proj (i,n)) . Gx1)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def_4
.= <*(Gx . i)*> - <*((proj (i,n)) . Gx01)*> by PDIFF_1:def_1
.= <*(Gx . i)*> - <*(Gx0 . i)*> by PDIFF_1:def_1
.= <*((Gx . i) - (Gx0 . i))*> by RVSUM_1:29
.= <*((Gsx - Gsx0) . i)*> by A29, RVSUM_1:27
.= <*(diffGR . i)*> by A26, REAL_NS1:5
.= <*((Ldiff + Rsdiff) . i)*> by REAL_NS1:2
.= <*((Ldiff . i) + (Rsdiff . i))*> by RVSUM_1:11 ;
hence ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by A31, A34, A35, A36, A33, RVSUM_1:13; ::_thesis: verum
end;
hence ( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ; ::_thesis: verum
end;
hence (Proj (i,n)) * g is_differentiable_in x0 by A2, A22, NDIFF_1:def_6; ::_thesis: (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0)
hence (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) by A2, A22, A24, NDIFF_1:def_7; ::_thesis: verum
end;
theorem :: PDIFF_6:29
for m, n being non empty Element of NAT
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m) holds
( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
proof
let m, n be non empty Element of NAT ; ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m) holds
( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: for x0 being Point of (REAL-NS m) holds
( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
let x0 be Point of (REAL-NS m); ::_thesis: ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
set RB = R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n));
( ( for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ) implies g is_differentiable_in x0 )
proof
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ; ::_thesis: g is_differentiable_in x0
defpred S1[ Element of NAT , Element of REAL ] means ( $2 > 0 & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < $2 } c= dom ((Proj ($1,n)) * g) & ex Ri being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < $2 } holds
(((Proj ($1,n)) * g) /. x) - (((Proj ($1,n)) * g) /. x0) = ((diff (((Proj ($1,n)) * g),x0)) . (x - x0)) + (Ri /. (x - x0)) );
A2: for k being Element of NAT st k in Seg n holds
ex dk being Element of REAL st S1[k,dk]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg n implies ex dk being Element of REAL st S1[k,dk] )
assume k in Seg n ; ::_thesis: ex dk being Element of REAL st S1[k,dk]
then ( 1 <= k & k <= n ) by FINSEQ_1:1;
then (Proj (k,n)) * g is_differentiable_in x0 by A1;
then consider Nk being Neighbourhood of x0 such that
A3: ( Nk c= dom ((Proj (k,n)) * g) & ex Rk being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) ) by NDIFF_1:def_7;
consider dk being Real such that
A4: ( 0 < dk & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= Nk ) by NFCONT_1:def_1;
reconsider dk = dk as Element of REAL ;
take dk ; ::_thesis: S1[k,dk]
thus 0 < dk by A4; ::_thesis: ( { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= dom ((Proj (k,n)) * g) & ex Ri being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Ri /. (x - x0)) )
thus { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } c= dom ((Proj (k,n)) * g) by A4, A3, XBOOLE_1:1; ::_thesis: ex Ri being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Ri /. (x - x0))
thus ex Rk being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) ::_thesis: verum
proof
consider Rk being RestFunc of (REAL-NS m),(REAL-NS 1) such that
A5: for x being Point of (REAL-NS m) st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) by A3;
take Rk ; ::_thesis: for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0))
thus for x being Point of (REAL-NS m) st x in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < dk } holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (Rk /. (x - x0)) by A4, A5; ::_thesis: verum
end;
end;
consider d being FinSequence of REAL such that
A6: ( dom d = Seg n & ( for k being Element of NAT st k in Seg n holds
S1[k,d /. k] ) ) from RECDEF_1:sch_17(A2);
set d0 = min d;
len d = n by A6, FINSEQ_1:def_3;
then A7: min_p d in dom d by RFINSEQ2:def_2;
then d /. (min_p d) > 0 by A6;
then A8: min d > 0 by A7, PARTFUN1:def_6;
defpred S2[ set , set ] means ex y being Element of REAL n st
( $2 = y & ( for i being Element of NAT st i in Seg n holds
y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . $1) ) );
A9: for x being Point of (REAL-NS m) ex y being Point of (REAL-NS n) st S2[x,y]
proof
let x be Point of (REAL-NS m); ::_thesis: ex y being Point of (REAL-NS n) st S2[x,y]
defpred S3[ Element of NAT , set ] means $2 = (proj (1,1)) . ((diff (((Proj ($1,n)) * g),x0)) . x);
A10: for i being Element of NAT st i in Seg n holds
ex r being Element of REAL st S3[i,r] ;
consider y being FinSequence of REAL such that
A11: ( dom y = Seg n & ( for i being Element of NAT st i in Seg n holds
S3[i,y /. i] ) ) from RECDEF_1:sch_17(A10);
len y = n by A11, FINSEQ_1:def_3;
then reconsider y = y as Element of REAL n by FINSEQ_2:92;
A12: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
y_._i_=_(proj_(1,1))_._((diff_(((Proj_(i,n))_*_g),x0))_._x)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) )
assume i in Seg n ; ::_thesis: y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x)
then ( S3[i,y /. i] & y /. i = y . i ) by A11, PARTFUN1:def_6;
hence y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ; ::_thesis: verum
end;
reconsider y0 = y as Point of (REAL-NS n) by REAL_NS1:def_4;
ex y being Element of REAL n st
( y0 = y & ( for i being Element of NAT st i in Seg n holds
y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ) ) by A12;
hence ex y0 being Point of (REAL-NS n) st S2[x,y0] ; ::_thesis: verum
end;
consider L being Function of (REAL-NS m),(REAL-NS n) such that
A13: for x being Point of (REAL-NS m) holds S2[x,L . x] from FUNCT_2:sch_3(A9);
A14: for x, y being VECTOR of (REAL-NS m) holds L . (x + y) = (L . x) + (L . y)
proof
let x, y be VECTOR of (REAL-NS m); ::_thesis: L . (x + y) = (L . x) + (L . y)
consider Lx being Element of REAL n such that
A15: ( L . x = Lx & ( for i being Element of NAT st i in Seg n holds
Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ) ) by A13;
consider Ly being Element of REAL n such that
A16: ( L . y = Ly & ( for i being Element of NAT st i in Seg n holds
Ly . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . y) ) ) by A13;
consider Lxy being Element of REAL n such that
A17: ( L . (x + y) = Lxy & ( for i being Element of NAT st i in Seg n holds
Lxy . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (x + y)) ) ) by A13;
dom Lxy = Seg n by FINSEQ_1:89;
then A18: dom Lxy = dom (Lx + Ly) by FINSEQ_1:89;
for i0 being Nat st i0 in dom Lxy holds
Lxy . i0 = (Lx + Ly) . i0
proof
let i0 be Nat; ::_thesis: ( i0 in dom Lxy implies Lxy . i0 = (Lx + Ly) . i0 )
reconsider i = i0 as Element of NAT by ORDINAL1:def_12;
assume i0 in dom Lxy ; ::_thesis: Lxy . i0 = (Lx + Ly) . i0
then i in Seg n by FINSEQ_1:89;
then A19: ( Lxy . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (x + y)) & Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) & Ly . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . y) ) by A15, A16, A17;
diff (((Proj (i,n)) * g),x0) is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def_9;
then A20: (diff (((Proj (i,n)) * g),x0)) . (x + y) = ((diff (((Proj (i,n)) * g),x0)) . x) + ((diff (((Proj (i,n)) * g),x0)) . y) by VECTSP_1:def_20;
reconsider Diffxy = (diff (((Proj (i,n)) * g),x0)) . (x + y) as Element of REAL 1 by REAL_NS1:def_4;
reconsider Diffx = (diff (((Proj (i,n)) * g),x0)) . x as Element of REAL 1 by REAL_NS1:def_4;
reconsider Diffy = (diff (((Proj (i,n)) * g),x0)) . y as Element of REAL 1 by REAL_NS1:def_4;
Diffxy = Diffx + Diffy by A20, REAL_NS1:2;
then Lxy . i0 = (Diffx + Diffy) . 1 by A19, PDIFF_1:def_1;
then Lxy . i0 = (Diffx . 1) + (Diffy . 1) by RVSUM_1:11;
then Lxy . i0 = (Lx . i0) + (Diffy . 1) by A19, PDIFF_1:def_1;
then Lxy . i0 = (Lx . i0) + (Ly . i0) by A19, PDIFF_1:def_1;
hence Lxy . i0 = (Lx + Ly) . i0 by RVSUM_1:11; ::_thesis: verum
end;
then Lxy = Lx + Ly by A18, FINSEQ_1:13;
hence L . (x + y) = (L . x) + (L . y) by A15, A16, A17, REAL_NS1:2; ::_thesis: verum
end;
for x being VECTOR of (REAL-NS m)
for r being Real holds L . (r * x) = r * (L . x)
proof
let x be VECTOR of (REAL-NS m); ::_thesis: for r being Real holds L . (r * x) = r * (L . x)
let r be Real; ::_thesis: L . (r * x) = r * (L . x)
consider Lx being Element of REAL n such that
A21: ( L . x = Lx & ( for i being Element of NAT st i in Seg n holds
Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) ) ) by A13;
consider Lrx being Element of REAL n such that
A22: ( L . (r * x) = Lrx & ( for i being Element of NAT st i in Seg n holds
Lrx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (r * x)) ) ) by A13;
dom (r * Lx) = Seg n by FINSEQ_1:89;
then A23: dom (r * Lx) = dom Lrx by FINSEQ_1:89;
for i0 being Nat st i0 in dom (r * Lx) holds
(r * Lx) . i0 = Lrx . i0
proof
let i0 be Nat; ::_thesis: ( i0 in dom (r * Lx) implies (r * Lx) . i0 = Lrx . i0 )
reconsider i = i0 as Element of NAT by ORDINAL1:def_12;
assume i0 in dom (r * Lx) ; ::_thesis: (r * Lx) . i0 = Lrx . i0
then i0 in Seg n by FINSEQ_1:89;
then A24: ( Lx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . x) & Lrx . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . (r * x)) ) by A21, A22;
diff (((Proj (i,n)) * g),x0) is LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def_9;
then A25: (diff (((Proj (i,n)) * g),x0)) . (r * x) = r * ((diff (((Proj (i,n)) * g),x0)) . x) by LOPBAN_1:def_5;
reconsider Diffrx = (diff (((Proj (i,n)) * g),x0)) . (r * x) as Element of REAL 1 by REAL_NS1:def_4;
reconsider Diffx = (diff (((Proj (i,n)) * g),x0)) . x as Element of REAL 1 by REAL_NS1:def_4;
Diffrx = r * Diffx by A25, REAL_NS1:3;
then Lrx . i0 = (r * Diffx) . 1 by A24, PDIFF_1:def_1;
then Lrx . i0 = r * (Diffx . 1) by RVSUM_1:45;
then Lrx . i0 = r * (Lx . i0) by A24, PDIFF_1:def_1;
hence (r * Lx) . i0 = Lrx . i0 by RVSUM_1:45; ::_thesis: verum
end;
then r * Lx = Lrx by A23, FINSEQ_1:13;
hence L . (r * x) = r * (L . x) by A21, A22, REAL_NS1:3; ::_thesis: verum
end;
then reconsider L = L as LinearOperator of (REAL-NS m),(REAL-NS n) by A14, VECTSP_1:def_20, LOPBAN_1:def_5;
reconsider L0 = L as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) by LOPBAN_1:def_9;
deffunc H1( Element of (REAL-NS m)) -> Element of the carrier of (REAL-NS n) = ((g /. ($1 + x0)) - (g /. x0)) - (L . $1);
consider R being Function of (REAL-NS m),(REAL-NS n) such that
A26: for x being Element of (REAL-NS m) holds R . x = H1(x) from FUNCT_2:sch_4();
A27: for x being Element of (REAL-NS m)
for i being Element of NAT st i in Seg n & x + x0 in dom g holds
((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x)
proof
let x be Element of (REAL-NS m); ::_thesis: for i being Element of NAT st i in Seg n & x + x0 in dom g holds
((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x)
let i be Element of NAT ; ::_thesis: ( i in Seg n & x + x0 in dom g implies ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) )
assume that
A28: i in Seg n and
A29: x + x0 in dom g ; ::_thesis: ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x)
x0 - x0 = 0. (REAL-NS m) by RLVECT_1:15;
then x0 - x0 = 0* m by REAL_NS1:def_4;
then ||.(x0 - x0).|| = |.(0* m).| by REAL_NS1:1;
then A30: ||.(x0 - x0).|| = 0 by EUCLID:7;
A31: ( 0 < d /. i & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d /. i } c= dom ((Proj (i,n)) * g) ) by A28, A6;
then x0 in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d /. i } by A30;
then A32: x0 in dom ((Proj (i,n)) * g) by A31;
A33: dom ((Proj (i,n)) * g) c= dom g by RELAT_1:25;
reconsider gxx0 = g /. (x + x0), gx0 = g /. x0, Lx = L . x as Element of REAL n by REAL_NS1:def_4;
reconsider Lx1 = L . x as Point of (REAL-NS n) ;
A34: ( - gx0 = (- 1) * (g /. x0) & - Lx = (- 1) * (L . x) ) by REAL_NS1:3;
then gxx0 + (- gx0) = (g /. (x + x0)) + ((- 1) * (g /. x0)) by REAL_NS1:2;
then A35: (gxx0 + (- gx0)) + (- Lx) = ((g /. (x + x0)) + ((- 1) * (g /. x0))) + ((- 1) * (L . x)) by A34, REAL_NS1:2;
gxx0 - gx0 = (g /. (x + x0)) - (g /. x0) by REAL_NS1:5;
then A36: ((g /. (x + x0)) - (g /. x0)) - (L . x) = (gxx0 - gx0) - Lx by REAL_NS1:5;
((Proj (i,n)) * R) . x = (Proj (i,n)) . (R . x) by FUNCT_2:15;
then ((Proj (i,n)) * R) . x = (Proj (i,n)) . (((g /. (x + x0)) - (g /. x0)) - (L . x)) by A26;
then ((Proj (i,n)) * R) . x = ((Proj (i,n)) . ((g /. (x + x0)) + ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by A36, A35, Th26;
then A37: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + ((Proj (i,n)) . ((- 1) * (g /. x0)))) + ((Proj (i,n)) . ((- 1) * (L . x))) by Th26;
( (Proj (i,n)) . ((- 1) * (g /. x0)) = (- 1) * ((Proj (i,n)) . (g /. x0)) & (Proj (i,n)) . ((- 1) * Lx1) = (- 1) * ((Proj (i,n)) . Lx1) ) by Th27;
then ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + (- ((Proj (i,n)) . (g /. x0)))) + ((- 1) * ((Proj (i,n)) . (L . x))) by A37, RLVECT_1:16;
then ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) + (- ((Proj (i,n)) . (g /. x0)))) + (- ((Proj (i,n)) . (L . x))) by RLVECT_1:16;
then ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) - ((Proj (i,n)) . (g /. x0))) + (- ((Proj (i,n)) . (L . x))) by RLVECT_1:def_11;
then A38: ((Proj (i,n)) * R) . x = (((Proj (i,n)) . (g /. (x + x0))) - ((Proj (i,n)) . (g /. x0))) - ((Proj (i,n)) . (L . x)) by RLVECT_1:def_11;
( g /. (x + x0) in the carrier of (REAL-NS n) & g /. x0 in the carrier of (REAL-NS n) ) ;
then A39: ( g /. (x + x0) in dom (Proj (i,n)) & g /. x0 in dom (Proj (i,n)) ) by FUNCT_2:def_1;
A40: (Proj (i,n)) . (g /. (x + x0)) = (Proj (i,n)) /. (g /. (x + x0))
.= ((Proj (i,n)) * g) /. (x + x0) by A29, A39, PARTFUN2:4 ;
(Proj (i,n)) . (g /. x0) = (Proj (i,n)) /. (g /. x0)
.= ((Proj (i,n)) * g) /. x0 by A32, A33, A39, PARTFUN2:4 ;
hence ((Proj (i,n)) * R) . x = ((((Proj (i,n)) * g) /. (x + x0)) - (((Proj (i,n)) * g) /. x0)) - (((Proj (i,n)) * L) . x) by A38, A40, FUNCT_2:15; ::_thesis: verum
end;
for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) )
proof
let r be Real; ::_thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) )
assume A41: r > 0 ; ::_thesis: ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) )
set r0 = ((sqrt n) ") * r;
A42: sqrt n > 0 by SQUARE_1:25;
then A43: ((sqrt n) ") * r > 0 by A41, XREAL_1:129;
defpred S3[ Element of NAT , Element of REAL ] means ( $2 > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < $2 holds
(||.z.|| ") * ||.(((Proj ($1,n)) * R) /. z).|| < ((sqrt n) ") * r ) );
A44: for k being Element of NAT st k in Seg n holds
ex dd being Element of REAL st S3[k,dd]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg n implies ex dd being Element of REAL st S3[k,dd] )
assume A45: k in Seg n ; ::_thesis: ex dd being Element of REAL st S3[k,dd]
then ( 1 <= k & k <= n ) by FINSEQ_1:1;
then (Proj (k,n)) * g is_differentiable_in x0 by A1;
then consider Nk being Neighbourhood of x0 such that
A46: ( Nk c= dom ((Proj (k,n)) * g) & ex PR being RestFunc of (REAL-NS m),(REAL-NS 1) st
for x being Point of (REAL-NS m) st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (PR /. (x - x0)) ) by NDIFF_1:def_7;
consider d0 being Real such that
A47: ( 0 < d0 & { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d0 } c= Nk ) by NFCONT_1:def_1;
consider PR being RestFunc of (REAL-NS m),(REAL-NS 1) such that
A48: for x being Point of (REAL-NS m) st x in Nk holds
(((Proj (k,n)) * g) /. x) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . (x - x0)) + (PR /. (x - x0)) by A46;
PR is total by NDIFF_1:def_5;
then consider d1 being Real such that
A49: ( d1 > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d1 holds
(||.z.|| ") * ||.(PR /. z).|| < ((sqrt n) ") * r ) ) by A43, NDIFF_1:23;
set dd = min (d0,d1);
take min (d0,d1) ; ::_thesis: S3[k, min (d0,d1)]
for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min (d0,d1) holds
(||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r
proof
let z be Point of (REAL-NS m); ::_thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < min (d0,d1) implies (||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r )
assume A50: ( z <> 0. (REAL-NS m) & ||.z.|| < min (d0,d1) ) ; ::_thesis: (||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r
min (d0,d1) <= d1 by XXREAL_0:17;
then ||.z.|| < d1 by A50, XXREAL_0:2;
then A51: (||.z.|| ") * ||.(PR /. z).|| < ((sqrt n) ") * r by A50, A49;
min (d0,d1) <= d0 by XXREAL_0:17;
then A52: ||.z.|| < d0 by A50, XXREAL_0:2;
A53: (z + x0) - x0 = z by RLVECT_4:1;
then A54: z + x0 in { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < d0 } by A52;
then z + x0 in Nk by A47;
then A55: z + x0 in dom ((Proj (k,n)) * g) by A46;
(((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0) = ((diff (((Proj (k,n)) * g),x0)) . ((z + x0) - x0)) + (PR /. ((z + x0) - x0)) by A54, A47, A48;
then A56: PR /. z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - ((diff (((Proj (k,n)) * g),x0)) . z) by A53, RLVECT_4:1;
dom ((Proj (k,n)) * g) c= dom g by RELAT_1:25;
then A57: ((Proj (k,n)) * R) . z = ((((Proj (k,n)) * g) /. (z + x0)) - (((Proj (k,n)) * g) /. x0)) - (((Proj (k,n)) * L) . z) by A55, A45, A27;
consider y being Element of REAL n such that
A58: ( L . z = y & ( for i being Element of NAT st i in Seg n holds
y . i = (proj (1,1)) . ((diff (((Proj (i,n)) * g),x0)) . z) ) ) by A13;
A59: y . k = (proj (1,1)) . ((diff (((Proj (k,n)) * g),x0)) . z) by A58, A45;
(diff (((Proj (k,n)) * g),x0)) . z is Element of REAL 1 by REAL_NS1:def_4;
then consider Dk being Element of REAL such that
A60: (diff (((Proj (k,n)) * g),x0)) . z = <*Dk*> by FINSEQ_2:97;
reconsider y1 = y as Point of (REAL-NS n) by REAL_NS1:def_4;
dom L = the carrier of (REAL-NS m) by FUNCT_2:def_1;
then ((Proj (k,n)) * L) . z = (Proj (k,n)) . (L . z) by FUNCT_1:13;
then ((Proj (k,n)) * L) . z = <*((proj (k,n)) . y1)*> by A58, PDIFF_1:def_4;
then ((Proj (k,n)) * L) . z = <*((proj (1,1)) . ((diff (((Proj (k,n)) * g),x0)) . z))*> by A59, PDIFF_1:def_1;
hence (||.z.|| ") * ||.(((Proj (k,n)) * R) /. z).|| < ((sqrt n) ") * r by A51, A56, A57, A60, PDIFF_1:1; ::_thesis: verum
end;
hence S3[k, min (d0,d1)] by A47, A49, XXREAL_0:21; ::_thesis: verum
end;
consider dd being FinSequence of REAL such that
A61: ( dom dd = Seg n & ( for i being Element of NAT st i in Seg n holds
S3[i,dd /. i] ) ) from RECDEF_1:sch_17(A44);
set d = min dd;
take min dd ; ::_thesis: ( min dd > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min dd holds
(||.z.|| ") * ||.(R /. z).|| < r ) )
len dd = n by A61, FINSEQ_1:def_3;
then A62: min_p dd in dom dd by RFINSEQ2:def_2;
then A63: dd /. (min_p dd) > 0 by A61;
for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min dd holds
(||.z.|| ") * ||.(R /. z).|| < r
proof
let z be Point of (REAL-NS m); ::_thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < min dd implies (||.z.|| ") * ||.(R /. z).|| < r )
assume A64: ( z <> 0. (REAL-NS m) & ||.z.|| < min dd ) ; ::_thesis: (||.z.|| ") * ||.(R /. z).|| < r
reconsider Rz = R /. z as Element of REAL n by REAL_NS1:def_4;
reconsider R0 = n |-> ((||.z.|| * (((sqrt n) ") * r)) ^2) as Element of n -tuples_on REAL ;
reconsider SRz = sqr Rz as Element of n -tuples_on REAL ;
||.z.|| <> 0 by A64, NORMSP_0:def_5;
then A65: ||.z.|| > 0 by NORMSP_1:4;
A66: for i0 being Nat st i0 in Seg n holds
SRz . i0 < R0 . i0
proof
let i0 be Nat; ::_thesis: ( i0 in Seg n implies SRz . i0 < R0 . i0 )
reconsider i = i0 as Element of NAT by ORDINAL1:def_12;
assume A67: i0 in Seg n ; ::_thesis: SRz . i0 < R0 . i0
then i in dom Rz by FINSEQ_2:124;
then (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:13;
then A68: (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def_2;
( 1 <= i & i <= n ) by A67, FINSEQ_1:1;
then ( 1 <= i & i <= len dd ) by A61, FINSEQ_1:def_3;
then min dd <= dd . i by RFINSEQ2:2;
then min dd <= dd /. i by A67, A61, PARTFUN1:def_6;
then ||.z.|| < dd /. i by A64, XXREAL_0:2;
then (||.z.|| ") * ||.(((Proj (i,n)) * R) /. z).|| < ((sqrt n) ") * r by A64, A67, A61;
then A69: ||.(((Proj (i,n)) * R) /. z).|| < (((sqrt n) ") * r) / (||.z.|| ") by A65, XREAL_1:81;
reconsider Rzi = <*(Rz . i)*> as Element of REAL 1 by FINSEQ_2:98;
((Proj (i,n)) * R) . z = (Proj (i,n)) . (R . z) by FUNCT_2:15;
then ((Proj (i,n)) * R) . z = <*((proj (i,n)) . Rz)*> by PDIFF_1:def_4;
then ((Proj (i,n)) * R) . z = <*(Rz . i)*> by PDIFF_1:def_1;
then ||.(((Proj (i,n)) * R) . z).|| = |.Rzi.| by REAL_NS1:1;
then |.(Rz . i).| < ||.z.|| * (((sqrt n) ") * r) by A69, JORDAN2C:10;
then |.(Rz . i).| ^2 < (||.z.|| * (((sqrt n) ") * r)) ^2 by COMPLEX1:46, SQUARE_1:16;
then (Rz . i0) ^2 < (||.z.|| * (((sqrt n) ") * r)) ^2 by COMPLEX1:75;
hence SRz . i0 < R0 . i0 by A67, A68, FINSEQ_2:57; ::_thesis: verum
end;
A70: for i being Nat st i in dom (sqr Rz) holds
0 <= (sqr Rz) . i
proof
let i be Nat; ::_thesis: ( i in dom (sqr Rz) implies 0 <= (sqr Rz) . i )
assume i in dom (sqr Rz) ; ::_thesis: 0 <= (sqr Rz) . i
then ( i in dom (sqrreal * Rz) & dom (sqrreal * Rz) c= dom Rz ) by RELAT_1:25;
then (sqr Rz) . i = sqrreal . (Rz . i) by FUNCT_1:13;
then (sqr Rz) . i = (Rz . i) ^2 by RVSUM_1:def_2;
hence 0 <= (sqr Rz) . i by XREAL_1:63; ::_thesis: verum
end;
A71: (||.z.|| * (((sqrt n) ") * r)) ^2 >= 0 by XREAL_1:63;
A72: ex i being Nat st
( i in Seg n & SRz . i < R0 . i )
proof
take 1 ; ::_thesis: ( 1 in Seg n & SRz . 1 < R0 . 1 )
1 <= n by NAT_1:14;
hence 1 in Seg n ; ::_thesis: SRz . 1 < R0 . 1
hence SRz . 1 < R0 . 1 by A66; ::_thesis: verum
end;
A73: sqrt n > 0 by SQUARE_1:25;
for i0 being Nat st i0 in Seg n holds
SRz . i0 <= R0 . i0 by A66;
then Sum SRz < Sum R0 by A72, RVSUM_1:83;
then Sum (sqr Rz) < n * ((||.z.|| * (((sqrt n) ") * r)) ^2) by RVSUM_1:80;
then |.Rz.| < sqrt (n * ((||.z.|| * (((sqrt n) ") * r)) ^2)) by A70, RVSUM_1:84, SQUARE_1:27;
then |.Rz.| < (sqrt n) * (sqrt ((||.z.|| * (((sqrt n) ") * r)) ^2)) by A71, SQUARE_1:29;
then |.Rz.| < (sqrt n) * |.(||.z.|| * (((sqrt n) ") * r)).| by COMPLEX1:72;
then |.Rz.| < (sqrt n) * (||.z.|| * (((sqrt n) ") * r)) by A42, A41, A65, ABSVALUE:def_1;
then |.Rz.| < ((sqrt n) * (((sqrt n) ") * r)) * ||.z.|| ;
then |.Rz.| / ||.z.|| < (sqrt n) * (((sqrt n) ") * r) by A65, XREAL_1:83;
then (||.z.|| ") * ||.(R /. z).|| < ((sqrt n) * ((sqrt n) ")) * r by REAL_NS1:1;
then (||.z.|| ") * ||.(R /. z).|| < 1 * r by A73, XCMPLX_0:def_7;
hence (||.z.|| ") * ||.(R /. z).|| < r ; ::_thesis: verum
end;
hence ( min dd > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < min dd holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) by A63, A62, PARTFUN1:def_6; ::_thesis: verum
end;
then reconsider R = R as RestFunc of (REAL-NS m),(REAL-NS n) by NDIFF_1:23;
set N = { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < min d } ;
reconsider N = { y where y is Point of (REAL-NS m) : ||.(y - x0).|| < min d } as Neighbourhood of x0 by A8, NFCONT_1:3;
now__::_thesis:_for_x_being_set_st_x_in_N_holds_
x_in_dom_g
let x be set ; ::_thesis: ( x in N implies x in dom g )
assume x in N ; ::_thesis: x in dom g
then consider y being Point of (REAL-NS m) such that
A74: ( x = y & ||.(y - x0).|| < min d ) ;
1 <= n by NAT_1:14;
then A75: ( 1 in Seg n & 1 in dom d ) by A6;
then A76: { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } c= dom ((Proj (1,n)) * g) by A6;
dom ((Proj (1,n)) * g) c= dom g by RELAT_1:25;
then A77: { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } c= dom g by A76, XBOOLE_1:1;
len d = n by A6, FINSEQ_1:def_3;
then 1 <= len d by NAT_1:14;
then min d <= d . 1 by RFINSEQ2:2;
then min d <= d /. 1 by A75, PARTFUN1:def_6;
then ||.(y - x0).|| < d /. 1 by A74, XXREAL_0:2;
then y in { z where z is Point of (REAL-NS m) : ||.(z - x0).|| < d /. 1 } ;
hence x in dom g by A74, A77; ::_thesis: verum
end;
then A78: N c= dom g by TARSKI:def_3;
ex L being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) ex R being RestFunc of (REAL-NS m),(REAL-NS n) st
for x being Point of (REAL-NS m) st x in N holds
(g /. x) - (g /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
take L0 ; ::_thesis: ex R being RestFunc of (REAL-NS m),(REAL-NS n) st
for x being Point of (REAL-NS m) st x in N holds
(g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))
take R ; ::_thesis: for x being Point of (REAL-NS m) st x in N holds
(g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))
hereby ::_thesis: verum
let x be Point of (REAL-NS m); ::_thesis: ( x in N implies (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) )
assume x in N ; ::_thesis: (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0))
A79: dom R = the carrier of (REAL-NS m) by PARTFUN1:def_2;
R . (x - x0) = ((g /. ((x - x0) + x0)) - (g /. x0)) - (L . (x - x0)) by A26;
then R . (x - x0) = ((g /. (x - (x0 - x0))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:29;
then R . (x - x0) = ((g /. (x - (x0 + (- x0)))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:def_11;
then R . (x - x0) = ((g /. (x - (0. (REAL-NS m)))) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:5;
then R . (x - x0) = ((g /. x) - (g /. x0)) - (L0 . (x - x0)) by RLVECT_1:13;
then R . (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by RLVECT_1:def_11;
then R /. (x - x0) = ((g /. x) - (g /. x0)) + (- (L0 . (x - x0))) by A79, PARTFUN1:def_6;
then (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + ((- (L0 . (x - x0))) + (L0 . (x - x0))) by RLVECT_1:def_3;
then (L0 . (x - x0)) + (R /. (x - x0)) = ((g /. x) - (g /. x0)) + (0. (REAL-NS n)) by RLVECT_1:5;
hence (g /. x) - (g /. x0) = (L0 . (x - x0)) + (R /. (x - x0)) by RLVECT_1:4; ::_thesis: verum
end;
end;
hence g is_differentiable_in x0 by A78, NDIFF_1:def_6; ::_thesis: verum
end;
hence ( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 ) by Th28; ::_thesis: verum
end;
definition
let X be set ;
let n, m be non empty Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
predf is_differentiable_on X means :Def4: :: PDIFF_6:def 4
( X c= dom f & ( for x being Element of REAL m st x in X holds
f | X is_differentiable_in x ) );
end;
:: deftheorem Def4 defines is_differentiable_on PDIFF_6:def_4_:_
for X being set
for n, m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n) holds
( f is_differentiable_on X iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f | X is_differentiable_in x ) ) );
theorem Th30: :: PDIFF_6:30
for X being set
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds
( f is_differentiable_on X iff g is_differentiable_on X )
proof
let X be set ; ::_thesis: for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds
( f is_differentiable_on X iff g is_differentiable_on X )
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds
( f is_differentiable_on X iff g is_differentiable_on X )
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds
( f is_differentiable_on X iff g is_differentiable_on X )
let g be PartFunc of (REAL-NS m),(REAL-NS n); ::_thesis: ( f = g implies ( f is_differentiable_on X iff g is_differentiable_on X ) )
assume A1: f = g ; ::_thesis: ( f is_differentiable_on X iff g is_differentiable_on X )
A2: now__::_thesis:_(_f_is_differentiable_on_X_implies_g_is_differentiable_on_X_)
assume A3: f is_differentiable_on X ; ::_thesis: g is_differentiable_on X
then A4: ( X c= dom f & ( for x being Element of REAL m st x in X holds
f | X is_differentiable_in x ) ) by Def4;
now__::_thesis:_for_y_being_Point_of_(REAL-NS_m)_st_y_in_X_holds_
g_|_X_is_differentiable_in_y
let y be Point of (REAL-NS m); ::_thesis: ( y in X implies g | X is_differentiable_in y )
reconsider x = y as Element of REAL m by REAL_NS1:def_4;
assume y in X ; ::_thesis: g | X is_differentiable_in y
then f | X is_differentiable_in x by A3, Def4;
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f | X = g & x = y & g is_differentiable_in y ) by PDIFF_1:def_7;
hence g | X is_differentiable_in y by A1; ::_thesis: verum
end;
hence g is_differentiable_on X by A1, A4, NDIFF_1:def_8; ::_thesis: verum
end;
now__::_thesis:_(_g_is_differentiable_on_X_implies_(_X_c=_dom_f_&_f_is_differentiable_on_X_)_)
assume A5: g is_differentiable_on X ; ::_thesis: ( X c= dom f & f is_differentiable_on X )
hence X c= dom f by A1, NDIFF_1:def_8; ::_thesis: f is_differentiable_on X
A6: ( X c= dom g & ( for x being Point of (REAL-NS m) st x in X holds
g | X is_differentiable_in x ) ) by A5, NDIFF_1:def_8;
now__::_thesis:_for_y_being_Element_of_REAL_m_st_y_in_X_holds_
f_|_X_is_differentiable_in_y
let y be Element of REAL m; ::_thesis: ( y in X implies f | X is_differentiable_in y )
reconsider x = y as Point of (REAL-NS m) by REAL_NS1:def_4;
assume y in X ; ::_thesis: f | X is_differentiable_in y
then g | X is_differentiable_in x by A5, NDIFF_1:def_8;
hence f | X is_differentiable_in y by A1, PDIFF_1:def_7; ::_thesis: verum
end;
hence f is_differentiable_on X by A1, A6, Def4; ::_thesis: verum
end;
hence ( f is_differentiable_on X iff g is_differentiable_on X ) by A2; ::_thesis: verum
end;
theorem :: PDIFF_6:31
for X being set
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is Subset of (REAL m)
proof
let X be set ; ::_thesis: for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is Subset of (REAL m)
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is Subset of (REAL m)
let f be PartFunc of (REAL m),(REAL n); ::_thesis: ( f is_differentiable_on X implies X is Subset of (REAL m) )
assume f is_differentiable_on X ; ::_thesis: X is Subset of (REAL m)
then X c= dom f by Def4;
hence X is Subset of (REAL m) by XBOOLE_1:1; ::_thesis: verum
end;
theorem :: PDIFF_6:32
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )
proof
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for Z being Subset of (REAL m) st ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )
let Z be Subset of (REAL m); ::_thesis: ( ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) implies ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) ) )
assume ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) ; ::_thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )
then consider Z0 being Subset of (REAL-NS m) such that
A1: ( Z = Z0 & Z0 is open ) ;
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4;
then reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) ;
A2: ( g is_differentiable_on Z0 iff ( Z0 c= dom g & ( for x being Point of (REAL-NS m) st x in Z0 holds
g is_differentiable_in x ) ) ) by A1, NDIFF_1:31;
thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) ) ::_thesis: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) implies f is_differentiable_on Z )
proof
assume A3: f is_differentiable_on Z ; ::_thesis: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) )
hence Z c= dom f by Def4; ::_thesis: for x being Element of REAL m st x in Z holds
f is_differentiable_in x
let x be Element of REAL m; ::_thesis: ( x in Z implies f is_differentiable_in x )
reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def_4;
assume x in Z ; ::_thesis: f is_differentiable_in x
then g is_differentiable_in y by A1, A2, A3, Th30;
hence f is_differentiable_in x by PDIFF_1:def_7; ::_thesis: verum
end;
assume A4: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) ; ::_thesis: f is_differentiable_on Z
now__::_thesis:_for_y_being_Point_of_(REAL-NS_m)_st_y_in_Z0_holds_
g_is_differentiable_in_y
let y be Point of (REAL-NS m); ::_thesis: ( y in Z0 implies g is_differentiable_in y )
reconsider x = y as Element of REAL m by REAL_NS1:def_4;
assume y in Z0 ; ::_thesis: g is_differentiable_in y
then f is_differentiable_in x by A1, A4;
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_differentiable_in y ) by PDIFF_1:def_7;
hence g is_differentiable_in y ; ::_thesis: verum
end;
hence f is_differentiable_on Z by A1, A2, A4, Th30; ::_thesis: verum
end;
theorem :: PDIFF_6:33
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st f is_differentiable_on Z holds
ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open )
proof
let m, n be non empty Element of NAT ; ::_thesis: for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st f is_differentiable_on Z holds
ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open )
let f be PartFunc of (REAL m),(REAL n); ::_thesis: for Z being Subset of (REAL m) st f is_differentiable_on Z holds
ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open )
let Z be Subset of (REAL m); ::_thesis: ( f is_differentiable_on Z implies ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) )
assume A1: f is_differentiable_on Z ; ::_thesis: ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open )
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def_4;
then reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) ;
reconsider Z0 = Z as Subset of (REAL-NS m) by REAL_NS1:def_4;
take Z0 ; ::_thesis: ( Z = Z0 & Z0 is open )
g is_differentiable_on Z0 by A1, Th30;
hence ( Z = Z0 & Z0 is open ) by NDIFF_1:32; ::_thesis: verum
end;