Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)

Regular Paper

高階微分の形式化について
On The Formalizations for Higher Derivatives of
Vector Valued Functions
師玉 康成 1 中正 和久 2,*
Yasunari Shidama1 Kazuhisa Nakasho2,*
1 長野県軽井沢町
1 Karuizawa, Nagano, Japan
2 山口大学大学院創成科学研究科, 山口県宇部市常盤台 2-16-1
2 Graduated School of Science and Technology for Innovation, Yamaguchi University,
2-16-1 Tokiwa-dai, Ube, Japan* nakasho@yamaguchi-u.ac.jp
Proof checked by Mizar Version: 8.1.11 and MML Version: 5.66.1402
Received: November 10, 2021. Accepted: May 16, 2022.

Abstract
In this paper, we formalized the deﬁnitions of higher-order derivatives and partial
derivatives of vector-valued functions on normed spaces using an inductive construction
method and proved some fundamental theorems.

1

はじめに
本稿ではノルム空間上の関数の高階微分について筆者らの形式化の現状について報告する．一変数実数値関数の高階導関数は一般的な微積分の教科書で比較的詳しく解説されている．Mizar Mathematical Library (以下 MML) では以下のように形式化している.

Listing 1. LinearOperator
deﬁnition
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
func diﬀ(f,Z) −> Functional Sequence of REAL,REAL means:: TAYLOR 1:def 5
it.0 = f|Z & for i be Nat holds it.(i+1) = (it.i) ‘| Z;
end;
deﬁnition

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

1/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)

let f be PartFunc of REAL,REAL;
let n be Nat;let Z be Subset of REAL;
pred f is diﬀerentiable on n,Z means:: TAYLOR 1:def 6
for i be Nat st i <= n−1 holds diﬀ(f,Z).i is diﬀerentiable on Z;
end;
theorem :: TAYLOR 1:33
for n be Nat,f be PartFunc of REAL,REAL,x0,r be Real st].x0−r,x0+r.[ c= dom f & 0 < r & f is diﬀerentiable on n+1,].x0−r,x0+r.[
for x be Real st x in ].x0−r,x0+r.[
ex s be Real st 0 < s & s < 1 & f.x=
Partial Sums(Taylor(f,].x0−r,x0+r.[,x0,x)).n + (diﬀ(f,].x0−r,x0+r.[).(n+1)).(x0+s∗(x−x0)) ∗ (x−x0) |ˆ (n+1) / ((n+1)!);

多変数実数値関数も二階微分までならベクトルや行列を用いて見通しの良い表現ができる．ところが，三階微分以上になると一変数関数の場合と異なり見通しが悪くなる．例
えば教科書 [1] では以下のように微分可能性を各変数についての偏微分で記述している．

“f を Rn の開集合 U で定義された関数とする.

(中略)

正整数 r に対し,f の r 次までの各種の偏微分係数∂ α1 +α2 +···+αn f, αi ≥ 0, α1 + α2 + · · · + αn ≤ r(∂x1 )α1 · · · (∂xn )αn(1)

が全て U で存在し，しかもこれらが U において連続であるとき，f を U 上の r 回連続微分可能な関数または C r 級関数とよぶ．”
さらに Rn から Rm への写像 f については値域のベクトルを成分に分け各成分 i の値を表す関数

(x1 , x2 , · · · xn ) ∈ Rn 7→ f i (x1 , x2 , · · · xn ) ∈ R
が全て U 上で r 回連続微分可能なとき f が r 回連続微分可能と定義している．

Rn ,Rm をノルム空間として扱い，一変数関数としての微分の形式化を行えば一変数
実数値関数の場合と類似の定義，命題が得られ見通しは比較的良くなる．しかしながら,それで定義される微分は，有界線形写像の集合が造るノルム空間 L(Rn , Rm ) の元であり，高階微分は，次章で述べるように

Rm , L(Rn , Rm ), L(Rn , L(Rn , Rm )), L(Rn , L(Rn , L(Rn , Rm ))) · · ·という形の L(Rn , Rm ) が造るノルム空間の「入れ子」が構成される．さらにこれに高階の偏導関数を導入するとより複雑化する．これを正しく扱うには厳密な形式化が必要である．本稿では，この形式化について次章以降で報告する．

2

ノルム空間上の関数の高階導関数
S, T をノルム線形空間とするとき，S から T への写像 L が線形写像であるための条

件と定義は MML で，以下のように LinearOperator of S,T という変数型を導入すること
により形式化している．

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

2/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)

Listing 2. LinearOperator
deﬁnition
let S,T be non empty addMagma;
let L be Function of S,T;
attr L is additivemeans:: VECTSP 1:def 20
for x,y being Element of S holds L.(x+y) = L.x+L.y;
end;
deﬁnition
let S,T be non empty RLSStruct;
let L be Function of S,T;
attr L is homogeneousmeans:: LOPBAN 1:def 5
for x being VECTOR of S,r being Real holds L.(r∗x) = r∗L.x;
end;
deﬁnition
let S,T be RealLinearSpace;mode LinearOperator of S,T is additive homogeneous Function of S,T;
end;

