NDIFF14: Higher Order Partial Differentiable Functions

:: Higher Order Partial Differentiable Functions
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received December 2, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users

theorem :: NDIFF14:1

for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S holds
( f | Z is_differentiable_on Z iff f is_differentiable_on Z )

proof end;

theorem Th2: :: NDIFF14:2

for L, M being RealNormSpace
for s being Point of L
for w being FinSequence of M
for X being FinSequence of (R_NormSpace_of_BoundedLinearOperators (L,M)) st dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) holds
Sum w = (Sum X) . s

proof end;

registration

let X be RealNormSpace;

cluster non empty open for Element of bool the carrier of X;

correctness

proof end;

end;

theorem Th3: :: NDIFF14:3

for X, Y being RealNormSpace
for Z being non empty Subset of X
for v, u being VECTOR of (RealVectSpace (Z,Y))
for f, g being PartFunc of X,Y
for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )

proof end;

definition

let X, Y be RealNormSpace;
let Z be non empty open Subset of X;
let n be Nat;

func Continuously_differentiable_Functions (Z,Y,n) -> Subset of (RealVectSpace (Z,Y)) equals :: NDIFF14:def 1
{ f where f is PartFunc of X,Y : ( dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) } ;

correctness

proof end;

end;

:: deftheorem defines Continuously_differentiable_Functions NDIFF14:def 1 :

theorem :: NDIFF14:4

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being Nat
for f being PartFunc of X,Y holds
( f in Continuously_differentiable_Functions (Z,Y,n) iff ( dom f = Z & f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z ) )

proof end;

registration

let X, Y be RealNormSpace;
let Z be non empty open Subset of X;
let n be Nat;

cluster Continuously_differentiable_Functions (Z,Y,n) -> functional non empty ;

coherence

proof end;

end;

theorem Th5: :: NDIFF14:5

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat holds Continuously_differentiable_Functions (Z,Y,n) is linearly-closed

proof end;

theorem :: NDIFF14:6

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat holds RLSStruct(# (Continuously_differentiable_Functions (Z,Y,n)),(Zero_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))),(Add_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))),(Mult_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))) #) is Subspace of RealVectSpace (Z,Y) by Th5, RSSPACE:11;

registration

let X, Y be RealNormSpace;
let Z be non empty open Subset of X;
let n be non empty Nat;

cluster RLSStruct(# (Continuously_differentiable_Functions (Z,Y,n)),(Zero_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))),(Add_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))),(Mult_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence by Th5, RSSPACE:11;

end;

definition

let X, Y be RealNormSpace;
let Z be non empty open Subset of X;
let n be non empty Nat;

func RVectSp_Continuously_differentiable_Funcs (Z,Y,n) -> strict RealLinearSpace equals :: NDIFF14:def 2
RLSStruct(# (Continuously_differentiable_Functions (Z,Y,n)),(Zero_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))),(Add_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))),(Mult_ ((Continuously_differentiable_Functions (Z,Y,n)),(RealVectSpace (Z,Y)))) #);

coherence ;

end;

:: deftheorem defines RVectSp_Continuously_differentiable_Funcs NDIFF14:def 2 :

registration

let X, Y be RealNormSpace;
let Z be non empty open Subset of X;
let n be non empty Nat;

cluster RVectSp_Continuously_differentiable_Funcs (Z,Y,n) -> strict constituted-Functions ;

coherence ;

end;

theorem Th7: :: NDIFF14:7

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat
for v, u being VECTOR of (RVectSp_Continuously_differentiable_Funcs (Z,Y,n))
for f, g being PartFunc of X,Y
for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )

proof end;

definition

let X, Y be RealNormSpace;
let Z be non empty open Subset of X;
let n be non empty Nat;
let f be Element of (RVectSp_Continuously_differentiable_Funcs (Z,Y,n));
let v be Element of Z;
:: original: .
redefine func f . v -> VECTOR of Y;
coherence

proof end;

end;

theorem :: NDIFF14:8

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat
for f, g, h being VECTOR of (RVectSp_Continuously_differentiable_Funcs (Z,Y,n)) holds
( h = f + g iff for x being Element of Z holds h . x = (f . x) + (g . x) )

proof end;

theorem :: NDIFF14:9

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat
for f, h being VECTOR of (RVectSp_Continuously_differentiable_Funcs (Z,Y,n))
for a being Real holds
( h = a * f iff for x being Element of Z holds h . x = a * (f . x) )

proof end;

theorem Th10: :: NDIFF14:10

for X, Y being RealNormSpace
for Z being non empty open Subset of X
for n being non empty Nat holds 0. (RVectSp_Continuously_differentiable_Funcs (Z,Y,n)) = Z --> (0. Y)

proof end;

theorem Th11: :: NDIFF14:11

for G0, F being RealNormSpace
for X being non empty open Subset of G0
for n being non empty Nat
for x being Point of G0 st x in X holds
for W0 being FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n))
for Wx being FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)) st dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) holds
Sum Wx = (Sum W0) . x

