:: The $C^k$ Space
:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received November 9, 2012
:: Copyright (c) 2012-2026 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, VECTSP_1, VECTSP_2, VALUED_0, RELSET_1, NAT_1, FINSEQ_1,
EUCLID, REAL_NS1, FUNCT_2, XREAL_0;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI;
equalities ALGSTR_0, FINSEQ_1, FUNCSDOM, RLVECT_1, STRUCT_0, BINOP_1,
VALUED_1, PDIFF_9;
expansions TARSKI, RLVECT_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 Nat;
let Z be set;
pred f is_continuously_differentiable_up_to_order k,Z means
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 Th1:
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
A1: f is_partial_differentiable_on Z,I;
reconsider k=(len I)-1 as Element of NAT by INT_1:5,FINSEQ_1:20;
A2: 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 A1;
hence thesis by A2,PDIFF_9:def 6;
end;
theorem Th2:
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
A1: X is open & X c= dom f;
hereby assume
A2: f is_continuously_differentiable_up_to_order 1,X;
now let i be Nat;
assume
A3: 1 <= i & i <= m;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
set I = <*ii*>;
A4: len I = 1 by FINSEQ_1:40;
i in Seg m by A3;
then {i} c= Seg m by ZFMISC_1:31;
then
A5: rng I c= Seg m by FINSEQ_1:38;
then
A6: f`partial|(X,I) is_continuous_on X by A2,A4;
thus f is_partial_differentiable_on X,i by A4,A5,A2,PDIFF_9:def 11,81;
hence f`partial|(X,i) is_continuous_on X by A1,A3,PDIFF_9:82,A6;
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 A1,PDIFF_9:63;
end;
assume
A7: 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
A8: 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 A1,PDIFF_9:63;
A9:now let I be non empty FinSequence of NAT;
assume
A10: len I <= 1 & rng I c= Seg m;
A11:1 <= len I by FINSEQ_1:20;
then 1 in dom I by FINSEQ_3:25; then
A14:I.1 in rng I by FUNCT_1:3;
reconsider i = I.1 as Element of NAT by ORDINAL1:def 12;
A15:1 <= i & i <= m by A14,A10,FINSEQ_1:1;
A16:I = <*I.1*> by FINSEQ_5:14,A10,A11,XXREAL_0:1;
then
A17: I = <*i*>;
thus f is_partial_differentiable_on X,I by A16,PDIFF_9:81,A15,A8;
f`partial|(X,i) is_continuous_on X by A15,A1,PDIFF_9:63,A7;
hence f`partial|(X,I) is_continuous_on X by A1,A8,A17,A15,PDIFF_9:82;
end;
then
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;
hence f is_continuously_differentiable_up_to_order 1,X
by A1,A9,PDIFF_9:def 11;
end;
theorem Th3:
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
A1: X is open & X c= dom f & f is_continuously_differentiable_up_to_order 1,X;
then
A2: f is_differentiable_on X by Th2;
reconsider g = <>*f as PartFunc of REAL m,REAL 1;
A3: g is_differentiable_on X by A1,A2,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 A3,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 Th4:
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
A1: f is_continuously_differentiable_up_to_order k,X
& g is_continuously_differentiable_up_to_order k,X & X is open;
A2:dom (f+g) = dom f /\ dom g by VALUED_1:def 1;
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
A3: len I <= k & rng I c= Seg m;
A4: f is_partial_differentiable_on X,I by A3,PDIFF_9:def 11,A1;
A5: g is_partial_differentiable_on X,I by A3,A1,PDIFF_9:def 11;
reconsider f0 = f`partial|(X,I) as PartFunc of REAL m,REAL;
reconsider g0 = g`partial|(X,I) as PartFunc of REAL m,REAL;
A6: X = dom f0 by Th1,A3,PDIFF_9:def 11,A1;
A7: X = dom g0 by Th1,A3,A1,PDIFF_9:def 11;
A8:f0 is_continuous_on X by A3,A1;
A9:g0 is_continuous_on X by A3,A1;
f0+g0 is_continuous_on X by A8,A9,A6,A7,PDIFF_9:46;
hence
(f+g)`partial|(X,I) is_continuous_on X by A1,A3,A4,A5,PDIFF_9:75;
end;
hence thesis by A2,A1,PDIFF_9:85,XBOOLE_1:19;
end;
theorem Th5:
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
A1: f is_continuously_differentiable_up_to_order k,X & X is open;
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
A2: len I <= k & rng I c= Seg m;
A3: f is_partial_differentiable_on X,I by A2,PDIFF_9:def 11,A1;
reconsider f0 = f`partial|(X,I) as PartFunc of REAL m,REAL;
X = dom f0 by Th1,A2,PDIFF_9:def 11,A1; then
r(#)f0 is_continuous_on X by A2,A1,PDIFF_9:47;
hence
(r(#)f)`partial|(X,I) is_continuous_on X by A1,A2,A3,PDIFF_9:79;
end;
hence thesis by PDIFF_9:86,A1,VALUED_1:def 5;
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
A1: f is_continuously_differentiable_up_to_order k,X
& g is_continuously_differentiable_up_to_order k,X & X is open;
A2:dom (f-g) = dom f /\ dom g by VALUED_1:12;
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
A3: len I <= k & rng I c= Seg m;
A4: f is_partial_differentiable_on X,I by A3,PDIFF_9:def 11,A1;
A5: g is_partial_differentiable_on X,I by A3,PDIFF_9:def 11,A1;
reconsider f0 = f`partial|(X,I) as PartFunc of REAL m,REAL;
reconsider g0 = g`partial|(X,I) as PartFunc of REAL m,REAL;
A6: X = dom f0 by Th1,A3,PDIFF_9:def 11,A1;
A7: X = dom g0 by Th1,A3,PDIFF_9:def 11,A1;
A8:f0 is_continuous_on X by A1,A3;
A9:g0 is_continuous_on X by A3,A1;
f0-g0 is_continuous_on X by A8,A9,A6,A7,PDIFF_9:46;
hence (f-g)`partial|(X,I) is_continuous_on X by A1,A3,A4,A5,PDIFF_9:77;
end;
hence thesis by A2,A1,PDIFF_9:85,XBOOLE_1:19;
end;
theorem Th7:
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
st f is_partial_differentiable_on Z,G
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;
assume A1: f is_partial_differentiable_on Z,G;
A2:dom G c= dom (G^I) by FINSEQ_1:26;
A3:for i be Nat st i <= len G - 1 holds (G^I)/.(i+1) = G/.(i+1)
proof
let i be Nat;
assume i <= len G - 1;
then
1 <= i+1 & i+1 <= len G by NAT_1:11,XREAL_1:19;
then
A4: i+1 in dom G by FINSEQ_3:25;
then
(G^I)/.(i+1) = (G^I).(i+1) by A2,PARTFUN1:def 6;
then
(G^I)/.(i+1) = G.(i+1) by A4,FINSEQ_1:def 7;
hence (G^I)/.(i+1) = G/.(i+1) by A4,PARTFUN1:def 6;
end;
A5:len (G^I) = len G + len I by FINSEQ_1:22;
A6:for i be Nat st i <= (len I)-1
holds (G^I)/.(len G + (i+1)) = I/.(i+1)
proof
let i be Nat;
assume i <= len I - 1;
then
A7: i+1 <= len I by XREAL_1:19;
then
A8: 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,A5,A7,XREAL_1:7;
hence (G^I)/.(len G + (i+1)) =(G^I).(len G + (i+1)) by PARTFUN1:def 6
.= I.(i+1) by A8,FINSEQ_1:def 7
.= I/.(i+1) by A8,PARTFUN1:def 6;
end;
defpred P0[Nat] means
$1 <= len G - 1 implies (PartDiffSeq(f,Z,G^I)).$1 =(PartDiffSeq(f,Z,G)).$1;
A9:P0[0]
proof
assume 0 <= len G - 1;
(PartDiffSeq(f,Z,G^I)).0 = f|Z by PDIFF_9:def 7;
hence (PartDiffSeq(f,Z,G^I)).0 = (PartDiffSeq(f,Z,G)).0 by PDIFF_9:def 7;
end;
A10:for k be Nat st P0[k] holds P0[k+1]
proof
let k be Nat;
assume
A11: P0[k];
assume
A12: k+1 <= len G - 1;
A13: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 A13,A3,A11,A12,XXREAL_0:2
.= (PartDiffSeq(f,Z,G)).(k+1) by PDIFF_9:def 7;
end;
A14:for n be Nat holds P0[n] from NAT_1:sch 2(A9,A10);
reconsider j= (len G)-1 as Element of NAT by INT_1:5,FINSEQ_1:20;
A15:(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 A14
.= ((PartDiffSeq(f,Z,G)).j)`partial|(Z,G/.(j+1)) by A3
.= (PartDiffSeq(f,Z,G)).(len G) by PDIFF_9:def 7;
defpred P[Nat] means
$1 <= (len I) -1 implies
(PartDiffSeq(g,Z,I)).$1 =(PartDiffSeq(f,Z,(G^I))).(len G + $1);
A16:P[0]
proof
assume 0 <= (len I) -1 ;
(PartDiffSeq(f,Z,(G^I))).(len G + 0)
= (PartDiffSeq(f,Z,G)).(len G) by A15
.= g
.= g|Z by PDIFF_9:72,A1
.= (PartDiffSeq(g,Z,I)).0 by PDIFF_9:def 7;
hence thesis;
end;
A17:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A18: P[k];
set i = (len G) + k;
assume
A19: k+1 <= (len I) -1;
A20: k <= k+1 by NAT_1:11;
(G^I)/.(i+1) = (G^I)/.(len G + (k+1));
then
A21: (G^I)/.(i+1) = I/.(k+1) by A6,A20,A19,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 A20,A19,A18,A21,PDIFF_9:def 7,XXREAL_0:2;
end;
A22:for n be Nat holds P[ n ] from NAT_1:sch 2(A16,A17);
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;
A23:j1= len G + j0 by A5;
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 A22,A23
.= ((PartDiffSeq(g,Z,I)).j0)`partial|(Z,I/.(j0+1)) by A6
.= 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
st f is_partial_differentiable_on Z,G
holds
f `partial|(Z,G^I) is_continuous_on Z
iff f`partial|(Z,G) `partial|(Z,I) is_continuous_on Z by Th7;
theorem Th9:
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 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 Nat,
I be non empty FinSequence of NAT;
assume
A1: f is_continuously_differentiable_up_to_order (i+j),Z
& rng I c= Seg m & len I = j;
then
A2: 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;
A3: f is_partial_differentiable_on Z,I by A2,A1,NAT_1:11;
f is_partial_differentiable_on Z,I by A2,A1,NAT_1:11;
hence Z c= dom (f`partial|(Z,I)) by Th1;
thus f`partial|(Z,I) is_partial_differentiable_up_to_order i,Z
by PDIFF_9:83,A1;
let J be non empty FinSequence of NAT;
assume
A4:len J <= i & rng J c= Seg m;
reconsider G = I^J as non empty FinSequence of NAT;
A5: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 A4,A5,A1,XBOOLE_1:8,XREAL_1:6;
then f`partial|(Z,G) is_continuous_on Z by A1;
hence thesis by A3,Th7;
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 Nat
st f is_continuously_differentiable_up_to_order i,Z & j <= i
holds f is_continuously_differentiable_up_to_order j,Z
by PDIFF_9:84,XXREAL_0:2;
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
A1: Z is open;
defpred P[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);
A2:P[0]
proof
let f,g be PartFunc of REAL m,REAL;
assume
A3: f is_continuously_differentiable_up_to_order 0,Z
& g is_continuously_differentiable_up_to_order 0,Z;
dom (f (#) g) = dom f /\ dom g by VALUED_1:def 4;
hence
f(#)g is_continuously_differentiable_up_to_order 0,Z
by A3,XBOOLE_1:19,FINSEQ_1:20,PDIFF_9:87,A1;
end;
A4:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A5: P[k];
let f,g be PartFunc of REAL m,REAL;
assume
A6: f is_continuously_differentiable_up_to_order k+1,Z
& g is_continuously_differentiable_up_to_order k+1,Z;
then
A7: f is_continuously_differentiable_up_to_order k,Z
& g is_continuously_differentiable_up_to_order k,Z by Th10,NAT_1:11;
dom (f (#) g) = dom f /\ dom g by VALUED_1:def 4;
then
A8: Z c= dom (f(#)g) by A6,XBOOLE_1:19;
now let I be non empty FinSequence of NAT;
assume
A9: len I <= k+1 & rng I c= Seg m;
then
A10: f is_partial_differentiable_on Z,I
& g is_partial_differentiable_on Z,I by PDIFF_9:def 11,A6;
A11: f `partial|(Z,I) is_continuous_on Z
& g `partial|(Z,I) is_continuous_on Z by A9,A6;
A12: 1 <= len I by FINSEQ_1:20;
then
A13: 1 in dom I by FINSEQ_3:25;
then
A14: I/.1 = I.1 by PARTFUN1:def 6;
A15: I.1 in rng I by A13,FUNCT_1:3;
reconsider i = I.1 as Element of NAT by ORDINAL1:def 12;
A16: 1 <= i & i <= m by A15,A9,FINSEQ_1:1;
per cases;
suppose
A17: 1 = len I;
then
A18: I = <*I.1*> by FINSEQ_5:14;
A19: f(#)g is_continuously_differentiable_up_to_order k,Z by A5,A7;
now per cases;
suppose
A20: k = 0;
A21: I = <*i*> by A17,FINSEQ_5:14;
A22: f is_partial_differentiable_on Z,i
& g is_partial_differentiable_on Z,i
by A18,A9,PDIFF_9:def 11,A6;
then
A23: (f(#)g)`partial|(Z,I) = (f(#)g)`partial|(Z,i)
by A1,A16,A21,PDIFF_9:68,82
.=(f`partial|(Z,i))(#)g + f(#)(g`partial|(Z,i))
by A1,A22,A16,PDIFF_9:68
.= f`partial|(Z,I)(#)g + f(#)(g`partial|(Z,i))
by A1,A16,A21,A22,PDIFF_9:82
.= f`partial|(Z,I)(#)g + f(#)(g`partial|(Z,I))
by A1,A16,A21,A22,PDIFF_9:82;
A24: Z c= dom (f`partial|(Z,I)) & Z c= dom (g`partial|(Z,I))
by A9,Th1,PDIFF_9:def 11,A6;
A25: f is_continuous_on Z by A1,Th3,A6,A20;
g is_continuous_on Z by A1,Th3,A6,A20;
then
A26: f`partial|(Z,I)(#)g is_continuous_on Z
by A11,A6,A24,PDIFF_9:48;
A27: f(#)(g`partial|(Z,I)) is_continuous_on Z
by A11,A25,A6,A24,PDIFF_9:48;
dom (f`partial|(Z,I)(#)g) = dom (f`partial|(Z,I)) /\ dom g
by VALUED_1:def 4;
then
A28: Z c= dom (f`partial|(Z,I)(#)g) by A24,A6,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 A24,A6,XBOOLE_1:19;
hence (f(#)g) `partial|(Z,I) is_continuous_on Z
by A23,A26,A27,A28,PDIFF_9:46;
end;
suppose k <> 0;
hence (f(#)g) `partial|(Z,I) is_continuous_on Z
by A19,A9,A17,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 A12,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 A12,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 A9,XREAL_1:20;
then
A29: len J <= k by A12,RFINSEQ:def 1;
A30: I = <*I/.1*>^(I/^1) by FINSEQ_5:29;
then
A31: rng I1 c= rng I & rng J c= rng I by A14,FINSEQ_1:29,30;
then
A32: rng J c= Seg m by A9;
I = I1^J by A14,FINSEQ_5:29;
then
A33: f is_partial_differentiable_on Z,i
& g is_partial_differentiable_on Z,i
by PDIFF_9:80,A10;
then
A34: f(#)g is_partial_differentiable_on Z,i by A1,A16,PDIFF_9:68;
then
A35: (f(#)g)`partial|(Z,I1) = (f(#)g)`partial|(Z,i)
by A1,A16,PDIFF_9:82
.=(f`partial|(Z,i))(#)g + f(#)(g`partial|(Z,i))
by A33,A16,PDIFF_9:68,A1
.= f`partial|(Z,I1)(#)g + f(#)(g`partial|(Z,i))
by A1,A16,A33,PDIFF_9:82
.= f`partial|(Z,I1)(#)g + f(#)(g`partial|(Z,I1))
by A1,A16,A33,PDIFF_9:82;
len I1 =1 & rng I1 c= Seg m by A31,A9,FINSEQ_1:39;
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 Th9,A6;
then
A36: 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 A5,A7;
then
f`partial|(Z,I1)(#)g is_partial_differentiable_on Z,J
& f(#)(g`partial|(Z,I1)) is_partial_differentiable_on Z,J
by A29,A32,PDIFF_9:def 11;
then
A37: (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 A1,A32,PDIFF_9:75;
A38: Z c= dom((f`partial|(Z,I1) (#)g ) `partial|(Z,J))
& Z c= dom (( f(#)(g`partial|(Z,I1)))`partial|(Z,J))
by A36,Th1,A29,A32,PDIFF_9:def 11;
(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 A36,A29,A9,XBOOLE_1:1,A31;
then
(f`partial|(Z,I1) (#)g + f(#)(g`partial|(Z,I1)))`partial|(Z,J)
is_continuous_on Z by A37,A38,PDIFF_9:46;
hence (f(#)g)`partial|(Z,I) is_continuous_on Z
by A30,A14,A34,A35,Th7;
end;
end;
hence f(#)g is_continuously_differentiable_up_to_order k+1,Z
by A8,PDIFF_9:87,A1,A6;
end;
for n be Nat holds P[ n ] from NAT_1:sch 2(A2,A4);
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
A1:X is open & f = X --> d;
let x be Element of REAL m;
assume
A2: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;
A3: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);
A4:0.(REAL-NS 1) = 0*1 by REAL_NS1:def 4
.= 1 |-> (0 qua Real) by EUCLID:def 4
.= <* 0 *> by FINSEQ_2:59;
A5:ZR = REAL m --> <* 0 *> by A4,A3,LOPBAN_1:31;
reconsider Z= X as Subset of REAL-NS m by REAL_NS1:def 4;
A6:Z is open by PDIFF_9:10,A1;
A7:dom f = X by A1,FUNCT_2:def 1;
then
A8: dom (<>*f) = X by PDIFF_9:3;
A9: Z = dom g by A7,PDIFF_9:3;
now let x be object;
assume x in dom(<>*f);
then
A10: x in X by A7,PDIFF_9:3;
then reconsider x1=x as Element of REAL m;
(<>*f).x = <* f.x1 *> by A7,A10,PDIFF_9:6;
hence (<>*f).x = <* d *> by A1,A10,FUNCOP_1:7;
end;
then
A11: <>*f = X --> <* d *> by A8,FUNCOP_1:11;
A12:
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,A6,A9;
then
A14:g is_differentiable_in x1 by A2,NDIFF_1:31,A6;
A15:ZR = (g`|Z)/.x1 by A12,A2,NDIFF_1:33,A6,A9
.= diff(g,x1) by A2,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 A5,A15,A16,PDIFF_6:3;
A18:dom (proj(1,1)*diff(<>*f,x) ) = REAL m by FUNCT_2:def 1;
now let y be object;
assume
A19: 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 A19,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,A18;
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
A1: X is open & f = X --> d;
let x0 be Element of REAL m,r be Real;
assume
A2: x0 in X & 0 < r;
take s=1 qua Real;
thus 0 < s;
let x1 be Element of REAL m;
assume
A3: x1 in X & |. x1- x0 .| < s;
let v be Element of REAL m;
A4:diff(f,x1).v = (REAL m --> 0).v by A1,Th12,A3
.= (0 qua Real) by FUNCOP_1:7;
diff(f,x0).v = (REAL m --> 0).v by A1,Th12,A2
.= (0 qua Real) by FUNCOP_1:7;
hence |. diff(f,x1).v - diff(f,x0).v.| <= r * |.v.| by A4,A2,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
A1: X is open & f = X --> d;
A2:X = dom f by A1,FUNCT_2:def 1;
for x be Element of REAL m st x in X holds f is_differentiable_in x
by Th12,A1;
hence f is_differentiable_on X by A2,A1,PDIFF_9:54;
thus dom (f`|X) = X by PDIFF_9:def 4,A2;
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
A3: x in X;
thus (f`|X)/.x = diff(f,x) by A2,PDIFF_9:def 4,A3
.= REAL m --> 0 by A3,Th12,A1;
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
A1: X is open;
assume
A2: f = X --> d;
assume
A3: 1 <= i & i <= m;
A4:dom f = X by A2,FUNCT_2:def 1;
A5:f is_differentiable_on X by Th14,A2,A1;
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 A2,Th13,A1;
hence thesis by A3,A4,A1,A5,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
A1: X is open & f = X --> d & 1 <= i & i <= m;
A2:f is_partial_differentiable_on X,i by A1,Th15;
A3:dom (f`partial|(X,i)) = X by A2,PDIFF_9:def 6;
now let x be object;
assume
A4: x in dom (f`partial|(X,i));
then
reconsider x1=x as Element of REAL m;
A5: f is_differentiable_in x1 & diff(f,x1) = REAL m --> 0 by Th12,A1,A3,A4;
A6: (reproj(i,0*m).1) in REAL m by XREAL_0:def 1,FUNCT_2:5;
A7: partdiff(f,x1,i) = diff(f,x1).(reproj(i,0*m).1) by PDIFF_7:23,A5,A1
.= 0 by A6,FUNCOP_1:7,A5;
thus (f`partial|(X,i)).x =(f`partial|(X,i))/.x1 by A4,PARTFUN1:def 6
.= 0 by A7,A2,A4,A3,PDIFF_9:def 6;
end;
hence thesis by A3,FUNCOP_1:11;
end;
Lm1:
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
A1:rng I c= Seg m;
assume
A2: i <= (len I)-1;
A3: (0 qua Real) + 1 <= i + 1 by XREAL_1:6;
i + 1 <= len I -1 + 1 by A2,XREAL_1:6;
then i+1 in Seg (len I) by A3;
then
A4: 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 A4,PARTFUN1:def 6;
hence 1 <= I/.(i+1) & I/.(i+1) <= m by FINSEQ_1:1,A1;
end;
Lm2:
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
A1: rng I c= Seg m;
assume 1 <= i & i <= len I;
then i in Seg (len I);
then
A2: 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 A2,PARTFUN1:def 6;
hence 1 <= I/.i & I/.i <= m by FINSEQ_1:1,A1;
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
A1:X is open & f = X --> d & rng I c= Seg m;
thus
A2: (PartDiffSeq(f,X,I)).0 = (X --> d) | X by A1,PDIFF_9:def 7
.= (X /\ X)--> d by FUNCOP_1:12
.= X --> d;
defpred P[Nat] means
1<=$1 & $1 <= (len I) implies (PartDiffSeq(f,X,I)).$1 = X --> 0;
A3:P[0];
A4:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A5: P[i];
assume
A6: 1<=i+1 & i+1 <= len I;
A7: i <= i + 1 by NAT_1:12;
per cases;
suppose A8: i=0;
A9: 1 <= I/.(i+1) & I/.(i+1) <= m by Lm2,A1,A6;
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,A1,A2,Th16;
end;
suppose A10: i <> 0;
A11: 1 <= I/.(i+1) & I/.(i+1) <= m by Lm2,A1,A6;
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 A10,A11,A1,Th16,A7,A5,NAT_1:14,XXREAL_0:2,A6;
end;
end;
for i be Nat holds P[i] from NAT_1:sch 2(A3,A4);
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
A1: 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
A2: i <= (len I)-1;
(len I)-1 <= len I - (0 qua Real) by XREAL_1:10;
then
A3: i <= (len I) by A2,XXREAL_0:2;
per cases;
suppose i=0;
then
A4: (PartDiffSeq(f,X,I)).i = X --> d by A1,Th17;
1 <= I/.(i+1) & I/.(i+1) <= m by Lm1,A1,A2;
hence thesis by A4,A1,Th15;
end;
suppose i <> 0;
then
1 <= i by NAT_1:14;
then
A5: (PartDiffSeq(f,X,I)).i = X --> 0 by A1,A3,Th17;
1 <= I/.(i+1) & I/.(i+1) <= m by Lm1,A1,A2;
hence thesis by A5,A1,Th15;
end;
end;
hence f is_partial_differentiable_on X,I;
reconsider k=(len I)-1 as Element of NAT by INT_1:5,FINSEQ_1:20;
A6: f`partial|(X,I) = ((PartDiffSeq(f,X,I)).k)`partial|(X,I/.(k+1))
by PDIFF_9:def 7;
A7: (len I) - 1 <= (len I) - (0 qua Real) by XREAL_1:10;
per cases;
suppose k = 0;
then
A8: (PartDiffSeq(f,X,I)).k = X --> d by A1,Th17;
1 <= I/.(k+1) & I/.(k+1) <= m by A1,Lm1;
hence f`partial|(X,I) is_continuous_on X by A1,A6,A8,Th15;
end;
suppose k <> 0;
then
1 <= k by NAT_1:14;
then
A9: (PartDiffSeq(f,X,I)).k = X --> 0 by A1,A7,Th17;
1 <= I/.(k+1) & I/.(k+1) <= m by A1,Lm1;
hence f`partial|(X,I) is_continuous_on X by A1,A6,A9,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
A1: X is open & f = X --> d; then
f is_partial_differentiable_up_to_order k,X by Th18;
hence thesis by A1,Th18,FUNCT_2:def 1;
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 object;
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;
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 object;
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;
A5: 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,Th4;
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 object 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,A5;
end;
then
A9: W is add-closed by IDEAL_1:def 1;
A10: for v be Element of V st v in W holds -v in W
proof
let v be Element of V such that
A11: v in W;
consider v1 be PartFunc of REAL m,REAL such that
A12: v1=v & v1 is_continuously_differentiable_up_to_order k,X
& dom v1 = X by A11;
A13:dom (-v1) = X by VALUED_1:def 5,A12;
A14: -v1 is_continuously_differentiable_up_to_order k,X by A12,Th5;
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 object;
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 A12;
end;
then -v=-v1 by A12,A16,VALUED_1:9;
hence -v in W by A14,A13;
end;
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
A17: u in W;
consider u1 be PartFunc of REAL m, REAL such that
A18: u1=u & u1 is_continuously_differentiable_up_to_order k,X & dom u1 = X
by A17;
A19:dom (a(#)u1) = X by A18,VALUED_1:def 5;
A20:a(#)u1 is_continuously_differentiable_up_to_order k,X by A18, Th5;
reconsider h = a*u as Element of Funcs(X,REAL);
A21:ex f being Function st h = f & dom f = X & rng f c= REAL by FUNCT_2:def 2;
for x be object st x in dom h holds h.x = a*(u1.x) by A18,FUNCSDOM:4;
then a*u=a(#)u1 by A18,A21,VALUED_1:def 5;
hence a*u in W by A20,A19;
end;
hence Ck_Functions(k,X) is additively-linearly-closed
by A9,A10,C0SP1:def 1,def 10;
A22: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
A23: v in W & u in W;
consider v1 be PartFunc of REAL m,REAL such that
A24: v1=v & v1 is_continuously_differentiable_up_to_order k,X
& dom v1 = X by A23;
consider u1 be PartFunc of REAL m,REAL such that
A25: u1=u & u1 is_continuously_differentiable_up_to_order k,X
& dom u1 = X by A23;
A26:dom (v1(#)u1) = dom v1 /\ dom u1 by VALUED_1:def 4
.= X by A24,A25;
A27:v1(#)u1 is_continuously_differentiable_up_to_order k,X by A24,A25,Th11;
reconsider h = v*u as Element of Funcs(X,REAL);
A28:ex f being Function st h = f & dom f = X & rng f c= REAL by FUNCT_2:def 2;
A29: dom v1 /\ dom u1 = X /\ X by A25,A24;
for x be object st x in dom h holds h.x = v1.x *u1.x
by A24,A25,FUNCSDOM:2;
then v*u=v1(#)u1 by A29,A28,VALUED_1:def 4;
hence v*u in W by A27,A26;
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;
A30: 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 A30;
hence thesis by A22,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;
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
A2: H = F+G;
let x be Element of X;
h1=f1+g1 by A2,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
A2: G = a*F;
let x be Element of X;
g1=a*f1 by A2,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
A2: H = F*G;
let x be Element of X;
h1 = f1*g1 by A2,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;