さらにこの線形写像 L が有界 (連続) であるための条件を以下のように Lipschitzian という属性 (attribute) を用いて形式化している．

Listing 3. Lipschitziandeﬁnition
let S,T be RealNormSpace;let L be LinearOperator of S,T;
attr L is Lipschitzian means :: LOPBAN 1:def 8
ex K being Real st 0 <= K & for x being VECTOR of S holds ||. L.x .|| <= K ∗ ||. x .||;
end;

以後，本稿では S から T への有界 (連続) 線形写像全体が造るノルム線形空間を L(S, T )で表す．紙面の制約上，本稿では解説を省くが，このノルム空間を MML では LOPBAN 1[2] で
R NormSpace of BoundedLinearOperators(S, T)と表し定義している．このノルム空間の元 L, F は S から T への有界線形写像であり，加法は写像の和 L + F

L + F : x ∈ S 7→ L.x + F.x ∈ T
で定義され，実数 λ との係数倍は，係数倍の写像 λL で定義している．

λL : x ∈ S 7→ λL.x ∈ T
またノルム ||L|| は||L|| = sup{||L.x|| : x ∈ S&||x|| ≤ 1}で定義される．

2.1

一階微分

f をその定義域 dom f が S の部分集合であり，T に値をとる写像とする．MML では
このように S 全域ではなく，S の部分集合上で定義される写像 (部分関数) を表す変数型
PartFunc of S,T

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

3/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)を定義している．S の全域で定義される関数 Function of S,T は PartFunc of S,T を自動的に認識するが，変数型としては厳密に区別される．以後このような関数を部分関数と呼ぶ．文中，写像あるいは関数とだけ書く場合は全域関数を意味する．以後，ノルム空間 (ノルムアフィン空間) 上での関数の微分を体系的に記述した教科書 [3] の記述に従う．

S の点 x0 ∈ S において S から T への有界線形写像 L と S から T への写像で||R.h||=0||h||̸=0,||h||→0 ||h||
lim

(2)

をみたす R,x0 の近傍 N が存在し，N 内の任意の点 x ∈ S で

f.x − f.x0 = L.(x − x0 ) + R.(x − x0 )(3)が成り立つとき，写像 f は x0 で (フレッシェ) 微分可能であると呼ばれこの有界線形
写像 L を f の x0 における微分と呼ぶ．
df が x0 で微分可能であれば，このような有界線形写像 L は一意に存在し， dx
f (x0 ) な

どで表すが，これは L(S, T ) の元である．

MML ではこれを diﬀ(f,x0) と表記し NDIFF 1 で以下のように定義している．
下記の NDIFF 1:def 5 が (2) 式に対応し，NDIFF 1:def 6 が (3) 式に対応する．

Listing 4. diﬀ
deﬁnition
let S,T;
let IT be PartFunc of S,T;
attr R is RestFunc−likemeans:: NDIFF 1:def 5
R is total & for h st h is non−zero holds (||.h.||”)(#)(R/∗h) is convergent & lim ((||.h.||”)(#)(R/∗h)) = 0.T;
end;
theorem :: NDIFF 1:23
for R be PartFunc of S,T st R is total holds
R is RestFunc−like iﬀ for r be Real st r > 0 ex d be Real st d > 0 &for z be Point of S st z <> 0.S & ||.z.|| < d holds ( ||.z.||”∗ ||. R/.z .||) < r;deﬁnition
let S,T;
let f be PartFunc of S,T;
let x0 be Point of S;
pred f is diﬀerentiable in x0
means:: NDIFF 1:def 6
ex N being Neighbourhood of x0 st N c= dom f & ex L,Rst for x be Point of S st x in N holds f/.x − f/.x0 = L. (x−x0) + R/.(x−x0);
end;
deﬁnition
let S,T;
let f be PartFunc of S,T;
let x0 be Point of S;
assumef is diﬀerentiable in x0;
func diﬀ(f,x0) −> Point of R NormSpace of BoundedLinearOperators(S,T) means :: NDIFF 1:def 7
ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be Point of
S st x in N holds f/.x−f/.x0 = it.(x−x0) + R/.(x−x0);end;

部分関数 f が S の開部分集合 X ⊆ S の全ての点 x ∈ X で微分可能であるとき f は X
上で微分可能であると言う．このとき部分関数x ∈ X 7→df (x) ∈ L(S, T )dx

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

(4)

4/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)
を f の導関数と呼ぶが，これは X から L(S, T ) への写像であり MML では f ‘|X で表し以下のように定義している．

Listing 5. f ‘|Xdeﬁnition
let X,S,T;
let f be PartFunc of S,T;
pred f is diﬀerentiable on X
means:: NDIFF 1:def 8
X c=dom f & for x be Point of S st x in X holds f|X is diﬀerentiable in x;
end;
deﬁnition
let S,T,X;
let f be PartFunc of S,T;
assumef is diﬀerentiable on X;
func f‘|X −> PartFunc of S,R NormSpace of BoundedLinearOperators(S,T) means :: NDIFF 1:def 9
dom it = X & for x be Point of S st x in X holds it/.x = diﬀ(f,x);
end;