proof end;

definition

let S be RealNormSpace-Sequence;
let T be RealNormSpace;
let I be non empty FinSequence of dom S;

func Partdiff_SP (S,T,I) -> RealNormSpace-Sequence means :Def3: :: NDIFF14:def 3
( dom it = dom I & it . 1 = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . 1),(dom S)))),T) & ( for i being Nat st 1 <= i & i < len I holds
it . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . (i + 1)),(dom S)))),(modetrans (it . i))) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Partdiff_SP NDIFF14:def 3 :

definition

let S be RealNormSpace-Sequence;
let T be RealNormSpace;
let I be non empty FinSequence of dom S;
let i be Nat;
assume A1: ( 1 <= i & i <= len I ) ;

func Partdiff_SP (S,T,I,i) -> RealNormSpace equals :Def4: :: NDIFF14:def 4
(Partdiff_SP (S,T,I)) . i;

correctness

proof end;

end;

:: deftheorem Def4 defines Partdiff_SP NDIFF14:def 4 :

theorem Th12: :: NDIFF14:12

for S being RealNormSpace-Sequence
for T being RealNormSpace
for I being non empty FinSequence of dom S holds
( Partdiff_SP (S,T,I,1) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . 1),(dom S)))),T) & ( for i being Nat st 1 <= i & i < len I holds
Partdiff_SP (S,T,I,(i + 1)) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . (i + 1)),(dom S)))),(Partdiff_SP (S,T,I,i))) ) )

proof end;

definition

let S be RealNormSpace-Sequence;
let T be RealNormSpace;
let I be non empty FinSequence of dom S;

func PartdiffSP (S,T,I) -> RealNormSpace equals :: NDIFF14:def 5
(Partdiff_SP (S,T,I)) . (len I);

correctness

proof end;

end;

:: deftheorem defines PartdiffSP NDIFF14:def 5 :

definition

let S be RealNormSpace-Sequence;
let T be RealNormSpace;
let Z be Subset of (product S);
let I be non empty FinSequence of dom S;
let f be PartFunc of (product S),T;

func PartDiffSeq (f,Z,I) -> FinSequence means :Def6: :: NDIFF14:def 6
( dom it = dom I & it . 1 = f `partial| (Z,(I . 1)) & ( for i being Nat st 1 <= i & i < len I holds
ex g being PartFunc of (product S),(Partdiff_SP (S,T,I,i)) st
( it . i = g & it . (i + 1) = g `partial| (Z,(I . (i + 1))) ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines PartDiffSeq NDIFF14:def 6 :

definition

let S be RealNormSpace-Sequence;
let T be RealNormSpace;
let Z be Subset of (product S);
let I be non empty FinSequence of dom S;
let f be PartFunc of (product S),T;
let i be Nat;
assume A1: ( 1 <= i & i <= len I ) ;

func PartDiffSeq (f,Z,I,i) -> PartFunc of (product S),(Partdiff_SP (S,T,I,i)) equals :Def7: :: NDIFF14:def 7
(PartDiffSeq (f,Z,I)) . i;

correctness

proof end;

end;

:: deftheorem Def7 defines PartDiffSeq NDIFF14:def 7 :

theorem Th13: :: NDIFF14:13

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( PartDiffSeq (f,Z,I,1) = f `partial| (Z,(I . 1)) & ( for i being Nat st 1 <= i & i < len I holds
PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I,i)) `partial| (Z,(I . (i + 1))) ) )

