:: Partial Differentiation, Differentiation and Continuity on $n$-Dimensional Real Normed Linear Spaces
:: by Takao Inou\'e , Adam Naumowicz , Noboru Endou and Yasunari Shidama
::
:: Received October 13, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

:: Some properties of partial differentiation
:: of PartFunc of REAL-NS m,REAL-NS n
theorem Th1: :: PDIFF_8:1
for n, i being Element of NAT
for q being Element of REAL n
for p being Point of (TOP-REAL n) st i in Seg n & q = p holds
abs (p /. i) <= |.q.|
proofend;

theorem Th2: :: PDIFF_8:2
for x being Real
for vx being Element of (REAL-NS 1) st vx = <*x*> holds
||.vx.|| = abs x
proofend;

theorem Th3: :: PDIFF_8:3
for n being non empty Element of NAT
for x being Point of (REAL-NS n)
for i being Element of NAT st 1 <= i &amp; i <= n holds
||.((Proj (i,n)) . x).|| <= ||.x.||
proofend;

theorem Th4: :: PDIFF_8:4
for n being non empty Element of NAT
for x being Element of (REAL-NS n)
for i being Element of NAT holds ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|
proofend;

theorem :: PDIFF_8:5
for n being non empty Element of NAT
for x being Element of REAL n
for i being Element of NAT st 1 <= i &amp; i <= n holds
|.((proj (i,n)) . x).| <= |.x.|
proofend;

theorem Th6: :: PDIFF_8:6
for m, n being non empty Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT st 1 <= i &amp; i <= n holds
( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) &amp; (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )
proofend;

theorem Th7: :: PDIFF_8:7
for m, n being non empty Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT st 1 <= i &amp; i <= n holds
( (Proj (i,n)) * s is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) &amp; (BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS 1))) . ((Proj (i,n)) * s) <= ((BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n))) * ((BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n))) . s) )
proofend;

theorem :: PDIFF_8:8
for n being non empty Element of NAT
for i being Element of NAT holds Proj (i,n) is homogeneous
proofend;

theorem :: PDIFF_8:9
for n being non empty Element of NAT
for x being Element of REAL n
for r being Real
for i being Element of NAT holds (proj (i,n)) . (r * x) = r * ((proj (i,n)) . x)
proofend;

theorem :: PDIFF_8:10
for n being non empty Element of NAT
for x, y being Element of REAL n
for i being Element of NAT holds (proj (i,n)) . (x + y) = ((proj (i,n)) . x) + ((proj (i,n)) . y)
proofend;

theorem Th11: :: PDIFF_8:11
for n being non empty Element of NAT
for x, y being Point of (REAL-NS n)
for i being Element of NAT holds (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)
proofend;

theorem :: PDIFF_8:12
for n being non empty Element of NAT
for x, y being Element of REAL n
for i being Element of NAT holds (proj (i,n)) . (x - y) = ((proj (i,n)) . x) - ((proj (i,n)) . y)
proofend;

Lm1:  for m, n being non empty Element of NAT
for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s &amp; ti = (Proj (i,n)) * t &amp; 1 <= i &amp; i <= n holds
si - ti = (Proj (i,n)) * (s - t)
proofend;

theorem Th13: :: PDIFF_8:13
for m, n being non empty Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s &amp; 1 <= i &amp; i <= n holds
||.si.|| <= ||.s.||
proofend;

theorem Th14: :: PDIFF_8:14
for m, n being non empty Element of NAT
for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)))
for i being Element of NAT st si = (Proj (i,n)) * s &amp; ti = (Proj (i,n)) * t &amp; 1 <= i &amp; i <= n holds
||.(si - ti).|| <= ||.(s - t).||
proofend;

theorem Th15: :: PDIFF_8:15
for K being Real
for n being Element of NAT
for s being Element of REAL n st ( for i being Element of NAT st 1 <= i &amp; i <= n holds
abs (s . i) <= K ) holds
|.s.| <= n * K
proofend;

theorem Th16: :: PDIFF_8:16
for K being Real
for n being non empty Element of NAT
for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i &amp; i <= n holds
||.((Proj (i,n)) . s).|| <= K ) holds
||.s.|| <= n * K
proofend;

theorem :: PDIFF_8:17
for K being Real
for n being non empty Element of NAT
for s being Element of REAL n st ( for i being Element of NAT st 1 <= i &amp; i <= n holds
|.((proj (i,n)) . s).| <= K ) holds
|.s.| <= n * K
proofend;

theorem Th18: :: PDIFF_8:18
for m, n being non empty Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for K being Real st ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s &amp; 1 <= i &amp; i <= n holds
||.si.|| <= K ) holds
||.s.|| <= n * K
proofend;

theorem Th19: :: PDIFF_8:19
for m, n being non empty Element of NAT
for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for K being Real st ( for i being Element of NAT
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s &amp; ti = (Proj (i,n)) * t &amp; 1 <= i &amp; i <= n holds
||.(si - ti).|| <= K ) holds
||.(s - t).|| <= n * K
proofend;

theorem Th20: :: PDIFF_8:20
for m, n being non empty Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL-NS m)
for i being Element of NAT st 1 <= i &amp; i <= m &amp; X is open holds
( ( f is_partial_differentiable_on X,i &amp; f `partial| (X,i) is_continuous_on X ) iff for j being Element of NAT st 1 <= j &amp; j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i &amp; ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )
proofend;

theorem Th21: :: PDIFF_8:21
for m, n being non empty Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL-NS m) st X is open holds
( ( f is_differentiable_on X &amp; f `| X is_continuous_on X ) iff for j being Element of NAT st 1 <= j &amp; j <= n holds
( (Proj (j,n)) * f is_differentiable_on X &amp; ((Proj (j,n)) * f) `| X is_continuous_on X ) )
proofend;

theorem :: PDIFF_8:22
for m, n being non empty Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL-NS m) st X is open holds
( ( for i being Element of NAT st 1 <= i &amp; i <= m holds
( f is_partial_differentiable_on X,i &amp; f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X &amp; f `| X is_continuous_on X ) )
proofend;