紙面数の制約上本稿では解説を省くが以上の微分に関する線形性その他の命題群がNDIFF 1 [4] ∼ NDIFF 6 [5] に収録されている．本稿ではそれらの命題群を高階導関数に拡張した命題群について現状を報告する．

高階導関数の帰納的定義

3

f をその定義域 dom f がノルム空間 S の部分集合である S からノルム空間 T への部
分関数 (PartFunc of S,T) とする．

f が S の開部分集合 X ⊆ S 上で微分可能であるとき f の導関数 f ′ |X の定義域
dom f ′ |X = X は S の部分集合であり，f ′ |X はノルム空間 S からノルム空間 L(S, T ) への部分関数であることから前章の微分の定義の値域を T から L(S, T ) へ変更すればこの定義をそのまま f ′ |X に適用できる．その導関数は(f ′ |X)′ |X : x ∈ X 7→

d ′(f |X)(x) ∈ L(S, L(S, T ))dx

であり，2 次導関数と呼ばれる．
さらにこの 2 次導関数に同じ操作を行えば，その導関数は((f ′ |X)′ |X)′ |X : x ∈ X 7→d((f ′ |X)′ |X)(x) ∈ L(S, L(S, L(S, T )))dx

であり，3 次導関数と呼ばれる．全く同様の操作を繰り返せば，高階の導関数が定義でき
る．NDIFF 6 [5] ではこの帰納的方法で以下のように高階の導関数を定義した．

3.1

有界線形写像が造るノルム空間の「入れ子」

先ず，以下の有界線形写像が造るノルム空間の「入れ子」の列 diﬀ SP を定義する．

Listing 6. NDIFF 6:def 2
deﬁnition let S,T be RealNormSpace;func diﬀ SP(S,T) −> Functionmeans:: NDIFF 6:def 2

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

5/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)

dom it = NAT & it.0 = T & for i be Nat holds
it.(i+1) = R NormSpace of BoundedLinearOperators(S,modetrans(it.i));
end;
deﬁnition
let S,T be RealNormSpace,i be Nat;func diﬀ SP(i,S,T) −> RealNormSpace equals :: NDIFF 6:def 3
diﬀ SP(S,T).i;
end;

上記の記述中の modetrans という Functor は以下で定義される．

definition let S be set;assume S is RealNormSpace;func modetrans(S) -> RealNormSpace equals :: NDIFF_6:def 1
S;
end;
これは「変数型」を厳密に区別する Mizar の特徴に対応する技巧的なもので帰納的定義の過程で，そのままでは，変数型 object をもつ it.i が RealNormSpace(ノルム空間) と自動的には認識されないため，これを RealNormSpace に読み替えるために導入されている．数学的には意味をもたない．