proof end;

definition

let S be RealNormSpace-Sequence;
let T be RealNormSpace;
let Z be Subset of (product S);
let I be non empty FinSequence of dom S;
let f be PartFunc of (product S),T;

pred f is_partial_differentiable_on Z,I means :: NDIFF14:def 8
( f is_partial_differentiable_on Z,I . 1 & ( for i being Nat st 1 <= i & i < len I holds
PartDiffSeq (f,Z,I,i) is_partial_differentiable_on Z,I . (i + 1) ) );

end;

:: deftheorem defines is_partial_differentiable_on NDIFF14:def 8 :

definition

let S be RealNormSpace-Sequence;
let T be RealNormSpace;
let Z be Subset of (product S);
let I be non empty FinSequence of dom S;
let f be PartFunc of (product S),T;

func f `partial| (Z,I) -> PartFunc of (product S),(Partdiff_SP (S,T,I,(len I))) equals :: NDIFF14:def 9
PartDiffSeq (f,Z,I,(len I));

coherence ;

end;

:: deftheorem defines `partial| NDIFF14:def 9 :

theorem :: NDIFF14:14

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for k being Element of dom S
for f being PartFunc of (product S),T holds
( f is_partial_differentiable_on Z,<*k*> iff f is_partial_differentiable_on Z,k ) by FINSEQ_1:40;

theorem Th15: :: NDIFF14:15

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for k being Element of dom S
for f being PartFunc of (product S),T holds f `partial| (Z,<*k*>) = f `partial| (Z,k)

proof end;

theorem Th16: :: NDIFF14:16

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I, G being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( ( for n being Nat st 1 <= n & n <= len G holds
( Partdiff_SP (S,T,(G ^ I),n) = Partdiff_SP (S,T,G,n) & PartDiffSeq (f,Z,(G ^ I),n) = PartDiffSeq (f,Z,G,n) ) ) & ( for n being Nat st 1 <= n & n <= len I holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,n) = Partdiff_SP (S,T,(G ^ I),((len G) + n)) & PartDiffSeq ((f `partial| (Z,G)),Z,I,n) = PartDiffSeq (f,Z,(G ^ I),((len G) + n)) ) ) )

proof end;

theorem Th17: :: NDIFF14:17

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I, G being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( Partdiff_SP (S,T,(G ^ I),(len G)) = Partdiff_SP (S,T,G,(len G)) & PartDiffSeq (f,Z,(G ^ I),(len G)) = PartDiffSeq (f,Z,G,(len G)) & Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(len I)) = Partdiff_SP (S,T,(G ^ I),((len G) + (len I))) & PartDiffSeq ((f `partial| (Z,G)),Z,I,(len I)) = PartDiffSeq (f,Z,(G ^ I),((len G) + (len I))) )

proof end;

theorem Th18: :: NDIFF14:18

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I, G being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( (f `partial| (Z,G)) `partial| (Z,I) = f `partial| (Z,(G ^ I)) & Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),I,(len I)) = Partdiff_SP (S,T,(G ^ I),(len (G ^ I))) )

proof end;

theorem :: NDIFF14:19

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for G being non empty FinSequence of dom S
for s being Element of dom S
for f being PartFunc of (product S),T holds
( Partdiff_SP (S,(Partdiff_SP (S,T,G,(len G))),<*s*>,1) = Partdiff_SP (S,T,(G ^ <*s*>),((len G) + 1)) & (f `partial| (Z,G)) `partial| (Z,s) = PartDiffSeq (f,Z,(G ^ <*s*>),((len G) + 1)) )

proof end;

theorem Th20: :: NDIFF14:20

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I, G being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( f is_partial_differentiable_on Z,I ^ G iff ( f is_partial_differentiable_on Z,I & f `partial| (Z,I) is_partial_differentiable_on Z,G ) )

proof end;

