:: The $C^k$ Space
:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received November 9, 2012
:: Copyright (c) 2012 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, ALGSTR_0, SUBSET_1, ARYTM_1, IDEAL_1, ARYTM_3,
FUNCSDOM, STRUCT_0, TARSKI, MESFUNC1, SUPINF_2, BINOP_1, FUNCT_1,
RELAT_1, RLVECT_1, VECTSP_1, RSSPACE, GROUP_1, REAL_1, POLYALG1, CARD_1,
FUNCOP_1, FUNCT_2, VALUED_1, LOPBAN_1, COMPLEX1, XXREAL_0, PRE_TOPC,
NAT_1, C0SP1, FINSEQ_1, FINSEQ_2, RCOMP_1, PARTFUN1, ORDINAL4, FDIFF_1,
PDIFF_1, REAL_NS1, EUCLID, CFCONT_1, RFINSEQ, CARD_3, PDIFF_9, CKSPACE1,
XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
REAL_1, NAT_1, COMPLEX1, FINSEQ_1, VALUED_1, FINSEQ_2, RFINSEQ, SEQFUNC,
STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM,
EUCLID, LOPBAN_1, IDEAL_1, C0SP1, NFCONT_1, NDIFF_1, REAL_NS1, PDIFF_1,
PDIFF_6, PDIFF_7, PDIFF_9;
constructors REAL_1, REALSET1, MEASURE6, BINOP_2, SEQ_1, IDEAL_1, XXREAL_2,
RELSET_1, SQUARE_1, NFCONT_1, FDIFF_1, NDIFF_1, PDIFF_1, MONOID_0,
INTEGR15, RFINSEQ, NAT_D, PDIFF_6, VFUNCT_1, PDIFF_7, VALUED_2, NFCONT_4,
SEQFUNC, PDIFF_9, C0SP1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, NUMBERS, ORDINAL1, MEMBERED,
FUNCSDOM, XXREAL_0, VECTSP_1, VECTSP_2, VALUED_0, RELSET_1, NAT_1,
FINSEQ_1, EUCLID, REAL_NS1, FUNCT_2, XCMPLX_0, XREAL_0;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions ALGSTR_0, TARSKI, FINSEQ_1, FUNCSDOM, RLVECT_1, STRUCT_0, BINOP_1,
VALUED_1, PDIFF_9;
theorems FUNCT_1, COMPLEX1, ZFMISC_1, TARSKI, XREAL_0, XXREAL_0, FUNCSDOM,
LOPBAN_1, FUNCT_2, XREAL_1, RLVECT_1, FUNCOP_1, VALUED_1, IDEAL_1,
RELSET_1, XBOOLE_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_3, RFINSEQ, NAT_1,
FINSEQ_5, PARTFUN1, NDIFF_1, REAL_NS1, PDIFF_1, ORDINAL1, PDIFF_6,
PDIFF_7, INT_1, PDIFF_9, C0SP1;
schemes NAT_1;
begin ::
definition
let m be non zero Element of NAT;
let f be PartFunc of REAL m,REAL;
let k be Element of NAT;
let Z be set;
pred f is_continuously_differentiable_up_to_order k,Z means :defX1:
Z c= dom f & f is_partial_differentiable_up_to_order k,Z &
for I be non empty FinSequence of NAT
st len I <= k & rng I c= Seg m holds
f`partial|(Z,I) is_continuous_on Z;
end;
theorem Th01:
for m be non zero Element of NAT,
Z be set,I be non empty FinSequence of NAT,
f be PartFunc of REAL m,REAL st f is_partial_differentiable_on Z,I
holds dom (f`partial|(Z,I)) = Z
proof
let m be non zero Element of NAT, Z be set,
I be non empty FinSequence of NAT,
f be PartFunc of REAL m,REAL;
assume
AS: f is_partial_differentiable_on Z,I;
reconsider k=(len I)-1 as Element of NAT by INT_1:5,FINSEQ_1:20;
P1: f`partial|(Z,I) = ((PartDiffSeq(f,Z,I)).k)`partial|(Z,I/.(k+1))
by PDIFF_9:def 7;
(PartDiffSeq(f,Z,I)).k is_partial_differentiable_on Z,I/.(k+1)
by PDIFF_9:def 8,AS;
hence thesis by P1,PDIFF_9:def 6;
end;
theorem Th02:
for m be non zero Element of NAT, k be Element of NAT,
X be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL st X is open & X c= dom f
holds
f is_continuously_differentiable_up_to_order 1,X
iff
(f is_differentiable_on X
& for x0 be Element of REAL m,r be Real st x0 in X & 0 < r
ex s be Real st 0 < s
& for x1 be Element of REAL m st x1 in X & |. x1- x0 .| < s holds
for v be Element of REAL m
holds |. diff(f,x1).v - diff(f,x0).v.| <= r * |.v.| )
proof
let m be non zero Element of NAT, k be Element of NAT,
X be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL;
assume
AS: X is open & X c= dom f;
hereby assume
A1: f is_continuously_differentiable_up_to_order 1,X;
now let i be Element of NAT;
assume
A2: 1 <= i & i <= m;
set I = <*i*>;
A3: len I = 1 by FINSEQ_1:40;
i in Seg m by A2;
then {i} c= Seg m by ZFMISC_1:31;
then
A4: rng I c= Seg m by FINSEQ_1:38;
then
A5: f`partial|(X,I) is_continuous_on X by A1,defX1,A3;
f is_partial_differentiable_on X,I by A3,A4,A1,PDIFF_9:def 10,defX1;
hence f is_partial_differentiable_on X,i by PDIFF_9:76;
thus f`partial|(X,i) is_continuous_on X by PDIFF_9:77,A5;
end;
hence f is_differentiable_on X
& for x0 be Element of REAL m,r be Real st x0 in X & 0 < r
ex s be Real st 0 < s
& for x1 be Element of REAL m st x1 in X & |. x1- x0 .| < s holds
for v be Element of REAL m
holds |. diff(f,x1).v - diff(f,x0).v.| <= r * |.v.| by AS,PDIFF_9:63;
end;
assume
A6: f is_differentiable_on X
& for x0 be Element of REAL m,r be Real st x0 in X & 0 < r
ex s be Real st 0 < s
& for x1 be Element of REAL m st x1 in X & |. x1- x0 .| < s holds
for v be Element of REAL m
holds |. diff(f,x1).v - diff(f,x0).v.| <= r * |.v.|;
then
A7: for i be Element of NAT st 1 <= i & i <= m holds
f is_partial_differentiable_on X,i &
f`partial|(X,i) is_continuous_on X by AS,PDIFF_9:63;
A8:now let I be non empty FinSequence of NAT;
assume
A9: len I <= 1 & rng I c= Seg m;
A10:1 <= len I by FINSEQ_1:20;
then
A11:1 in dom I by FINSEQ_3:25;
then
A12:I/.1 = I.1 by PARTFUN1:def 6;
A13:I.1 in rng I by A11,FUNCT_1:3;
reconsider i = I.1 as Element of NAT by ORDINAL1:def 12;
A14:1 <= i & i <= m by A13,A9,FINSEQ_1:1;
A15:I = <*I/.1*> by FINSEQ_5:14,A9,A10,XXREAL_0:1;
then
A16: I = <*i*> by PARTFUN1:def 6,A11;
thus f is_partial_differentiable_on X,I by A15,A12,PDIFF_9:76,A14,A7;
f`partial|(X,i) is_continuous_on X by A14,AS,PDIFF_9:63,A6;
hence f`partial|(X,I) is_continuous_on X by A16,PDIFF_9:77;
end;
then
A17:for I be non empty FinSequence of NAT st len I <= 1 & rng I c= Seg m
holds f is_partial_differentiable_on X,I;
for I be non empty FinSequence of NAT st len I <= 1 & rng I c= Seg m
holds f`partial|(X,I) is_continuous_on X by A8;
hence f is_continuously_differentiable_up_to_order 1,X
by AS,A17,defX1,PDIFF_9:def 10;
end;
theorem Th03:
for m be non zero Element of NAT, X be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL st X is open & X c= dom f
& f is_continuously_differentiable_up_to_order 1,X
holds
f is_continuous_on X
proof
let m be non zero Element of NAT,
X be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL;
assume
AS: X is open & X c= dom f & f is_continuously_differentiable_up_to_order 1,X;
then
A1: f is_differentiable_on X by Th02;
reconsider g = <>*f as PartFunc of REAL m,REAL 1;
A2: g is_differentiable_on X by AS,A1,PDIFF_9:53;
the carrier of (REAL-NS m) = REAL m
& the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
then
reconsider h = <>*f as PartFunc of REAL-NS m,REAL-NS 1;
h is_differentiable_on X by A2,PDIFF_6:30;
then h is_continuous_on X by NDIFF_1:45;
then g is_continuous_on X by PDIFF_7:37;
hence f is_continuous_on X by PDIFF_9:44;
end;
theorem Th04:
for m be non zero Element of NAT, k be Element of NAT,
X be non empty Subset of REAL m, f,g be PartFunc of REAL m,REAL
st f is_continuously_differentiable_up_to_order k,X &
g is_continuously_differentiable_up_to_order k,X & X is open
holds
f+g is_continuously_differentiable_up_to_order k,X
proof
let m be non zero Element of NAT, k be Element of NAT,
X be non empty Subset of REAL m,
f,g be PartFunc of REAL m,REAL;
assume
AS1: f is_continuously_differentiable_up_to_order k,X
& g is_continuously_differentiable_up_to_order k,X & X is open;
A1:X c= dom f & f is_partial_differentiable_up_to_order k,X
& for f0 be PartFunc of REAL m,REAL,I be non empty FinSequence of NAT
st len I <= k & rng I c= Seg m &
f0= f`partial|(X,I) holds f0 is_continuous_on X by AS1,defX1;
A2:X c= dom g & g is_partial_differentiable_up_to_order k,X
& for g0 be PartFunc of REAL m,REAL,I be non empty FinSequence of NAT
st len I <= k & rng I c= Seg m &
g0= g`partial|(X,I) holds g0 is_continuous_on X by AS1,defX1;
A3:dom (f+g) = dom f /\ dom g by VALUED_1:def 1;
A4:(f+g) is_partial_differentiable_up_to_order k,X by A1,A2,AS1,PDIFF_9:80;
for I be non empty FinSequence of NAT st len I <= k & rng I c= Seg m
holds (f+g)`partial|(X,I) is_continuous_on X
proof
let I be non empty FinSequence of NAT;
assume
A5: len I <= k & rng I c= Seg m;
A6: f is_partial_differentiable_on X,I by A5,PDIFF_9:def 10,AS1,defX1;
A7: g is_partial_differentiable_on X,I by A5,AS1,defX1,PDIFF_9:def 10;
reconsider f0 = f`partial|(X,I) as PartFunc of REAL m,REAL;
reconsider g0 = g`partial|(X,I) as PartFunc of REAL m,REAL;
A8: X = dom f0 by Th01,A6;
A9: X = dom g0 by Th01,A7;
A10:f0 is_continuous_on X by A5,AS1,defX1;
A11:g0 is_continuous_on X by A5,AS1,defX1;
f0+g0 is_continuous_on X by A10,A11,A8,A9,PDIFF_9:46;
hence
(f+g)`partial|(X,I) is_continuous_on X by AS1,A5,A6,A7,PDIFF_9:70;
end;
hence thesis by A3,A4,defX1,A1,A2,XBOOLE_1:19;
end;
theorem Th05:
for m be non zero Element of NAT, k be Element of NAT,
X be non empty Subset of REAL m,r be Real,
f be PartFunc of REAL m,REAL st
f is_continuously_differentiable_up_to_order k,X & X is open
holds
r(#)f is_continuously_differentiable_up_to_order k,X
proof
let m be non zero Element of NAT, k be Element of NAT,
X be non empty Subset of REAL m,r be Real,
f be PartFunc of REAL m,REAL;
assume
AS: f is_continuously_differentiable_up_to_order k,X & X is open;
A1:X c= dom f & f is_partial_differentiable_up_to_order k,X
& for f0 be PartFunc of REAL m,REAL,I be non empty FinSequence of NAT
st len I <= k & rng I c= Seg m & f0= f`partial|(X,I)
holds f0 is_continuous_on X by AS,defX1;
A2:X c= dom (r(#)f) by VALUED_1:def 5,A1;
A3:(r(#)f) is_partial_differentiable_up_to_order k,X by PDIFF_9:81,AS,defX1;
for I be non empty FinSequence of NAT st len I <= k & rng I c= Seg m
holds (r(#)f)`partial|(X,I) is_continuous_on X
proof
let I be non empty FinSequence of NAT;
assume
A4: len I <= k & rng I c= Seg m;
A5: f is_partial_differentiable_on X,I by A4,PDIFF_9:def 10,AS,defX1;
reconsider f0 = f`partial|(X,I) as PartFunc of REAL m,REAL;
A6: X = dom f0 by Th01,A5;
f0 is_continuous_on X by A4,AS,defX1;
then
r(#)f0 is_continuous_on X by A6,PDIFF_9:47;
hence
(r(#)f)`partial|(X,I) is_continuous_on X by AS,A4,A5,PDIFF_9:74;
end;
hence thesis by A2,A3,defX1;
end;
theorem
for m be non zero Element of NAT, k be Element of NAT,
X be non empty Subset of REAL m,
f,g be PartFunc of REAL m,REAL st
f is_continuously_differentiable_up_to_order k,X &
g is_continuously_differentiable_up_to_order k,X & X is open
holds
f-g is_continuously_differentiable_up_to_order k,X
proof
let m be non zero Element of NAT, k be Element of NAT,
X be non empty Subset of REAL m,
f,g be PartFunc of REAL m,REAL;
assume
AS: f is_continuously_differentiable_up_to_order k,X
& g is_continuously_differentiable_up_to_order k,X & X is open;
A1:X c= dom f & f is_partial_differentiable_up_to_order k,X
& for f0 be PartFunc of REAL m,REAL,I be non empty FinSequence of NAT
st len I <= k & rng I c= Seg m & f0= f`partial|(X,I)
holds f0 is_continuous_on X by AS,defX1;
A2:X c= dom g & g is_partial_differentiable_up_to_order k,X
& for g0 be PartFunc of REAL m,REAL,I be non empty FinSequence of NAT
st len I <= k & rng I c= Seg m & g0= g`partial|(X,I)
holds g0 is_continuous_on X by AS,defX1;
A3:dom (f-g) = dom f /\ dom g by VALUED_1:12;
A4:(f-g) is_partial_differentiable_up_to_order k,X by A1,A2,AS,PDIFF_9:80;
for I be non empty FinSequence of NAT st len I <= k & rng I c= Seg m
holds (f-g)`partial|(X,I) is_continuous_on X
proof
let I be non empty FinSequence of NAT;
assume
A5: len I <= k & rng I c= Seg m;
A6: f is_partial_differentiable_on X,I by A5,PDIFF_9:def 10,AS,defX1;
A7: g is_partial_differentiable_on X,I by A5,PDIFF_9:def 10,AS,defX1;
reconsider f0 = f`partial|(X,I) as PartFunc of REAL m,REAL;
reconsider g0 = g`partial|(X,I) as PartFunc of REAL m,REAL;
A8: X = dom f0 by Th01,A6;
A9: X = dom g0 by Th01,A7;
A10:f0 is_continuous_on X by AS,A5,defX1;
A11:g0 is_continuous_on X by A5,AS,defX1;
f0-g0 is_continuous_on X by A10,A11,A8,A9,PDIFF_9:46;
hence (f-g)`partial|(X,I) is_continuous_on X by AS,A5,A6,A7,PDIFF_9:72;
end;
hence thesis by A3,A4,defX1,A1,A2,XBOOLE_1:19;
end;
theorem Th07:
for m be non zero Element of NAT,Z be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL,I,G be non empty FinSequence of NAT
holds f `partial|(Z,G^I) = f`partial|(Z,G) `partial|(Z,I)
proof
let m be non zero Element of NAT, Z be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL, I,G be non empty FinSequence of NAT;
set g = f`partial|(Z,G);
reconsider Z0 = 0 as Element of NAT;
A1:dom G c= dom (G^I) by FINSEQ_1:26;
A2:for i be Element of NAT st i <= len G - 1 holds (G^I)/.(i+1) = G/.(i+1)
proof
let i be Element of NAT;
assume i <= len G - 1;
then
1 <= i+1 & i+1 <= len G by NAT_1:11,XREAL_1:19;
then
A3: i+1 in dom G by FINSEQ_3:25;
then
(G^I)/.(i+1) = (G^I).(i+1) by A1,PARTFUN1:def 6;
then
(G^I)/.(i+1) = G.(i+1) by A3,FINSEQ_1:def 7;
hence (G^I)/.(i+1) = G/.(i+1) by A3,PARTFUN1:def 6;
end;
A4:len (G^I) = len G + len I by FINSEQ_1:22;
A5:for i be Element of NAT st i <= (len I)-1
holds (G^I)/.(len G + (i+1)) = I/.(i+1)
proof
let i be Element of NAT;
assume i <= len I - 1;
then
A6: i+1 <= len I by XREAL_1:19;
then
A7: i+1 in dom I by FINSEQ_3:25,NAT_1:11;
1 <= len G + (i+1) by NAT_1:11,XREAL_1:38;
then
len G + (i+1) in dom (G^I) by FINSEQ_3:25,A4,A6,XREAL_1:7;
hence (G^I)/.(len G + (i+1)) =(G^I).(len G + (i+1)) by PARTFUN1:def 6
.= I.(i+1) by A7,FINSEQ_1:def 7
.= I/.(i+1) by A7,PARTFUN1:def 6;
end;
defpred P0[Element of NAT] means
$1 <= len G - 1 implies (PartDiffSeq(f,Z,G^I)).$1 =(PartDiffSeq(f,Z,G)).$1;
A8:P0[0]
proof
assume 0 <= len G - 1;
(PartDiffSeq(f,Z,G^I)).0 = f by PDIFF_9:def 7;
hence (PartDiffSeq(f,Z,G^I)).0 = (PartDiffSeq(f,Z,G)).0 by PDIFF_9:def 7;
end;
A9:for k be Element of NAT st P0[k] holds P0[k+1]
proof
let k be Element of NAT;
assume
A10: P0[k];
assume
A11: k+1 <= len G - 1;
A12:k <= k+1 by NAT_1:11;
thus (PartDiffSeq(f,Z,G^I)).(k+1)
= ((PartDiffSeq(f,Z,G^I)).k)`partial|(Z,(G^I)/.(k+1)) by PDIFF_9:def 7
.= ((PartDiffSeq(f,Z,G)).k)`partial|(Z,G/.(k+1))
by A12,A2,A10,A11,XXREAL_0:2
.= (PartDiffSeq(f,Z,G)).(k+1) by PDIFF_9:def 7;
end;
A13:for n be Element of NAT holds P0[n] from NAT_1:sch 1(A8,A9);
reconsider j= (len G)-1 as Element of NAT by INT_1:5,FINSEQ_1:20;
A14:(PartDiffSeq(f,Z,G^I)).(len G)
= ((PartDiffSeq(f,Z,G^I)).j)`partial|(Z,(G^I)/.(j+1))
by PDIFF_9:def 7
.= ((PartDiffSeq(f,Z,G)).j)`partial|(Z,(G^I)/.(j+1)) by A13
.= ((PartDiffSeq(f,Z,G)).j)`partial|(Z,G/.(j+1)) by A2
.= (PartDiffSeq(f,Z,G)).(len G) by PDIFF_9:def 7;
defpred P[Element of NAT] means
$1 <= (len I) -1 implies
(PartDiffSeq(g,Z,I)).$1 =(PartDiffSeq(f,Z,(G^I))).(len G + $1);
A15:P[0] by A14,PDIFF_9:def 7;
A16:for k be Element of NAT st P[k] holds P[k+1]
proof
let k be Element of NAT;
assume
A17: P[k];
set i = (len G) + k;
assume
A18: k+1 <= (len I) -1;
A19: k <= k+1 by NAT_1:11;
(G^I)/.(i+1) = (G^I)/.(len G + (k+1));
then
A20: (G^I)/.(i+1) = I/.(k+1) by A5,A19,A18,XXREAL_0:2;
(PartDiffSeq(f,Z,(G^I))).(len G + (k+1))
= ((PartDiffSeq(f,Z,(G^I))).i)`partial|(Z,(G^I)/.(i+1)) by PDIFF_9:def 7;
hence thesis by A19,A18,A17,A20,PDIFF_9:def 7,XXREAL_0:2;
end;
A21:for n be Element of NAT holds P[ n ] from NAT_1:sch 1(A15,A16);
reconsider j0= (len I)-1 as Element of NAT by INT_1:5,FINSEQ_1:20;
reconsider j1= (len (G^I))-1 as Element of NAT by INT_1:5,FINSEQ_1:20;
A22:j1= len G + j0 by A4;
f `partial|(Z,G^I)
= ((PartDiffSeq(f,Z,G^I)).j1)`partial|(Z,(G^I)/.(j1+1)) by PDIFF_9:def 7
.= ((PartDiffSeq(g,Z,I)).j0)`partial|(Z,(G^I)/.(len G + (j0+1)))
by A21,A22
.= ((PartDiffSeq(g,Z,I)).j0)`partial|(Z,I/.(j0+1)) by A5
.= g `partial|(Z,I) by PDIFF_9:def 7;
hence thesis;
end;
theorem
for m be non zero Element of NAT, Z be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL, I,G be non empty FinSequence of NAT
holds
f `partial|(Z,G^I) is_continuous_on Z
iff f`partial|(Z,G) `partial|(Z,I) is_continuous_on Z by Th07;
theorem Th09:
for m be non zero Element of NAT, Z be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL, i,j be Element of NAT,
I be non empty FinSequence of NAT
st f is_continuously_differentiable_up_to_order (i+j),Z
& rng I c= Seg m & len I = j
holds
f`partial|(Z,I) is_continuously_differentiable_up_to_order i,Z
proof
let m be non zero Element of NAT, Z be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL, i,j be Element of NAT,
I be non empty FinSequence of NAT;
assume
AS1: f is_continuously_differentiable_up_to_order (i+j),Z
& rng I c= Seg m & len I = j;
then
A1: Z c= dom f & f is_partial_differentiable_up_to_order (i+j),Z
& for I be non empty FinSequence of NAT
st len I <= (i+j) & rng I c= Seg m
holds f`partial|(Z,I) is_continuous_on Z by defX1;
f is_partial_differentiable_on Z,I by A1,AS1,PDIFF_9:def 10,NAT_1:11;
hence Z c= dom (f`partial|(Z,I)) by Th01;
thus f`partial|(Z,I) is_partial_differentiable_up_to_order i,Z
by PDIFF_9:78,defX1,AS1;
let J be non empty FinSequence of NAT;
assume
AS2:len J <= i & rng J c= Seg m;
reconsider G = I^J as non empty FinSequence of NAT;
A2:rng G = rng I \/ rng J by FINSEQ_1:31;
len G = len I + len J by FINSEQ_1:22;
then
len G <= i+j & rng G c= Seg m by AS2,A2,AS1,XBOOLE_1:8,XREAL_1:6;
then f`partial|(Z,G) is_continuous_on Z by AS1,defX1;
hence thesis by Th07;
end;
theorem Th10:
for m be non zero Element of NAT, Z be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL, i,j be Element of NAT
st f is_continuously_differentiable_up_to_order i,Z & j <= i
holds f is_continuously_differentiable_up_to_order j,Z
proof
let m be non zero Element of NAT, Z be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL, i,j be Element of NAT;
assume
AS: f is_continuously_differentiable_up_to_order i,Z & j <= i;
hence Z c= dom f by defX1;
thus
f is_partial_differentiable_up_to_order j,Z by PDIFF_9:79,AS,defX1;
let I be non empty FinSequence of NAT;
assume len I <= j & rng I c= Seg m;
hence thesis by AS,XXREAL_0:2,defX1;
end;
theorem Th11:
for m be non zero Element of NAT, Z be non empty Subset of REAL m
st Z is open
holds
for k be Element of NAT,f,g be PartFunc of REAL m,REAL st
f is_continuously_differentiable_up_to_order k,Z &
g is_continuously_differentiable_up_to_order k,Z
holds
f(#)g is_continuously_differentiable_up_to_order k,Z
proof
let m be non zero Element of NAT, Z be non empty Subset of REAL m;
assume
AS: Z is open;
defpred P[Element of NAT] means
for f,g be PartFunc of REAL m,REAL
st f is_continuously_differentiable_up_to_order $1,Z
& g is_continuously_differentiable_up_to_order $1,Z
holds f(#)g is_continuously_differentiable_up_to_order $1,Z;
set Z0 = (0 qua Nat);
A1:P[0]
proof
let f,g be PartFunc of REAL m,REAL;
assume
A2: f is_continuously_differentiable_up_to_order 0,Z
& g is_continuously_differentiable_up_to_order 0,Z;
then
A3: Z c= dom f & f is_partial_differentiable_up_to_order 0,Z &
for I be non empty FinSequence of NAT
st len I <= 0 & rng I c= Seg m
holds f`partial|(Z,I) is_continuous_on Z by defX1;
A4: Z c= dom g & g is_partial_differentiable_up_to_order 0,Z &
for I be non empty FinSequence of NAT
st len I <= 0 & rng I c= Seg m
holds g`partial|(Z,I) is_continuous_on Z by A2,defX1;
A5: dom (f (#) g) = dom f /\ dom g by VALUED_1:def 4;
A6: (f (#) g) is_partial_differentiable_up_to_order 0,Z
by PDIFF_9:82,AS,A3,A4;
for I be non empty FinSequence of NAT st len I <= Z0 & rng I c= Seg m
holds (f(#)g) `partial|(Z,I) is_continuous_on Z by FINSEQ_1:20;
hence
f(#)g is_continuously_differentiable_up_to_order 0,Z
by A5,A6,defX1,A3,A4,XBOOLE_1:19;
end;
A7:for k be Element of NAT st P[k] holds P[k+1]
proof
let k be Element of NAT;
assume
A8: P[k];
let f,g be PartFunc of REAL m,REAL;
assume
A9: f is_continuously_differentiable_up_to_order k+1,Z
& g is_continuously_differentiable_up_to_order k+1,Z;
then
A10: f is_continuously_differentiable_up_to_order k,Z
& g is_continuously_differentiable_up_to_order k,Z by Th10,NAT_1:11;
A11:Z c= dom f & f is_partial_differentiable_up_to_order k+1,Z &
for I be non empty FinSequence of NAT st len I <= k+1 & rng I c= Seg m
holds f`partial|(Z,I) is_continuous_on Z by A9,defX1;
A12:Z c= dom g & g is_partial_differentiable_up_to_order k+1,Z &
for I be non empty FinSequence of NAT st len I <= k+1 & rng I c= Seg m
holds g`partial|(Z,I) is_continuous_on Z by A9,defX1;
dom (f (#) g) = dom f /\ dom g by VALUED_1:def 4;
then
A13: Z c= dom (f(#)g) by A11,A12,XBOOLE_1:19;
now let I be non empty FinSequence of NAT;
assume
A14: len I <= k+1 & rng I c= Seg m;
then
A15: f is_partial_differentiable_on Z,I
& g is_partial_differentiable_on Z,I by PDIFF_9:def 10,A9,defX1;
A16: f `partial|(Z,I) is_continuous_on Z
& g `partial|(Z,I) is_continuous_on Z by A14,A9,defX1;
A17: 1 <= len I by FINSEQ_1:20;
then
A18: 1 in dom I by FINSEQ_3:25;
then
A19: I/.1 = I.1 by PARTFUN1:def 6;
A20: I.1 in rng I by A18,FUNCT_1:3;
reconsider i = I.1 as Element of NAT by ORDINAL1:def 12;
A21: 1 <= i & i <= m by A20,A14,FINSEQ_1:1;
per cases;
suppose
A22: 1 = len I;
then
A23: I = <*I/.1*> by FINSEQ_5:14;
A24: f(#)g is_continuously_differentiable_up_to_order k,Z by A8,A10;
now per cases;
suppose
A25: k = 0;
A26: I = <*i*> by A19,A22,FINSEQ_5:14;
A27: f is_partial_differentiable_on Z,i
& g is_partial_differentiable_on Z,i by A19,A23,A15,PDIFF_9:76;
A28: (f(#)g)`partial|(Z,I) = (f(#)g)`partial|(Z,i) by A26,PDIFF_9:77
.=(f`partial|(Z,i))(#)g + f(#)(g`partial|(Z,i))
by A27,A21,PDIFF_9:68,AS
.= f`partial|(Z,I)(#)g + f(#)(g`partial|(Z,i))
by A26,PDIFF_9:77
.= f`partial|(Z,I)(#)g + f(#)(g`partial|(Z,I))
by A26,PDIFF_9:77;
A29: Z c= dom (f`partial|(Z,I)) & Z c= dom (g`partial|(Z,I))
by A15,Th01;
A30: f is_continuous_on Z by AS,A11,Th03,A9,A25;
g is_continuous_on Z by AS,A12,Th03,A9,A25;
then
A31: f`partial|(Z,I)(#)g is_continuous_on Z
by A16,A12,A29,PDIFF_9:48;
A32: f(#)(g`partial|(Z,I)) is_continuous_on Z
by A16,A30,A11,A29,PDIFF_9:48;
dom (f`partial|(Z,I)(#)g) = dom (f`partial|(Z,I)) /\ dom g
by VALUED_1:def 4;
then
A33: Z c= dom (f`partial|(Z,I)(#)g) by A29,A12,XBOOLE_1:19;
dom (f(#)(g`partial|(Z,I))) = dom f /\ dom (g`partial|(Z,I))
by VALUED_1:def 4;
then
Z c= dom (f(#)(g`partial|(Z,I))) by A29,A11,XBOOLE_1:19;
hence (f(#)g) `partial|(Z,I) is_continuous_on Z
by A28,A31,A32,A33,PDIFF_9:46;
end;
suppose k <> 0;
hence (f(#)g) `partial|(Z,I) is_continuous_on Z
by A24,A14,defX1,A22,NAT_1:14;
end;
end;
hence (f(#)g) `partial|(Z,I) is_continuous_on Z;
end;
suppose 1 <> len I;
then 1 < len I by A17,XXREAL_0:1;
then 1+1 <= len I by NAT_1:13;
then 1 <= len I - 1 by XREAL_1:19;
then 1 <= len (I/^1) by A17,RFINSEQ:def 1;
then
reconsider J = I/^1 as non empty FinSequence of NAT by FINSEQ_1:20;
set I1 = <*i*>;
len I - 1 <= k by A14,XREAL_1:20;
then
A34: len J <= k by A17,RFINSEQ:def 1;
A35: I = <*I/.1*>^(I/^1) by FINSEQ_5:29;
then
A36: rng I1 c= rng I & rng J c= rng I by A19,FINSEQ_1:29,30;
then
A37: rng J c= Seg m by A14,XBOOLE_1:1;
I = I1^J by A19,FINSEQ_5:29;
then
A38: f is_partial_differentiable_on Z,i
& g is_partial_differentiable_on Z,i
by PDIFF_9:76,PDIFF_9:75,A15;
A39: (f(#)g)`partial|(Z,I1) = (f(#)g)`partial|(Z,i) by PDIFF_9:77
.=(f`partial|(Z,i))(#)g + f(#)(g`partial|(Z,i))
by A38,A21,PDIFF_9:68,AS
.= f`partial|(Z,I1)(#)g + f(#)(g`partial|(Z,i)) by PDIFF_9:77
.= f`partial|(Z,I1)(#)g + f(#)(g`partial|(Z,I1)) by PDIFF_9:77;
len I1 =1 & rng I1 c= Seg m by A36,A14,FINSEQ_1:39,XBOOLE_1:1;
then
f`partial|(Z,I1) is_continuously_differentiable_up_to_order k,Z
& g`partial|(Z,I1) is_continuously_differentiable_up_to_order k,Z
by Th09,A9;
then
A40: f`partial|(Z,I1)(#)g is_continuously_differentiable_up_to_order k,Z
& f(#)(g`partial|(Z,I1))
is_continuously_differentiable_up_to_order k,Z
by A8,A10;
then
A41: f`partial|(Z,I1)(#)g is_partial_differentiable_on Z,J
& f(#)(g`partial|(Z,I1)) is_partial_differentiable_on Z,J
by A34,A37,PDIFF_9:def 10,defX1;
then
A42: (f`partial|(Z,I1) (#)g + f(#)(g`partial|(Z,I1)))`partial|(Z,J)
=(f`partial|(Z,I1) (#)g ) `partial|(Z,J)
+ ( f(#)(g`partial|(Z,I1)))`partial|(Z,J) by AS,A37,PDIFF_9:70;
A43: Z c= dom((f`partial|(Z,I1) (#)g ) `partial|(Z,J))
& Z c= dom (( f(#)(g`partial|(Z,I1)))`partial|(Z,J)) by A41,Th01;
(f`partial|(Z,I1) (#)g ) `partial|(Z,J) is_continuous_on Z
& ( f(#)(g`partial|(Z,I1)))`partial|(Z,J) is_continuous_on Z
by A40,A34,defX1,A14,XBOOLE_1:1,A36;
then
(f`partial|(Z,I1) (#)g + f(#)(g`partial|(Z,I1)))`partial|(Z,J)
is_continuous_on Z by A42,A43,PDIFF_9:46;
hence (f(#)g)`partial|(Z,I) is_continuous_on Z by A35,A19,A39,Th07;
end;
end;
hence f(#)g is_continuously_differentiable_up_to_order k+1,Z
by A13,defX1,PDIFF_9:82,AS,A11,A12;
end;
for n be Element of NAT holds P[ n ] from NAT_1:sch 1(A1,A7);
hence thesis;
end;
theorem Th12:
for m be non zero Element of NAT, f be PartFunc of REAL m,REAL,
X be non empty Subset of REAL m, d be Real
st X is open & f = X --> d
holds
for x be Element of REAL m st x in X holds
f is_differentiable_in x & diff(f,x) = REAL m --> 0
proof
let m be non zero Element of NAT, f be PartFunc of REAL m,REAL,
X be non empty Subset of REAL m, d be Real;
assume
AS1:X is open & f = X --> d;
let x be Element of REAL m;
assume
AS2:x in X;
d in REAL by XREAL_0:def 1; then
<*d*> in 1-tuples_on REAL by FINSEQ_2:98;
then
<*d*> in REAL 1 by EUCLID:def 1;
then
reconsider rd=<*d*> as Point of REAL-NS 1 by REAL_NS1:def 4;
A1:the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS 1) = REAL 1
by REAL_NS1:def 4;
then
reconsider g = <>*f as PartFunc of REAL-NS m,REAL-NS 1;
reconsider x1 = x as Point of REAL-NS m by REAL_NS1:def 4;
set ZR= 0.R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS 1);
A2:0.(REAL-NS 1) = 0*1 by REAL_NS1:def 4
.= 1 |-> (0 qua Real) by EUCLID:def 4
.= <* 0 *> by FINSEQ_2:59;
A3:ZR = REAL m --> <* 0 *> by A2,A1,LOPBAN_1:31;
reconsider Z= X as Subset of REAL-NS m by REAL_NS1:def 4;
A4:Z is open by PDIFF_9:10,AS1;
A5:dom f = X by AS1,FUNCT_2:def 1;
then
A6: dom (<>*f) = X by PDIFF_9:3;
then
A7: Z = dom g;
now let x be element;
assume x in dom(<>*f);
then
A8: x in X by A5,PDIFF_9:3;
then reconsider x1=x as Element of REAL m;
(<>*f).x = <* f.x1 *> by A5,A8,PDIFF_9:6;
hence (<>*f).x = <* d *> by AS1,A8,FUNCOP_1:7;
end;
then
A11: <>*f = X --> <* d *> by A6,FUNCOP_1:11;
rng g = {rd} by A11,FUNCOP_1:8; then
A13:g is_differentiable_on Z
& for x be Point of REAL-NS m st x in Z
holds (g`|Z)/.x = ZR by NDIFF_1:33,A4,A7;
then
A14:g is_differentiable_in x1 by AS2,NDIFF_1:31,A4;
A15:ZR = (g`|Z)/.x1 by A13,AS2
.= diff(g,x1) by AS2,NDIFF_1:def 9,A13;
A16:<>*f is_differentiable_in x by PDIFF_6:2,A14;
hence f is_differentiable_in x by PDIFF_7:def 1;
A17:diff(<>*f,x) = REAL m --> <* 0 *> by A3,A15,A16,PDIFF_6:3;
A19:dom (proj(1,1)*diff(<>*f,x) ) = REAL m by FUNCT_2:def 1;
now let y be element;
assume
AS3: y in dom (proj(1,1)*diff(<>*f,x) );
then reconsider y1=y as Element of REAL m;
thus (proj(1,1)*diff(<>*f,x) ).y
= proj(1,1).((diff(<>*f,x) ).y1) by AS3,FUNCT_1:12
.= proj(1,1).(<* 0 *>) by A17,FUNCOP_1:7
.= 0 by PDIFF_1:1;
end;
then proj(1,1)*diff(<>*f,x) = dom (proj(1,1)*diff(<>*f,x) ) --> 0
by FUNCOP_1:11;
hence diff(f,x) = REAL m --> 0 by PDIFF_7:def 2,A19;
end;
theorem Th13:
for m be non zero Element of NAT, f be PartFunc of REAL m,REAL,
X be non empty Subset of REAL m, d be Real
st X is open & f = X --> d
holds
for x0 be Element of REAL m,r be Real st x0 in X & 0 < r
ex s be Real
st 0 < s & for x1 be Element of REAL m st x1 in X & |. x1- x0 .| < s
holds for v be Element of REAL m
holds |. diff(f,x1).v - diff(f,x0).v.| <= r * |.v.|
proof
let m be non zero Element of NAT, f be PartFunc of REAL m,REAL,
X be non empty Subset of REAL m, d be Real;
assume
AS1: X is open & f = X --> d;
let x0 be Element of REAL m,r be Real;
assume
AS2: x0 in X & 0 < r;
take s=1 qua Real;
thus 0 < s;
let x1 be Element of REAL m;
assume
AS3: x1 in X & |. x1- x0 .| < s;
let v be Element of REAL m;
A1:diff(f,x1).v = (REAL m --> 0).v by AS1,Th12,AS3
.= (0 qua Real) by FUNCOP_1:7;
diff(f,x0).v = (REAL m --> 0).v by AS1,Th12,AS2
.= (0 qua Real) by FUNCOP_1:7;
hence |. diff(f,x1).v - diff(f,x0).v.| <= r * |.v.| by A1,AS2,COMPLEX1:44;
end;
theorem Th14:
for m be non zero Element of NAT, f be PartFunc of REAL m,REAL,
X be non empty Subset of REAL m, d be Real
st X is open & f = X --> d
holds
f is_differentiable_on X & dom (f`|X) = X
& for x be Element of REAL m st x in X
holds (f`|X)/.x = (REAL m --> 0)
proof
let m be non zero Element of NAT, f be PartFunc of REAL m,REAL,
X be non empty Subset of REAL m, d be Real;
assume
AS: X is open & f = X --> d;
A1:X = dom f by AS,FUNCT_2:def 1;
for x be Element of REAL m st x in X holds f is_differentiable_in x
by Th12,AS;
hence f is_differentiable_on X by A1,AS,PDIFF_9:54;
thus dom (f`|X) = X by PDIFF_9:def 4,A1;
thus for x be Element of REAL m st x in X holds (f`|X)/.x = REAL m --> 0
proof
let x be Element of REAL m;
assume
A2: x in X;
thus (f`|X)/.x = diff(f,x) by A1,PDIFF_9:def 4,A2
.= REAL m --> 0 by A2,Th12,AS;
end;
end;
theorem Th15:
for m be non zero Element of NAT, f be PartFunc of REAL m,REAL,
X be non empty Subset of REAL m, d be Real, i be Element of NAT
st X is open & f = X --> d & 1 <= i & i <= m
holds
f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X
proof
let m be non zero Element of NAT, f be PartFunc of REAL m,REAL,
X be non empty Subset of REAL m, d be Real, i be Element of NAT;
assume
AS1: X is open;
assume
AS2: f = X --> d;
assume
AS3: 1 <= i & i <= m;
A1:dom f = X by AS2,FUNCT_2:def 1;
A2:f is_differentiable_on X by Th14,AS2,AS1;
for x0 be Element of REAL m,r be Real st x0 in X & 0 < r
ex s be Real
st 0 < s & for x1 be Element of REAL m st x1 in X & |. x1- x0 .| < s
holds for v be Element of REAL m
holds |. diff(f,x1).v - diff(f,x0).v.| <= r * |.v.| by AS2,Th13,AS1;
hence thesis by AS3,A1,AS1,A2,PDIFF_9:63;
end;
theorem Th16:
for m be non zero Element of NAT, i be Element of NAT,
f be PartFunc of REAL m,REAL, X be non empty Subset of REAL m,
d be Real st X is open & f = X --> d & 1 <= i & i <= m
holds
f`partial|(X,i) = X --> 0
proof
let m be non zero Element of NAT, i be Element of NAT,
f be PartFunc of REAL m,REAL, X be non empty Subset of REAL m,
d be Real;
assume
AS: X is open & f = X --> d & 1 <= i & i <= m;
A1:f is_partial_differentiable_on X,i by AS,Th15;
A2:dom (f`partial|(X,i)) = X by A1,PDIFF_9:def 6;
now let x be element;
assume
A3: x in dom (f`partial|(X,i));
then
reconsider x1=x as Element of REAL m;
A4: f is_differentiable_in x1 & diff(f,x1) = REAL m --> 0 by Th12,AS,A2,A3;
A: (reproj(i,0*m).1) in REAL m by XREAL_0:def 1,FUNCT_2:5;
A5: partdiff(f,x1,i) = diff(f,x1).(reproj(i,0*m).1) by PDIFF_7:23,A4,AS
.= 0 by A,FUNCOP_1:7,A4;
thus (f`partial|(X,i)).x =(f`partial|(X,i))/.x1 by A3,PARTFUN1:def 6
.= 0 by A5,A1,A3,A2,PDIFF_9:def 6;
end;
hence thesis by A2,FUNCOP_1:11;
end;
XX11:
for m be non zero Element of NAT, I be non empty FinSequence of NAT,
i be Element of NAT st rng I c= Seg m & i <= (len I)-1
holds
1 <= I/.(i+1) & I/.(i+1) <= m
proof
let m be non zero Element of NAT,
I be non empty FinSequence of NAT,
i be Element of NAT;
assume
AS1:rng I c= Seg m;
assume
AS2: i <= (len I)-1;
A1: (0 qua Real) + 1 <= i + 1 by XREAL_1:6;
i + 1 <= len I -1 + 1 by AS2,XREAL_1:6;
then i+1 in Seg (len I) by A1;
then
A2: i+1 in dom I by FINSEQ_1:def 3;
then I.(i+1) in rng I by FUNCT_1:3;
then I/.(i+1) in rng I by A2,PARTFUN1:def 6;
hence 1 <= I/.(i+1) & I/.(i+1) <= m by FINSEQ_1:1,AS1;
end;
XX12:
for m be non zero Element of NAT, I be non empty FinSequence of NAT,
i be Element of NAT st rng I c= Seg m & 1 <= i & i <= len I
holds
1 <= I/.i & I/.i <= m
proof
let m be non zero Element of NAT,
I be non empty FinSequence of NAT,
i be Element of NAT;
assume
AS: rng I c= Seg m;
assume 1 <= i & i <= len I;
then i in Seg (len I);
then
A1: i in dom I by FINSEQ_1:def 3;
then I.i in rng I by FUNCT_1:3;
then I/.i in rng I by A1,PARTFUN1:def 6;
hence 1 <= I/.i & I/.i <= m by FINSEQ_1:1,AS;
end;
theorem Th17:
for m be non zero Element of NAT, I be non empty FinSequence of NAT,
X be non empty Subset of REAL m, f be PartFunc of REAL m,REAL,
d be Real st X is open & f = X --> d & rng I c= Seg m
holds
(PartDiffSeq(f,X,I)).0 = X --> d
&
for i be Element of NAT st 1<=i & i <= len I
holds (PartDiffSeq(f,X,I)).i = X --> 0
proof
let m be non zero Element of NAT,
I be non empty FinSequence of NAT,
X be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL,
d be Real;
assume
AS1:X is open & f = X --> d & rng I c= Seg m;
thus
A1: (PartDiffSeq(f,X,I)).0 = X --> d by AS1,PDIFF_9:def 7;
defpred P[Nat] means
1<=$1 & $1 <= (len I) implies (PartDiffSeq(f,X,I)).$1 = X --> 0;
A2:P[0];
A3:for i be Element of NAT st P[i] holds P[i+1]
proof
let i be Element of NAT;
assume
AS2: P[i];
assume
A4: 1<=i+1 & i+1 <= len I;
i <= i + 1 by NAT_1:12;
then
A5: i <= len I by XXREAL_0:2,A4;
per cases;
suppose i=0;
then
A6: (PartDiffSeq(f,X,I)).i = X --> d by A1;
A7: 1 <= I/.(i+1) & I/.(i+1) <= m by XX12,AS1,A4;
thus (PartDiffSeq(f,X,I)).(i+1)
= ((PartDiffSeq(f,X,I)).i)`partial|(X,I/.(i+1)) by PDIFF_9:def 7
.= X --> 0 by A6,A7,AS1,Th16;
end;
suppose i <> 0;
then
A8: (PartDiffSeq(f,X,I)).i = X --> 0 by A5,AS2,NAT_1:14;
A9: 1 <= I/.(i+1) & I/.(i+1) <= m by XX12,AS1,A4;
thus (PartDiffSeq(f,X,I)).(i+1)
= ((PartDiffSeq(f,X,I)).i)`partial|(X,I/.(i+1)) by PDIFF_9:def 7
.= X --> 0 by A8,A9,AS1,Th16;
end;
end;
for i be Element of NAT holds P[i] from NAT_1:sch 1(A2,A3);
hence thesis;
end;
theorem Th18:
for m be non zero Element of NAT, I be non empty FinSequence of NAT,
X be non empty Subset of REAL m,f be PartFunc of REAL m,REAL,
d be Real st X is open & f = X --> d & rng I c= Seg m
holds
f is_partial_differentiable_on X,I & f`partial|(X,I) is_continuous_on X
proof
let m be non zero Element of NAT,
I be non empty FinSequence of NAT,
X be non empty Subset of REAL m,
f be PartFunc of REAL m,REAL,
d be Real;
assume
AS1: X is open & f = X --> d & rng I c= Seg m;
for i be Element of NAT st i <= (len I)-1
holds (PartDiffSeq(f,X,I)).i is_partial_differentiable_on X,I/.(i+1)
proof
let i be Element of NAT;
assume
AS2: i <= (len I)-1;
(len I)-1 <= len I - (0 qua Real) by XREAL_1:10;
then
A1: i <= (len I) by AS2,XXREAL_0:2;
per cases;
suppose i=0;
then
A2: (PartDiffSeq(f,X,I)).i = X --> d by AS1,Th17;
1 <= I/.(i+1) & I/.(i+1) <= m by XX11,AS1,AS2;
hence thesis by A2,AS1,Th15;
end;
suppose i <> 0;
then
1 <= i by NAT_1:14;
then
A3: (PartDiffSeq(f,X,I)).i = X --> 0 by AS1,A1,Th17;
1 <= I/.(i+1) & I/.(i+1) <= m by XX11,AS1,AS2;
hence thesis by A3,AS1,Th15;
end;
end;
hence f is_partial_differentiable_on X,I by PDIFF_9:def 8;
reconsider k=(len I)-1 as Element of NAT by INT_1:5,FINSEQ_1:20;
A4: f`partial|(X,I) = ((PartDiffSeq(f,X,I)).k)`partial|(X,I/.(k+1))
by PDIFF_9:def 7;
a5: (len I) - 1 <= (len I) - (0 qua Real) by XREAL_1:10;
per cases;
suppose k = 0;
then
A6: (PartDiffSeq(f,X,I)).k = X --> d by AS1,Th17;
1 <= I/.(k+1) & I/.(k+1) <= m by AS1,XX11;
hence f`partial|(X,I) is_continuous_on X by AS1,A4,A6,Th15;
end;
suppose k <> 0;
then
1 <= k by NAT_1:14;
then
A7: (PartDiffSeq(f,X,I)).k = X --> 0 by AS1,a5,Th17;
1 <= I/.(k+1) & I/.(k+1) <= m by AS1,XX11;
hence f`partial|(X,I) is_continuous_on X by AS1,A4,A7,Th15;
end;
end;
theorem Th19:
for m be non zero Element of NAT, k be Element of NAT,
X be non empty Subset of REAL m, f be PartFunc of REAL m,REAL,
d be Real st X is open & f = X --> d
holds
f is_continuously_differentiable_up_to_order k,X
proof
let m be non zero Element of NAT, k be Element of NAT,
X be non empty Subset of REAL m, f be PartFunc of REAL m,REAL,
d be Real;
assume
AS: X is open & f = X --> d;
A1:X = dom f by FUNCT_2:def 1,AS;
for I be non empty FinSequence of NAT st len I <= k & rng I c= Seg m
holds f is_partial_differentiable_on X,I by AS,Th18;
then
A2:f is_partial_differentiable_up_to_order k,X by PDIFF_9:def 10;
for I be non empty FinSequence of NAT st len I <= k & rng I c= Seg m
holds f`partial|(X,I) is_continuous_on X by AS,Th18;
hence thesis by A1,A2,defX1;
end;
registration ::: should be moved to PDIFF_7
let m be non zero Element of NAT;
cluster open for non empty Subset of REAL m;
correctness
proof
REAL m c= REAL m;
then
reconsider X = REAL m as non empty Subset of REAL m;
for x be Element of REAL m st x in X holds
ex r be Real st r>0 & {y where y is Element of REAL m: |. y-x .| < r} c= X
proof
let x be Element of REAL m;
assume x in X;
take r = 1;
thus r > 0;
now let z be element;
assume z in {y where y is Element of REAL m: |. y-x .| < r};
then ex y be Element of REAL m st z=y & |. y-x .| < r;
hence z in X;
end;
hence
{y where y is Element of REAL m: |. y-x .| < r} c= X by TARSKI:def 3;
end;
then X is open by PDIFF_7:31;
hence thesis;
end;
end;
begin
definition
let m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m;
func Ck_Functions(k,X) -> non empty Subset of RAlgebra X equals
{ f where f is PartFunc of REAL m,REAL
: f is_continuously_differentiable_up_to_order k,X & dom f = X };
correctness
proof
A1:{ f where f is PartFunc of REAL m,REAL
: f is_continuously_differentiable_up_to_order k,X & dom f = X }
c= Funcs(X,REAL)
proof
let x be element;
assume x in { f where f is PartFunc of REAL m,REAL
: f is_continuously_differentiable_up_to_order k,X & dom f = X };
then
consider f be PartFunc of REAL m,REAL such that
A2: x=f & f is_continuously_differentiable_up_to_order k,X & dom f = X;
rng f c= REAL;
then
f is Function of X,REAL by A2,FUNCT_2:2;
hence x in Funcs(X,REAL) by A2,FUNCT_2:8;
end;
A3:X --> 0 is Function of X,REAL by XREAL_0:def 1,FUNCOP_1:45;
dom (X --> 0) = X by FUNCT_2:def 1;
then
reconsider g = X --> 0 as PartFunc of REAL m,REAL by A3,RELSET_1:5;
A4:dom g = X by FUNCT_2:def 1;
g is_continuously_differentiable_up_to_order k,X by Th19;
then
g in { f where f is PartFunc of REAL m,REAL
: f is_continuously_differentiable_up_to_order k,X & dom f = X }
by A4;
hence thesis by A1;
end;
end;
registration
let m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m;
cluster Ck_Functions(k,X) -> additively-linearly-closed
multiplicatively-closed;
coherence
proof
set W = Ck_Functions(k,X);
set V = RAlgebra X;
A1:RAlgebra X is RealLinearSpace by C0SP1:7;
for v,u be Element of V st v in W & u in W holds v + u in W
proof
let v,u be Element of V such that
A2: v in W & u in W;
consider v1 be PartFunc of REAL m,REAL such that
A3: v1=v & v1 is_continuously_differentiable_up_to_order k,X
& dom v1 = X by A2;
consider u1 be PartFunc of REAL m, REAL such that
A4: u1=u & u1 is_continuously_differentiable_up_to_order k,X
& dom u1 = X by A2;
a: dom (v1+u1) = dom v1 /\ dom u1 by VALUED_1:def 1;
A6: v1+u1 is_continuously_differentiable_up_to_order k,X by A3,A4,Th04;
reconsider h = v+u as Element of Funcs(X,REAL);
A7: ex f being Function st h = f & dom f = X
& rng f c= REAL by FUNCT_2:def 2;
A8: dom v1 /\ dom u1 = X /\ X by A4,A3;
for x be element st x in dom h holds h.x = v1.x + u1.x
by A3,A4,FUNCSDOM:1;
then v+u=v1+u1 by A8,A7,VALUED_1:def 1;
hence v+u in W by A6,A3,A4,a;
end;
then
A9: W is add-closed by IDEAL_1:def 1;
for v be Element of V st v in W holds -v in W
proof
let v be Element of V such that
A10: v in W;
consider v1 be PartFunc of REAL m,REAL such that
A11: v1=v & v1 is_continuously_differentiable_up_to_order k,X
& dom v1 = X by A10;
A12:dom (-v1) = X by VALUED_1:def 5,A11;
A14: -v1 is_continuously_differentiable_up_to_order k,X by A11,Th05;
reconsider h = -v, v2 = v as Element of Funcs(X,REAL);
A15:h=(-1)*v by A1,RLVECT_1:16;
A16:ex f being Function st h = f & dom f = X & rng f c= REAL by FUNCT_2:def 2;
now let x be element;
assume x in dom h;
then reconsider y=x as Element of X;
h.x = (-1)*(v2.y) by A15,FUNCSDOM:4;
hence h.x = -v1.x by A11;
end;
then -v=-v1 by A11,A16,VALUED_1:9;
hence -v in W by A14,A12;
end;
then
A17:W is having-inverse by C0SP1:def 1;
for a be Real, u be Element of V st u in W holds a * u in W
proof
let a be Real, u be Element of V such that
A18: u in W;
consider u1 be PartFunc of REAL m, REAL such that
A19: u1=u & u1 is_continuously_differentiable_up_to_order k,X & dom u1 = X
by A18;
A20:dom (a(#)u1) = X by A19,VALUED_1:def 5;
A21:a(#)u1 is_continuously_differentiable_up_to_order k,X by A19, Th05;
reconsider h = a*u as Element of Funcs(X,REAL);
A22:ex f being Function st h = f & dom f = X & rng f c= REAL by FUNCT_2:def 2;
for x be element st x in dom h holds h.x = a*(u1.x) by A19,FUNCSDOM:4;
then a*u=a(#)u1 by A19,A22,VALUED_1:def 5;
hence a*u in W by A21,A20;
end;
hence Ck_Functions(k,X) is additively-linearly-closed
by A9,A17,C0SP1:def 10;
A23:for v,u be Element of V st v in W & u in W holds v * u in W
proof
let v,u be Element of V such that
A24: v in W & u in W;
consider v1 be PartFunc of REAL m,REAL such that
A25: v1=v & v1 is_continuously_differentiable_up_to_order k,X
& dom v1 = X by A24;
consider u1 be PartFunc of REAL m,REAL such that
A26: u1=u & u1 is_continuously_differentiable_up_to_order k,X
& dom u1 = X by A24;
A27:dom (v1(#)u1) = dom v1 /\ dom u1 by VALUED_1:def 4
.= X by A25,A26;
A28:v1(#)u1 is_continuously_differentiable_up_to_order k,X by A25,A26,Th11;
reconsider h = v*u as Element of Funcs(X,REAL);
A29:ex f being Function st h = f & dom f = X & rng f c= REAL by FUNCT_2:def 2;
A30: dom v1 /\ dom u1 = X /\ X by A26,A25;
for x be element st x in dom h holds h.x = v1.x *u1.x
by A25,A26,FUNCSDOM:2;
then v*u=v1(#)u1 by A30,A29,VALUED_1:def 4;
hence v*u in W by A28,A27;
end;
set g = RealFuncUnit X;
dom g = X by FUNCT_2:def 1;
then
reconsider g as PartFunc of REAL m,REAL by RELSET_1:5;
A31: dom g = X by FUNCT_2:def 1;
g is_continuously_differentiable_up_to_order k,X by Th19;
then 1.V in W by A31;
hence thesis by A23,C0SP1:def 4;
end;
end;
definition
let m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m;
func R_Algebra_of_Ck_Functions(k,X) -> Subalgebra of RAlgebra X equals
AlgebraStr (# Ck_Functions(k,X),
mult_(Ck_Functions(k,X),RAlgebra X),
Add_(Ck_Functions(k,X),RAlgebra X),
Mult_(Ck_Functions(k,X),RAlgebra X),
One_(Ck_Functions(k,X),RAlgebra X),
Zero_(Ck_Functions(k,X),RAlgebra X) #);
coherence by C0SP1:6;
end;
registration
let m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m;
cluster R_Algebra_of_Ck_Functions(k,X) -> Abelian add-associative
right_zeroed right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital
commutative associative right_unital right-distributive
scalar-associative vector-associative;
coherence
proof
now let v be VECTOR of R_Algebra_of_Ck_Functions(k,X);
reconsider v1=v as VECTOR of RAlgebra X by TARSKI:def 3;
1 * v = 1*v1 by C0SP1:8;
hence 1 * v =v by FUNCSDOM:12;
end;
hence thesis by RLVECT_1:def 8;
end;
end;
theorem
for m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m,
F,G,H being VECTOR of R_Algebra_of_Ck_Functions(k,X),
f,g,h being PartFunc of REAL m, REAL
holds
(f=F & g=G & h=H implies ( H = F+G iff
(for x be Element of X holds h.x = f.x + g.x)))
proof
let m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m;
let F,G,H be VECTOR of R_Algebra_of_Ck_Functions(k,X);
let f,g,h be PartFunc of REAL m, REAL;
assume
A1: f=F & g=G & h=H;
reconsider f1=F, g1=G, h1=H as VECTOR of RAlgebra X by TARSKI:def 3;
hereby assume
A3: H = F+G;
let x be Element of X;
h1=f1+g1 by A3,C0SP1:8;
hence h.x = f.x+g.x by A1,FUNCSDOM:1;
end;
assume for x be Element of X holds h.x = f.x+g.x;
then h1=f1+g1 by A1,FUNCSDOM:1;
hence H =F+G by C0SP1:8;
end;
theorem
for m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m,
F,G,H being VECTOR of R_Algebra_of_Ck_Functions(k,X),
f,g,h being PartFunc of REAL m, REAL,
a being Real
holds
(f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x ))
proof
let m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m,
F,G,H be VECTOR of R_Algebra_of_Ck_Functions(k,X),
f,g,h be PartFunc of REAL m, REAL,
a be Real;
assume
A1: f=F & g=G;
reconsider f1=F, g1=G as VECTOR of RAlgebra X by TARSKI:def 3;
hereby assume
A3: G = a*F;
let x be Element of X;
g1=a*f1 by A3,C0SP1:8;
hence g.x=a*f.x by A1,FUNCSDOM:4;
end;
assume for x be Element of X holds g.x=a*f.x;
then g1=a*f1 by A1,FUNCSDOM:4;
hence G =a*F by C0SP1:8;
end;
theorem
for m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m,
F,G,H being VECTOR of R_Algebra_of_Ck_Functions(k,X),
f,g,h being PartFunc of REAL m, REAL
holds
(f=F & g=G & h=H implies ( H = F*G iff (for x be Element of X
holds h.x = f.x * g.x)))
proof
let m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m,
F,G,H be VECTOR of R_Algebra_of_Ck_Functions(k,X),
f,g,h be PartFunc of REAL m, REAL;
assume
A1: f=F & g=G & h=H;
reconsider f1=F, g1=G, h1=H as VECTOR of RAlgebra X by TARSKI:def 3;
hereby assume
A3: H = F*G;
let x be Element of X;
h1 = f1*g1 by A3,C0SP1:8;
hence h.x = f.x * g.x by A1,FUNCSDOM:2;
end;
assume for x be Element of X holds h.x = f.x * g.x;
then h1 = f1 * g1 by A1,FUNCSDOM:2;
hence H = F * G by C0SP1:8;
end;
theorem
for m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m
holds
0.R_Algebra_of_Ck_Functions(k,X) = X --> 0
proof
let m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m;
0.RAlgebra X = X --> 0;
hence thesis by C0SP1:8;
end;
theorem
for m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m holds
1_R_Algebra_of_Ck_Functions(k,X) = X --> 1
proof
let m be non zero Element of NAT, k be Element of NAT,
X be non empty open Subset of REAL m;
1_RAlgebra X = X --> 1;
hence thesis by C0SP1:8;
end;