diﬀ SP(S,T,I) はT, L(S, T ), L(S, L(S, T ), L(S, L(S, L(S, T )) · · ·という，ノルム空間の「入れ子」の列を表している．

3.2

高階微分の列Z を S の開部分集合とし，f を前章と同様にその定義域 dom f がノルム空間 S の部
分集合である S からノルム空間 T への部分関数とする．
上記の有界線形写像が造るノルム空間の「入れ子」列 diﬀ SP(S,T,I) を用いて高階微分の列を次のように定義した．

Listing 7. NDIFF 6:def 5
deﬁnition let S,T be RealNormSpace,f be PartFunc of S,T,
Z be Subset of S;
func diﬀ(f,Z) −> Functionmeans:: NDIFF 6:def 5
dom it = NAT & it.0 = f|Z & for i be Nat holds it.(i+1) = modetrans(it.i,S,diﬀ SP(i,S,T)) ‘| Z;
end;
deﬁnition
let S,T be RealNormSpace,f be PartFunc of S,T,
Z be Subset of S,i be Nat;func diﬀ(f,i,Z) −> PartFunc of S,diﬀ SP(i,S,T)
equals:: NDIFF 6:def 6
diﬀ(f,Z).i;
end;

上記の記述中 modetrans も前項と同様に技巧的なもので帰納的定義の過程で，it.i がノルム空間 S からノルム空間 diﬀ SP(i,S,T) への部分関数 (PartFunc of S,diﬀ SP(i,S,T))と自動的には認識されないため，これを読み替えるためのものである．
この微分の列には以下の漸化式が成り立っている．

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

6/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)

Listing 8. NDIFF 6:11
theorem :: NDIFF 6:11
diﬀ(f,Z).0 = f|Z & diﬀ(f,Z).1 = (f|Z)‘| Z & diﬀ(f,Z).2 = ((f|Z)‘| Z) ‘| Z;
theorem :: NDIFF 6:13
diﬀ(f,i+1,Z) = diﬀ(f,i,Z) ‘|Z;3.3

高階微分可能性

この高階微分の列を用いて n 階微分可能性を以下のように述語

is_differentiable_on n,Zで定義する．

Listing 9. NDIFF 6:def 7
deﬁnition
let S,T be RealNormSpace,f be PartFunc of S,T;
let Z be Subset of S,n be Nat;
pred f is diﬀerentiable on n,Zmeans:: NDIFF 6:def 7
Z c= dom f & for i be Nat st i <= n−1 holds modetrans(diﬀ(f,Z).i,S,diﬀ SP(i,S,T)) is diﬀerentiable on Z;
end;以上の定義のもとに，NDIFF 6 では高階微分可能性とその線形性その他について，命題群の形式化証明を行った．以下にその一部を示す．

Listing 10. NDIFF6
theorem :: NDIFF 6:17
for S,T be RealNormSpace,f be PartFunc of S,T,
Z be Subset of S,n be Nat st
f is diﬀerentiable on n,Z for m be Nat st m <= nholds f is diﬀerentiable on m,Z;
theorem :: NDIFF 6:18
for n be Nat,f be PartFunc of S,T
st 1 <= n & f is diﬀerentiable on n,Z holds Z is open;
theorem :: NDIFF 6:20
for n being Nat,f,g being PartFunc of S,T
st 1<=n & f is diﬀerentiable on n,Z & g is diﬀerentiable on n,Zholds
for i being Nat st i<=n holds diﬀ(f+g,i,Z) = diﬀ(f,i,Z) + diﬀ(g,i,Z);
theorem :: NDIFF 6:21
for n be Nat,f,g be PartFunc of S,T
st 1 <= n & f is diﬀerentiable on n,Z & g is diﬀerentiable on n,Zholds f+g is diﬀerentiable on n,Z;4

高階偏導関数の帰納的定義

4.1

一階偏導関数ノルム空間の有限列は PRVECT 2 [6] で RealNormSpace-Sequence という変数型で定義されている．ある自然数 n が存在して x の定義域が自然数の部分集合 Seg n = {i ∈ N :MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

7/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)i ∈ i ≤ n} と一致する写像 x を有限列 (FinSequence) と呼ぶ．n を x の長さと言い，len xで表す. 詳細は省略するが，ノルム空間の長さ n の有限列 G =< ∗G1 , G2 , · · · , Gn ∗ > のQ
多重直積空間 1≤i≤n Gi は PRVECT 2 [6] で以下のように product という名の functorを用いて定義されている．

definition
let G be RealLinearSpace-Sequence;func product G -> non empty strict RLSStruct equals :: PRVECT_2:def 9
RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #);coherence ;end;definition
let G be RealNormSpace-Sequence;func product G -> strict non empty NORMSTR means:: PRVECT_2:def 13

the RLSStruct of it = product (G qua RealLinearSpace-Sequence)& the normF of it = productnorm G;
end;
ノルム空間 product G のベクトルの集合 product (carr G) は各 i ∈ I で xi が Gi の元である有限列 x =< ∗x1 , x2 , · · · , xn ∗ > の集合である．product G の 2 つの元 x, y ∈product G の加法 x + y は写像としての和x + y : i ∈ Seg n 7→ xi + yi ∈ Giであり，実数 λ との係数倍は λx は写像としての係数倍

λx : i ∈ Seg n 7→ λxi ∈ Gi
である．x のノルム||.x.|| =s X||.xi .||21≤i≤nは PRVECT 2 [6] で以下のように表現されている．

definition
let G be RealNormSpace-Sequence;func productnorm G -> Function of product carr (G qua
RealLinearSpace-Sequence),REAL means :: PRVECT_2:def 12
for x being Element of product carr G holds it.x = |.normsequence(G,x).|;end;
NDIFF 5 [7] で product G のベクトル x =< ∗x1 , x2 , · · · , xn ∗ > の第 i 番目の要素を取り出す作用proj(i) : < ∗x1 , x2 , · · · , xn ∗ >∈Y

Gk 7→ xi ∈ Gi

1≤k≤n

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

8/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)
及び第 i 番目の要素を置換する作用

reproj(i, x) : r ∈ Gi 7→< ∗x1 , x2 , · · · , xi−1 , r, xi+1 , · · · , xn ∗ >∈

Y

Gk

1≤k≤n

をそれぞれ以下の functor で定義している．

definition
let G be RealNormSpace-Sequence;
let i be Element of dom G;
func proj i -> Function of product G,G.i means:: NDIFF_5:def 3

for x be Element of product carr G holds it.x = x.i;
end;definition
let G be RealNormSpace-Sequence,i be Element of dom G,
x be Element of product G;
func reproj(i,x) -> Function of G.i,product G means:: NDIFF_5:def 4

for r be Element of G.i holds it.r = x +* (i,r);end;
G =< ∗G1 , G2 , · · · , Gn ∗ > の多重直積空間 product G からノルム空間 F への部分関数

f : x ∈ dom f ⊆ product G 7→ f.x ∈ Fの第 i 成分についての x =< ∗x1 , x2 , · · · , xn ∗ >∈ product G における一階の偏微分可能性と偏微分が以下のように定義されている．

