:: 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-2021 Association of Mizar Users

:: 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
|.(p /. i).| <= |.q.|

proof end;

theorem Th2: :: PDIFF_8:2

for x being Real
for vx being Element of (REAL-NS 1) st vx = <*x*> holds
||.vx.|| = |.x.|

proof end;

theorem Th3: :: PDIFF_8:3

for n being non zero Element of NAT
for x being Point of (REAL-NS n)
for i being Nat st 1 <= i & i <= n holds
||.((Proj (i,n)) . x).|| <= ||.x.||

proof end;

theorem Th4: :: PDIFF_8:4

for n being non zero 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).|

proof end;

theorem :: PDIFF_8:5

for n being non zero Element of NAT
for x being Element of REAL n
for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . x).| <= |.x.|

proof end;

theorem Th6: :: PDIFF_8:6

for m, n being non zero Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Nat st 1 <= i & i <= n holds
( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )

proof end;

theorem Th7: :: PDIFF_8:7

for m, n being non zero Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Nat st 1 <= i & i <= n holds
( (Proj (i,n)) * s is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) & (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) )

proof end;

theorem :: PDIFF_8:8

for n being non zero Element of NAT
for i being Element of NAT holds Proj (i,n) is homogeneous

proof end;

theorem :: PDIFF_8:9

for n being non zero 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)

proof end;

theorem :: PDIFF_8:10

for n being non zero 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)

proof end;

theorem Th11: :: PDIFF_8:11

for n being non zero Element of NAT
for x, y being Point of (REAL-NS n)
for i being Nat holds (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)

proof end;

theorem :: PDIFF_8:12

for n being non zero 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)

proof end;

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

proof end;

theorem Th13: :: PDIFF_8:13

for m, n being non zero Element of NAT
for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for i being Nat
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= ||.s.||

proof end;

theorem Th14: :: PDIFF_8:14

for m, n being non zero 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 Nat st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= ||.(s - t).||

proof end;

theorem Th15: :: PDIFF_8:15

for K being Real
for n being Nat
for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds
|.(s . i).| <= K ) holds
|.s.| <= n * K

proof end;

theorem Th16: :: PDIFF_8:16

for K being Real
for n being non zero Element of NAT
for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ) holds
||.s.|| <= n * K

proof end;

theorem :: PDIFF_8:17

for K being Real
for n being non zero Element of NAT
for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . s).| <= K ) holds
|.s.| <= n * K

proof end;

theorem Th18: :: PDIFF_8:18

for m, n being non zero 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 & 1 <= i & i <= n holds
||.si.|| <= K ) holds
||.s.|| <= n * K

proof end;

theorem Th19: :: PDIFF_8:19

for m, n being non zero 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 & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= K ) holds
||.(s - t).|| <= n * K

proof end;

theorem Th20: :: PDIFF_8:20

for m, n being non zero 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 Nat st 1 <= i & i <= m & X is open holds
( ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) iff for j being Nat st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )

proof end;

theorem Th21: :: PDIFF_8:21

for m, n being non zero 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 & f `| X is_continuous_on X ) iff for j being Nat st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) )

proof end;

theorem :: PDIFF_8:22

for m, n being non zero 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 Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & f `| X is_continuous_on X ) )

proof end;