:: The $C^k$ Space
:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received November 9, 2012
:: Copyright (c) 2012-2025 Association of Mizar Users


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 :: CKSPACE1:def 1
( Z c= dom f & f is_partial_differentiable_up_to_order k,Z & ( for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds
f `partial| (Z,I) is_continuous_on Z ) );
end;

:: deftheorem defines is_continuously_differentiable_up_to_order CKSPACE1:def 1 :
for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for k being Nat
for Z being set holds
( f is_continuously_differentiable_up_to_order k,Z iff ( Z c= dom f & f is_partial_differentiable_up_to_order k,Z & ( for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds
f `partial| (Z,I) is_continuous_on Z ) ) );

theorem Th1: :: CKSPACE1:1
for m being non zero Element of NAT
for Z being set
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_on Z,I holds
dom (f `partial| (Z,I)) = Z
proof end;

theorem Th2: :: CKSPACE1:2
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty Subset of (REAL m)
for f being 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 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
proof end;

theorem Th3: :: CKSPACE1:3
for m being non zero Element of NAT
for X being non empty Subset of (REAL m)
for f being 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 end;

theorem Th4: :: CKSPACE1:4
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty Subset of (REAL m)
for f, g being 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 end;

theorem Th5: :: CKSPACE1:5
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty Subset of (REAL m)
for r being Real
for f being 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 end;

theorem :: CKSPACE1:6
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty Subset of (REAL m)
for f, g being 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 end;

theorem Th7: :: CKSPACE1:7
for m being non zero Element of NAT
for Z being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for I, G being 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 end;

theorem :: CKSPACE1:8
for m being non zero Element of NAT
for Z being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for I, G being 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: :: CKSPACE1:9
for m being non zero Element of NAT
for Z being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for i, j being Nat
for I being 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 end;

theorem Th10: :: CKSPACE1:10
for m being non zero Element of NAT
for Z being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for i, j being 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: :: CKSPACE1:11
for m being non zero Element of NAT
for Z being non empty Subset of (REAL m) st Z is open holds
for k being Element of NAT
for f, g being 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 end;

theorem Th12: :: CKSPACE1:12
for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d holds
for x being Element of REAL m st x in X holds
( f is_differentiable_in x & diff (f,x) = (REAL m) --> 0 )
proof end;

theorem Th13: :: CKSPACE1:13
for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d holds
for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) )
proof end;

theorem Th14: :: CKSPACE1:14
for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d holds
( f is_differentiable_on X & dom (f `| X) = X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0 ) )
proof end;

theorem Th15: :: CKSPACE1:15
for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real
for i being 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 end;

theorem Th16: :: CKSPACE1:16
for m being non zero Element of NAT
for i being Element of NAT
for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d & 1 <= i & i <= m holds
f `partial| (X,i) = X --> 0
proof end;

Lm1: for m being non zero Element of NAT
for I being non empty FinSequence of NAT
for i being Element of NAT st rng I c= Seg m & i <= (len I) - 1 holds
( 1 <= I /. (i + 1) & I /. (i + 1) <= m )
proof end;

Lm2: for m being non zero Element of NAT
for I being non empty FinSequence of NAT
for i being Element of NAT st rng I c= Seg m & 1 <= i & i <= len I holds
( 1 <= I /. i & I /. i <= m )
proof end;

theorem Th17: :: CKSPACE1:17
for m being non zero Element of NAT
for I being non empty FinSequence of NAT
for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for d being Real st X is open & f = X --> d & rng I c= Seg m holds
( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds
(PartDiffSeq (f,X,I)) . i = X --> 0 ) )
proof end;

theorem Th18: :: CKSPACE1:18
for m being non zero Element of NAT
for I being non empty FinSequence of NAT
for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for d being 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 end;

theorem Th19: :: CKSPACE1:19
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for d being Real st X is open & f = X --> d holds
f is_continuously_differentiable_up_to_order k,X
proof end;

registration
let m be non zero Element of NAT ;
cluster non empty functional FinSequence-membered open for Element of K16((REAL m));
correctness
existence
ex b1 being non empty Subset of (REAL m) st b1 is open ;
proof end;
end;

definition
let m be non zero Element of NAT ;
let k be Element of NAT ;
let X be non empty open Subset of (REAL m);
func Ck_Functions (k,X) -> non empty Subset of (RAlgebra X) equals :: CKSPACE1:def 2
 { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } ;
correctness
coherence
{ f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } is non empty Subset of (RAlgebra X);
proof end;
end;

:: deftheorem defines Ck_Functions CKSPACE1:def 2 :
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m) holds Ck_Functions (k,X) = { f where f is PartFunc of (REAL m),REAL : ( f is_continuously_differentiable_up_to_order k,X & dom f = X ) } ;

registration
let m be non zero Element of NAT ;
let k be Element of NAT ;
let X be non empty open Subset of (REAL m);
cluster Ck_Functions (k,X) -> non empty multiplicatively-closed additively-linearly-closed ;
coherence
( Ck_Functions (k,X) is additively-linearly-closed & Ck_Functions (k,X) is multiplicatively-closed )
proof end;
end;

definition
let m be non zero Element of NAT ;
let k be Element of NAT ;
let X be non empty open Subset of (REAL m);
func R_Algebra_of_Ck_Functions (k,X) -> Subalgebra of RAlgebra X equals :: CKSPACE1:def 3
 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
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))) #) is Subalgebra of RAlgebra X by C0SP1:6;
end;

:: deftheorem defines R_Algebra_of_Ck_Functions CKSPACE1:def 3 :
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m) holds R_Algebra_of_Ck_Functions (k,X) = 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))) #);

registration
let m be non zero Element of NAT ;
let k be Element of NAT ;
let X be non empty open Subset of (REAL m);
cluster R_Algebra_of_Ck_Functions (k,X) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital right-distributive right_unital associative commutative vector-associative ;
coherence
( R_Algebra_of_Ck_Functions (k,X) is Abelian & R_Algebra_of_Ck_Functions (k,X) is add-associative & R_Algebra_of_Ck_Functions (k,X) is right_zeroed & R_Algebra_of_Ck_Functions (k,X) is right_complementable & R_Algebra_of_Ck_Functions (k,X) is vector-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-associative & R_Algebra_of_Ck_Functions (k,X) is scalar-unital & R_Algebra_of_Ck_Functions (k,X) is commutative & R_Algebra_of_Ck_Functions (k,X) is associative & R_Algebra_of_Ck_Functions (k,X) is right_unital & R_Algebra_of_Ck_Functions (k,X) is right-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-associative & R_Algebra_of_Ck_Functions (k,X) is vector-associative )
proof end;
end;

theorem :: CKSPACE1:20
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m)
for F, G, H being VECTOR of (R_Algebra_of_Ck_Functions (k,X))
for f, g, h being PartFunc of (REAL m),REAL st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
proof end;

theorem :: CKSPACE1:21
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m)
for F, G, H being VECTOR of (R_Algebra_of_Ck_Functions (k,X))
for f, g, h being PartFunc of (REAL m),REAL
for a being Real st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proof end;

theorem :: CKSPACE1:22
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m)
for F, G, H being VECTOR of (R_Algebra_of_Ck_Functions (k,X))
for f, g, h being PartFunc of (REAL m),REAL st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
proof end;

theorem :: CKSPACE1:23
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m) holds 0. (R_Algebra_of_Ck_Functions (k,X)) = X --> 0
proof end;

theorem :: CKSPACE1:24
for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m) holds 1_ (R_Algebra_of_Ck_Functions (k,X)) = X --> 1
proof end;