definition
let G be RealNormSpace-Sequence,F be RealNormSpace,let i be set,f be PartFunc of product G,F;
let x being Element of product G;
pred f is_partial_differentiable_in x,i means:: NDIFF_5:def 6

f*reproj(In(i,dom G),x) is_differentiable_in proj(In(i,dom G)).x;
end;
definition
let G be RealNormSpace-Sequence,F be RealNormSpace;
let i be set,f be PartFunc of product G,F;
let x be Point of product G;
func partdiff(f,x,i)-> Point of R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),F)

equals:: NDIFF_5:def 7
diff(f*reproj(In(i,dom G),x),proj(In(i,dom G)).x);
end;

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

9/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)
NDIFF 5:def 6 は, 写像
Yr ∈ Gi 7→ f (x1 , x2 , · · · , xi−1 , r, xi+1 , · · · , xn ) ∈

Gk

1≤k≤n

が r = xi で微分可能なとき，f は x で 第 i 成分について偏微分可能であることを意味する．NDIFF 5:def 7 は∂d
f (x1 , x2 , · · · , xn ) =f (x1 , x2 , · · · , xi−1 , r, xi+1 , · · · , xn )
∂xi
dr
r=xi
を意味する．
前章と同様に product G の部分集合 X 上の第 i 成分に関する一階の偏微分可能性と偏導関数が定義できる．

definition
let G be RealNormSpace-Sequence,F be RealNormSpace;
let i be set,f be PartFunc of product G,F;
let X be set;
pred f is_partial_differentiable_on X,i means:: NDIFF_5:def 8

X c= dom f & for x be Point of product G st x in X
holds f|X is_partial_differentiable_in x,i;
end;
definition
let G be RealNormSpace-Sequence;let S be RealNormSpace;
let i be set;let f be PartFunc of product G, S;
let X be set;assumef is_partial_differentiable_on X,i;func f ‘partial|(X,i) -> PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),S)
means :: NDIFF_5:def 9
dom it = X &for x be Point of product G st x in X holds it/.x = partdiff(f,x,i);end;
以上の定義のもとに，筆者らは NDIFF 5 [7] で偏微分可能性とその偏微分の線形性その他について，命題群の形式化証明を行っている．以下はその一部である．

Listing 11. NDIFF5
theorem :: NDIFF 5:56
for G be RealNormSpace−Sequence,S be RealNormSpace,f be PartFunc of product G,S,
X be Subset of product G,x be Point of product G
st X is open & x in X &(for i be set st i in dom G holds f is partial diﬀerentiable on X,i & f‘partial|(X,i) is continuous on X)
holds

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

10/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)

f is diﬀerentiable in x & for h be Point of product G
ex w be FinSequence of S st dom w = dom G &(for i be set st i in dom G holds w.i = partdiﬀ(f,x,i).(proj(In(i,dom G)).h))& diﬀ(f,x).h = Sum w;
theorem :: NDIFF 5:57
for G be RealNormSpace−Sequence,F be RealNormSpace,f be PartFunc of product G,F,X be Subset of product G
st X is open holds(for i be set st i in dom G holds f is partial diﬀerentiable on X,i & f‘partial|(X,i) is continuous on X)
iﬀ f is diﬀerentiable on X & f‘|X is continuous on X;

特に，命題 NDIFF 5:57 は第一章で述べた各変数についての連続偏微分可能性による微分可能性の定義と本稿で述べている連続微分可能性の定義が同値であることを示して
いる．

4.2

高階偏導関数高階導関数と同様に一階の偏微分可能性と偏微分を用いれば，帰納的高階の偏微分が定義できる．先ず，以下の有界線形写像が造るノルム空間の「入れ子」の列 Partdiﬀ SPを定義する．

Listing 12. PartdiﬀSP
deﬁnition
let S be RealNormSpace−Sequence,T be RealNormSpace,
I be non empty FinSequence of (dom S) ;func Partdiﬀ SP(S,T,I) −> RealNormSpace−Sequencemeans:: NDIFF14:def 3
dom it = dom I & it.1 = R NormSpace of BoundedLinearOperators(S.(In(I.1,dom S)),T)& for i be 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));
end;
deﬁnition
let S be RealNormSpace−Sequence,T be RealNormSpace,I be non empty FinSequence of (dom S),
i be Nat ;assume 1<=i & i <= len I;
func Partdiﬀ SP(S,T,I,i) −> RealNormSpace equals :: NDIFF14:def 4Partdiﬀ SP(S,T,I).i;
end;
deﬁnition
let S be RealNormSpace−Sequence,T be RealNormSpace,I be non empty FinSequence of (dom S);
func PartdiﬀSP(S,T,I) −> RealNormSpace equals :: NDIFF14:def 5( Partdiﬀ SP(S,T,I) ).(len I);
end;

