PDIFF_8: Partial Differentiation, Differentiation and Continuity on $n$-Dimensional Real Normed Linear Spaces

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

environ

vocabularies HIDDEN, PRE_TOPC, RLVECT_1, FUNCT_1, ARYTM_3, ARYTM_1, FINSEQ_1, FINSEQ_2, XXREAL_2, FINSET_1, MEMBERED, RVSUM_1, RELAT_1, COMPLEX1, SQUARE_1, RCOMP_1, XBOOLE_0, PARTFUN1, NORMSP_1, LOPBAN_1, FDIFF_1, PDIFF_1, REAL_NS1, BORSUK_1, EUCLID, NUMBERS, STRUCT_0, CFCONT_1, FUNCT_4, REAL_1, SUBSET_1, CARD_1, TARSKI, XXREAL_0, CARD_3, NAT_1, SEQ_4, UNIALG_1, FCONT_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, MEMBERED, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, RVSUM_1, SEQ_4, FUNCT_7, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_0, EUCLID, LOPBAN_1, NFCONT_1, NDIFF_1, REAL_NS1, PDIFF_1;
definitions LOPBAN_1;
theorems ABSVALUE, EUCLID, XREAL_1, COMPLEX1, FINSEQ_1, FINSEQ_2, FINSEQ_3, ORDINAL1, NAT_1, FINSET_1, XXREAL_0, FUNCT_7, RVSUM_1, RELAT_1, FUNCT_1, FUNCT_2, SQUARE_1, NORMSP_1, LOPBAN_1, PARTFUN1, NFCONT_1, NDIFF_1, REAL_NS1, VALUED_1, PDIFF_1, XXREAL_2, XCMPLX_1, PDIFF_6, SEQ_4, VECTSP_1, PDIFF_7, LOPBAN_2, JORDAN2B, SERIES_3, CARD_1, XREAL_0;
schemes NAT_1, FINSEQ_1;
registrations FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, VALUED_0, XXREAL_2, FINSEQ_1, FINSEQ_2, STRUCT_0, MONOID_0, EUCLID, LOPBAN_1, JORDAN2B, REAL_NS1, PDIFF_6, CARD_1, SQUARE_1;
constructors HIDDEN, RELSET_1, REAL_1, SQUARE_1, NAT_D, BINOP_2, FINSEQOP, SEQ_4, FINSEQ_7, MONOID_0, RSSPACE3, NFCONT_1, NDIFF_1, PDIFF_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities XBOOLE_0, SQUARE_1, FINSEQ_1, NORMSP_0, EUCLID, LOPBAN_1;
expansions ;

:: 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;