theorem Th21: :: NDIFF14:21

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for f, g being PartFunc of (product S),T
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f + g is_partial_differentiable_on Z,i & (f + g) `partial| (Z,i) = (f `partial| (Z,i)) + (g `partial| (Z,i)) )

proof end;

theorem Th22: :: NDIFF14:22

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for f being PartFunc of (product S),T
for i being set st Z is open & f is_differentiable_on Z holds
( f is_partial_differentiable_on Z,i & ( for x being Point of (product S) st x in Z holds
(f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S)))) ) )

proof end;

theorem Th23: :: NDIFF14:23

for S being RealNormSpace-Sequence
for s being set holds reproj ((In (s,(dom S))),(0. (product S))) is Lipschitzian LinearOperator of (S . (In (s,(dom S)))),(product S)

proof end;

theorem Th24: :: NDIFF14:24

for S being RealNormSpace-Sequence
for s being set holds
( proj (In (s,(dom S))) is Lipschitzian LinearOperator of (product S),(S . (In (s,(dom S)))) & ex LP being Point of (R_NormSpace_of_BoundedLinearOperators ((product S),(S . (In (s,(dom S)))))) st
( LP = proj (In (s,(dom S))) & ||.LP.|| <= 1 ) )

proof end;

theorem Th25: :: NDIFF14:25

for S being RealNormSpace-Sequence
for G being RealNormSpace
for Z being non empty Subset of (product S)
for f being PartFunc of (product S),G
for s being set
for i being Nat st f is_differentiable_on i + 1,Z holds
f `partial| (Z,s) is_differentiable_on i,Z

proof end;

theorem Th26: :: NDIFF14:26

proof end;

theorem Th27: :: NDIFF14:27

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for f being PartFunc of (product S),T
for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( a (#) f is_partial_differentiable_on Z,i & (a (#) f) `partial| (Z,i) = a (#) (f `partial| (Z,i)) )

proof end;

theorem Th28: :: NDIFF14:28

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for f being PartFunc of (product S),T
for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( - f is_partial_differentiable_on Z,i & (- f) `partial| (Z,i) = - (f `partial| (Z,i)) )

proof end;

theorem :: NDIFF14:29

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for f, g being PartFunc of (product S),T
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f - g is_partial_differentiable_on Z,i & (f - g) `partial| (Z,i) = (f `partial| (Z,i)) - (g `partial| (Z,i)) )

proof end;

theorem Th30: :: NDIFF14:30

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f + g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) ) )

proof end;

theorem Th31: :: NDIFF14:31

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f being PartFunc of (product S),T
for a being Real st Z is open & f is_partial_differentiable_on Z,I holds
( a (#) f is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((a (#) f),Z,I,i) = a (#) (PartDiffSeq (f,Z,I,i)) ) )

proof end;

theorem Th32: :: NDIFF14:32

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I holds
( - f is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i)) ) )

proof end;

theorem :: NDIFF14:33

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f - g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i)) ) )

proof end;

definition

let S be RealNormSpace-Sequence;
let T be RealNormSpace;
let Z be Subset of (product S);
let f be PartFunc of (product S),T;
let k be Nat;

pred f is_partial_differentiable_up_to_order k,Z means :: NDIFF14:def 10
for I being non empty FinSequence of dom S st len I <= k holds
f is_partial_differentiable_on Z,I;

end;

:: deftheorem defines is_partial_differentiable_up_to_order NDIFF14:def 10 :

theorem :: NDIFF14:34

for G being RealNormSpace-Sequence
for X being non empty Subset of (product G) st X is open holds
for n being Nat
for F being RealNormSpace
for f being PartFunc of (product G),F st f is_differentiable_on n,X holds
for I being non empty FinSequence of dom G st len I <= n holds
f is_partial_differentiable_on X,I

proof end;

theorem Th35: :: NDIFF14:35

for G being RealNormSpace-Sequence
for X being non empty Subset of (product G) st X is open holds
for n being Nat
for F being RealNormSpace
for f being PartFunc of (product G),F st f is_differentiable_on n,X & diff (f,n,X) is_continuous_on X holds
for I being non empty FinSequence of dom G st len I <= n holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )

proof end;

theorem :: NDIFF14:36

for G being RealNormSpace-Sequence
for X being non empty open Subset of (product G)
for F being RealNormSpace
for f being PartFunc of (product G),F
for n being Nat st 1 <= n holds
( ( f is_differentiable_on n,X & diff (f,n,X) is_continuous_on X ) iff for I being non empty FinSequence of dom G st len I <= n holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X ) )

proof end;