これは例えば T をノルム空間，S を長さ 3 のノルム空間の有限列 S1 = X, S2 = Y, S3 =Z, domS = {1, 2, 3} とし，I を長さ 4 の domS = {1, 2, 3} の有限列 I1 = 2, I2 = 1, I3 =2, I4 = 1 とするとき Partdiﬀ SP(S,T,I) はL(Y, T ), L(X, L(Y, T )), L(Y, L(X, L(Y, T ))), L(X, L(Y, L(X, L(Y, T ))))となる有限列である．この有界線形写像が造るノルム空間の「入れ子」を用いて高階偏微分の列を以下で定義した．

Listing 13. PartDiﬀSeq

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

11/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)deﬁnition
let S be RealNormSpace−Sequence,T be RealNormSpace,Z be Subset of product S,
I be non empty FinSequence of (dom S),
f be PartFunc of product S,T;
func PartDiﬀSeq(f,Z,I) −> FinSequencemeans:: NDIFF14:def 6
dom it = dom I & it.1 = f‘partial|(Z,I.1)& for i be Nat
st 1<=i & i < len I holds
ex g be PartFunc of product S,Partdiﬀ SP(S,T,I,i)
st it.i = g & it.(i+1) = g‘partial|(Z,I.(i+1));
end;
deﬁnition
let S be RealNormSpace−Sequence,T be RealNormSpace,Z be Subset of product S,
I be non empty FinSequence of (dom S),
f be PartFunc of product S,T;
let i be Nat ;assume 1 <=i & i <= len I;
func PartDiﬀSeq(f,Z,I,i) −> PartFunc of product S,Partdiﬀ SP(S,T,I,i) equals :: NDIFF14:def 7
PartDiﬀSeq(f,Z,I).i;
end;

前述の例と同様に T をノルム空間，S を長さ 3 のノルム空間の有限列 S1 = X, S2 =Y, S3 = Z, dom S = {1, 2, 3} とし，I を長さ 4 の dom S = {1, 2, 3} の有限列 I1 = 2, I2 =1, I3 = 2, I4 = 1 とするとき，関数f : (x, y, z) ∈Y

Si = X × Y × Z 7→ f (x, y, z) ∈ T

1≤i≤3の 4 階の偏導関数 PartDiﬀSeq(f,Z,I) は第 1,2,3 の変数 x, y, z に関する偏導関数をそれぞれ ∂∂X f, ∂∂Y f, ∂∂Z f と表すことにすれば，

∂
∂2
∂3
∂4
f,
f,
f,
f
∂Y ∂X ∂Y ∂Y ∂X ∂Y ∂X ∂Y ∂X ∂Y
である．この高階偏微分の列を用いて高階偏微分可能性を以下のように述語

is_partial_differentiable_onで定義する．

Listing 14. NDIFF14:def 8
deﬁnition
let S be RealNormSpace−Sequence,T be RealNormSpace,Z be Subset of product S,
I be non empty FinSequence of (dom S),
f be PartFunc of product S,T;
pred f is partial diﬀerentiable on Z, I means :: NDIFF14:def 8
f is partial diﬀerentiable on Z,I.1& for i be Nat st 1 <= i & i < (len I)
holds PartDiﬀSeq(f,Z,I,i) is partial diﬀerentiable on Z,I.(i+1);
end;

また高階偏微分を以下で定義する．

Listing 15. NDIFF14:def 9
deﬁnition
let S be RealNormSpace−Sequence,T be RealNormSpace,
Z be Subset of product S, I be non empty FinSequence of (dom S),
f be PartFunc of product S,T;

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

12/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)

func f ‘partial| (Z,I) −>PartFunc of product S,Partdiﬀ SP(S,T,I,len I)
PartDiﬀSeq (f,Z,I,len I);
end;equals:: NDIFF14:def 9以上の定義のもとに，NDIFF14 では高階偏微分可能性とその偏微分の線形性について，以下の命題群の形式化証明を行った．以下にその一部を示す．

Listing 16. NDIFF14:30-31
theorem :: NDIFF14:30
for S be RealNormSpace−Sequence,T be RealNormSpace,Z be Subset of product S,
I be non empty FinSequence of (dom S),
f,g be PartFunc of product S,T
st Z is open & f is partial diﬀerentiable on Z,I & g is partial diﬀerentiable on Z,Iholds f+g is partial diﬀerentiable on Z,I& for i be Nat st 1<= i & i <= len I holds PartDiﬀSeq(f+g,Z,I,i)=PartDiﬀSeq(f,Z,I,i) + PartDiﬀSeq(g,Z,I,i);theorem :: NDIFF14:31
for S be RealNormSpace−Sequence,T be RealNormSpace,Z be Subset of product S,
I be non empty FinSequence of (dom S),
f be PartFunc of product S,T,a be Realst Z is open & f is partial diﬀerentiable on Z,Iholds a(#)f is partial diﬀerentiable on Z,I& for i be Nat st 1<= i & i <= len I
holds PartDiﬀSeq(a(#)f,Z,I,i) =a(#)PartDiﬀSeq(f,Z,I,i);5有界双線形写像と合成関数の微分
このノルム空間の S, T, U について，f を S から T への部分関数，g を T から U への部分関数とするとき，f, g の合成関数 g · f の一階微分に関する定理は以下がある．

Listing 17. NDIFF 2:13
theorem :: NDIFF 2:13
for f1 be PartFunc of S,T st f1 is diﬀerentiable in x0 for f2 be
PartFunc of T,U st f2 is diﬀerentiable in (f1/.x0) holds f2∗f1
is diﬀerentiable in x0 & diﬀ(f2∗f1,x0) = diﬀ(f2,f1/.x0)∗diﬀ(f1,x0);

これを n 階微分に拡張するためには，微分の階数に関する数学的帰納法を用いるが，その際に有界双線形写像の微分を用いる必要がある．

E, F, G をノルム空間とするとき，E, F から G への双線形写像 (BilinearOperator of
E,F,G) は LOPBAN 8 [8] で定義され，以下の定理で特徴付けられ，変数型 BilinearOperator of E,F,G が導入されている．
Listing 18. LOPBAN 8:12
theorem :: LOPBAN 8:12
for E,F,G be RealNormSpace,L be Function of [:E,F:],Gholds
L is Bilinear
iﬀ( ( for x1,x2 be Point of E,y be Point of F holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y) )&( for x be Point of E,y be Point of F,a be Real holds L.(a∗x,y) = a ∗ L.(x,y) )&( for x be Point of E,y1,y2 be Point of F holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2) )MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

13/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)&( for x be Point of E,y be Point of F,a be Real holds L.(x,a∗y) = a ∗ L.(x,y) ) );deﬁnition
let E,F,G be RealNormSpace;mode BilinearOperator of E,F,G is Bilinear Function of [:E,F:],G;end;

また, 有界 (連続) 双線形写像は以下のように特徴付けられ, 定義されている.

Listing 19. LOPBAN 9:def 3
theorem :: LOPBAN 8:13
for E,F,G be RealNormSpace,f be BilinearOperator of E,F,G
holds( f is continuous on the carrier of [:E,F:] iﬀ f is continuous in 0.( [:E,F:] ) )&( f is continuous on the carrier of [:E,F:]
iﬀ
ex K be Real st 0 <= K & for x be Point of E,y be Point of F
holds ||. f.(x,y) .|| <= K ∗ ||.x.|| ∗ ||.y.|| );deﬁnition
let E,F,G be RealNormSpace;let f be BilinearOperator of E,F,G;
attr f is Lipschitzian means :: LOPBAN 9:def 3
ex K being Real st 0 <= K &for x being VECTOR of E,y being VECTOR ofend;

F holds ||. f.(x,y) .|| <= K ∗ ||. x .|| ∗ ||. y .||;

有界 (連続) 線形写像，有界 (連続) 双線形写像は以下のように任意の階数で連続微分可能である．

Listing 20. NDIFF12
theorem :: NDIFF12:20
for L be Lipschitzian LinearOperator of E,Fholds for i be Nat holdsdiﬀ(L,i,[#]E) is diﬀerentiable on [#]E & diﬀ(L,i,[#]E) ‘| [#]E is continuous on [#]E;
theorem :: NDIFF12:21
for B be Lipschitzian BilinearOperator of E,F,G
holds
for i be Nat
holds diﬀ (B,i,[#][:E,F:]) is diﬀerentiable on [#][:E,F:]& diﬀ (B,i,[#][:E,F:]) ‘| [#][:E,F:] is continuous on [#][:E,F:];

これを用いると有界双線形写像と合成関数の一階微分に関する定理が得られる．

Listing 21. NDIFF13:42
theorem :: NDIFF13:42
for i be Nat, S,E,F,G be RealNormSpace,Z be Subset of S,
B be Lipschitzian BilinearOperator of E,F,G,
u be PartFunc of S,E, v be PartFunc of S,F,
w be PartFunc of S,[:E,F:], W be PartFunc of S,Gst W = B ∗ w & w = <:u,v:>& u is diﬀerentiable on i,Z & diﬀ(u,i,Z) is continuous on Z
& v is diﬀerentiable on i,Z & diﬀ(v,i,Z) is continuous on Z
holds
W is diﬀerentiable on i,Z & diﬀ(W,i,Z) is continuous on Z;
theorem :: NDIFF13:44
for i be Nat,E,F,G be RealNormSpace,Z be Subset of E,
T be Subset of F,u be PartFunc of E,F,v be PartFunc of F,G

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

14/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)

st u.:Z c= T
& u is diﬀerentiable on i,Z & diﬀ(u,i,Z) is continuous on Z
& v is diﬀerentiable on i,T & diﬀ(v,i,T) is continuous on T
holdsv∗u is diﬀerentiable on i,Z & diﬀ(v∗u,i,Z) is continuous on Z;

さらに上記の定理を高階微分に拡張した以下の定理を得た．

Listing 22. NDIFF13:61
theorem :: NDIFF13:61
for S,E,F be RealNormSpace,u be PartFunc of S,E,v be PartFunc of S,F,
w be PartFunc of S,[:E,F:],Z be Subset of S,i be Nat
st w = <:u,v:>& u is diﬀerentiable on i+1,Z & diﬀ(u,i+1,Z) is continuous on Z
& v is diﬀerentiable on i+1,Z & diﬀ(v,i+1,Z) is continuous on Z
holds
w is diﬀerentiable on i+1,Z & diﬀ(w,i+1,Z) is continuous on Z;n 階連続微分可能性と，全ての変数に関する n 階連続偏微分可能性が同値であることの以下の定理の証明を形式化した．

Listing 23. NDIFF14:36
theorem :: NDIFF14:36
for G being RealNormSpace−Sequence,
X being non empty open Subset of (product G),
F being RealNormSpace,f being PartFunc of (product G),F
for n being Nat st 1 <= nholds ( f is diﬀerentiable on n,X & diﬀ (f,n,X) is continuous on X )iﬀ
for I being non empty FinSequence of (dom G)
st len I <= n holds f is partial diﬀerentiable on X,I & f ‘partial| (X,I) is continuous on X;

Q
さらに, ノルム空間の有限列 {Si }1≤i≤n の多重直積空間 1≤i≤n Si から有限列 {Fk }1≤k≤m
Qの多重直積空間 1≤k≤m Fk への部分関数について以下の定理を形式化した．
これを用いれば，Rn から Rm への多変数関数 f の k 階連続微分可能性に関して，第 1章の冒頭に述べた (1) 式のように全変数について連続偏微分可能性を用いた定義と Rn , Rm
をノルム空間とみなし，f を一変数関数として扱った場合の k 階連続微分可能性が同値であることが容易に判る．この同値性については紙面の制約上割愛し次回以降に報告する．

Listing 24. NDIFF15:32
theorem :: NDIFF15:32
for S be RealNormSpace−Sequence, F be RealNormSpace−Sequence,
g be PartFunc of product F,product S, X be non empty open Subset of product F,
k be Natst X c=dom g & 1 <=kholds ( g is diﬀerentiable on k,X & diﬀ (g,k,X) is continuous on X )iﬀfor i be Element of dom S
holds for I being non empty FinSequence of (dom F) st len I <= k holds
proj(i)∗g is partial diﬀerentiable on X,I & (proj(i)∗g)‘partial| (X,I) is continuous on X;

6

まとめ
ノルム空間上の部分関数の高階微分の形式化の現状について報告した．筆者らは既にこれに基づいて，ノルム空間上の Taylor 展開や，n 階連続微分可能な関数についての陰MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

15/16

Mechanized Mathematics and Its Applications, Works in Progress Formalizations for Higher Derivatives (Shidama and Nakasho)
関数定理，逆関数定理などの証明を形式化した．さらに，それらの諸定理の準備の上に微分多様体の形式化を開始している．これらについては次回以降に報告する．

参考文献[1] Matsushima Y. Tayotai nyumon. Shokabo; 1965.
[2] Shidama Y. Banach Space of Bounded Linear Operators. Formalized Mathematics. 2004;12(1):39–48. Available from: http://fm.mizar.org/2004-12/pdf12-1/
lopban_1.pdf.
[3] Schwartz L, Kojima J. Kaisekigaku 2 (Bibunhou). Tokyo Tosho; 1985.
[4] Imura H, Kimura M, Shidama Y. The Diﬀerentiable Functions on Normed Linear
Spaces. Formalized Mathematics. 2004;12(3):321–327. Available from: http://fm.
mizar.org/2004-12/pdf12-3/ndiff_1.pdf.
[5] Endou N, Shidama Y. Diﬀerentiation in Normed Spaces. Formalized Mathematics.
2013;21(2):95–102.
[6] Endou N, Shidama Y, Miyajima K. The Product Space of Real Normed Spaces and
its Properties. Formalized Mathematics. 2007;15(3):81–85.
[7] Shidama Y. Diﬀerentiable Functions on Normed Linear Spaces. Formalized Mathematics. 2012;20(1):31–40.
[8] Nakasho K, Futa Y, Shidama Y. Continuity of Bounded Linear Operators on Normed
Linear Spaces. Formalized Mathematics. 2018;26(3):231–237.

Mizar article information
Works in Progress
NDIFF12 Dif f erential of Lipschitzian Bilinear Operators
by Kazuhisa Nakasho and Yasunari Shidama
Summary: In this article,we formalized the proves of some fundamentally important theorems
for higher-order derivatives of bounded bilinear Operator on norm spaces.

NDIFF13 Dif f erentiation of composite f unctions
by Kazuhisa Nakasho and Yasunari Shidama
Summary: In this articlce,we formalized the proves of some fundamentally important theorems for higher-order derivatives of composite functions on norm spaces. as next,using thesethorem, we proved the inverce functions theorem for norm-valued function of norm space.

NDIFF14 Higher order derivatives and partial derivatives
by Kazuhisa Nakasho and Yasunari Shidama
Summary: In this article, we formalized the deﬁnitions of higher-order derivatives and partial
derivatives of vector valued functions on norme spaces using an inductive construction method,and prove some fundamentally important theorems.

MMA-WiP (2022), vol.4, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.2 - ISSN 2434-5458 (Online)

16/16