Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

Regular Paper

高階微分による陰関数定理の形式化について
On The Formalizations for Implicit Function
Theorem with Higher Derivatives of Vector Valued
Functions
中正 和久 1,* 師玉 康成 2Kazuhisa Nakasho1,* Yasunari Shidama2
1 山口大学大学院創成科学研究科, 山口県宇部市常盤台 2-16-1
1 Graduated School of Science and Technology for Innovation, Yamaguchi University,
2-16-1 Tokiwa-dai, Ube, Japan
2 長野県軽井沢町
2 Karuizawa, Nagano, Japan* nakasho@yamaguchi-u.ac.jp
Proof checked by Mizar Version: 8.1.12 and MML Version: 5.73.1435
Received: December 6, 2022. Accepted: March 14, 2023.

Abstract
In this paper, we report on the formalization of the implicit function theorem andthe inverse function theorem with higher-order derivatives and partial derivatives ofvector-valued functions on normed spaces.

1

はじめに
筆者らはこれまでに Laurent Schwartz による著書 [1] にしたがって，[2] でノルム空間上の陰関数定理を，[3] で逆関数定理をそれぞれ以下のように形式化した．

Listing 1. NDIFF 9:21
theorem :: NDIFF 9:21
for E be RealNormSpace,
G,F be non trivial RealBanachSpace,
Z be Subset of [:E,F:],f be PartFunc of [:E,F:], G,a be Point of E, b be Point of F, c be Point of G,
z be Point of [:E,F:]
st Z is open & dom f = Z

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

1/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)& f is diﬀerentiable on Z & f ‘| Z is continuous on Z
& [a,b] in Z & f.(a,b) = c & z = [a,b]& partdiﬀ‘2(f,z) is invertible
holds
ex r1,r2 be Realst 0 < r1 & 0 < r2
& [:Ball(a,r1),cl Ball(b,r2):] c= Z
& ( for x be Point of E st x in Ball(a,r1) holds
ex y be Point of F st y in Ball(b,r2) & f.(x,y) = c )& ( for x be Point of E st x in Ball(a,r1) holds
for y1,y2 be Point of F st y1 in Ball(b,r2) & y2 in Ball(b,r2)& f.(x,y1) = c & f.(x,y2) = c holds y1=y2 )& ( ex g be PartFunc of E,F
st dom g = Ball(a,r1) & rng g c= Ball(b,r2)& g is continuous on Ball(a,r1) & g.a = b& ( for x be Point of E st x in Ball(a,r1) holds f.(x,g.x) = c )& g is diﬀerentiable on Ball(a,r1)& g ‘| Ball(a,r1) is continuous on Ball(a,r1)& ( for x be Point of E, z be Point of [:E,F:]
st x in Ball(a,r1) & z = [x,g.x]
holds diﬀ(g,x) = − ( Inv partdiﬀ‘2(f,z)) ∗ partdiﬀ‘1(f,z) )& ( for x be Point of E, z be Point of [:E,F:]
st x in Ball(a,r1) & z =[x,g.x]
holds partdiﬀ‘2(f,z) is invertible ) )& ( for g1,g2 be PartFunc of E,F
st dom g1 = Ball(a,r1) & rng g1 c= Ball(b,r2)& ( for x be Point of E st x in Ball(a,r1) holds f.(x,g1.x) = c )& dom g2 = Ball(a,r1) & rng g2 c= Ball(b,r2)& ( for x be Point of E st x in Ball(a,r1) holds f.(x,g2.x) = c )holds g1 = g2);

Listing 2. NDIFF10:17
theorem :: NDIFF10:17
for E,F be non trivial RealBanachSpace,
Z be Subset of E,
f be PartFunc of E,F,
a be Point of E, b be Point of F
st Z is open & dom f = Z& f is diﬀerentiable on Z & f ‘| Z is continuous on Z
& a in Z & f.a = b& diﬀ(f,a) is invertible
holds
ex A be Subset of E,B be Subset of F,
g be PartFunc of F,E
st A is open & B is open
& A c= dom f & a in A & b in B
& f.:A = B & dom g = B & rng g = A& dom(f|A) = A & rng(f|A) = B& (f|A) is one−to−one & g is one−to−one& g = (f|A)” & (f|A) = g” & g.b = a& g is continuous on B & g is diﬀerentiable on B
& g ‘| B is continuous on B & ( for y be Point of F st y in B
holds diﬀ(f,g/.y) is invertible )& ( for y be Point of F st y in B holds diﬀ(g,y) = Inv diﬀ(f,g/.y) );さらに [4] では有限次元空間上でのそれらの行列表現を形式化した．また， [5] で報告した NDIFF12.abs ではノルム空間上での高階微分，偏微分の形式化を行っている．本稿
では，これらを用いたノルム空間上の高階連続微分可能関数に関する陰関数定理と逆関数定理の形式化について報告する．
筆者らは，上記の NDIFF 9:21 で存在が保証されている陰関数 g について，以下のNDIFF13:65 のように f が高階連続微分可能であるときに，g も同様に高階連続微分可能であることを示す定理とその証明の形式化を行った．

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

2/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

Listing 3. NDIFF13:65
theorem :: NDIFF13:65
for E be RealBanachSpace, F,G be non trivial RealBanachSpace,
Z be non empty Subset of [:E,F:],c be Point of G,
A be Subset of E, B be Subset of F
st Z is open & A is open & B is open & [:A,B:] c= Z
holds
for i be Nat,f be PartFunc of [:E,F:],G, g be PartFunc of E,F
st dom f = Z & f is diﬀerentiable on i+1,Z& diﬀ(f,i+1,Z) is continuous on Z
& dom g = A & rng g c= B & g is continuous on A
& ( for x be Point of E st x in A holds f.(x,g.x) = c )& ( for x be Point of E, z be Point of [:E,F:] st x in A & z = [x,g.x]
holds partdiﬀ‘2(f,z) is invertible )holds
g is diﬀerentiable on i+1,A & diﬀ(g,i+1,A) is continuous on A
& for x be Point of E, z be Point of [:E,F:] st x in A & z = [x,g.x]
holds diﬀ(g,x) = − (Inv partdiﬀ‘2(f,z)) ∗ partdiﬀ‘1(f,z);

その概要は次の通りである．

E をノルム空間,F, G をバナハ空間 (RealBanachSpace)，Z を E, F の直積空間 E × Fの開部分集合，c を G の点，A, B をそれぞれ E, F の開集合で

A×B ⊆Zとする．

f : (x, y) ∈ Z ⊆ E × F 7→ f (x, y) ∈ G
を Z から G への写像で Z 上で i + 1 階連続微分可能とする．また，g を A から B への写像で A に含まれる E の任意の点 x ∈ A についてf (x, g(x)) = c
かつ∂f(x, g(x))∂yが可逆であるとする．このとき，g は i + 1 階連続微分可能であり，A に含まれる E の任意の点 x ∈ A について

g ′ (x) =(∂f(x, g(x))
∂y

)−1
◦

∂f
(x, g(x))
∂x

(1)

である．
さらに，以下の NDIFF13:67 のように，上記の逆関数定理 NDIFF10:17 の関数 f がn + 1 階連続微分可能であるとき，その存在が保証される関数 g も n + 1 階連続微分可能であることを示す定理とその証明の形式化を行った．

Listing 4. NDIFF13:67
theorem :: NDIFF13:67
for E,F be non trivial RealBanachSpace,
Z be Subset of E, f be PartFunc of E,F,
a be Point of E, b be Point of F, n be Nat
st Z is open & dom f = Z & f is diﬀerentiable on n+1,Z & diﬀ(f,n+1,Z) is continuous on Z

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

3/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)& a in Z & f.a = b & diﬀ(f,a) is invertible
holds
ex A be Subset of E,B be Subset of F, g be PartFunc of F,E
st A is open & B is open & A c= dom f& a in A & b in B & f.:A = B& dom g = B & rng g = A & dom(f|A) = A & rng(f|A) = B& (f|A) is one−to−one & g is one−to−one& g = (f|A)” & (f|A) = g” & g.b = a& ( for y be Point of F st y in B holds diﬀ(f,g/.y) is invertible )& ( for y be Point of F st y in B holds diﬀ(g,y) = Inv diﬀ(f,g/.y) )& f is diﬀerentiable on n+1,A & diﬀ(f,n+1,A) is continuous on A
& g is diﬀerentiable on n+1,B & diﬀ(g,n+1,B) is continuous on B;

その概要は次の通りである．

E, F をバナハ空間 (RealBanachSpace)，Z を E の開部分集合，
f : x ∈ Z ⊆ E 7→ f (x) ∈ F
を Z から F への写像で Z 上で n + 1 階連続微分可能とする．a, b をそれぞれ E, F の元とし，a は Z に含まれ

f (a) = b(2)

f (a) が可逆

(3)′とする．このとき，f の定義域 Z に含まれる a の開近傍 A と b の開近傍 B 及び B から

A の上への写像 g が存在し，
f (A) = B, g(b) = aを満たす．f の A 上への制限 f |A と g は全単射であり，互いに逆写像になっている．しかも，f |A と g はそれぞれ A, B 上 n + 1 階連続微分可能である．また，B の任意の点 y ∈ B
について

f ′ (g(y))
は可逆であり，g ′ (y) = f ′ (g(y))−1
を満たす．

積の微分

2

ここで，3 章と 4 章で述べる定理の証明で用いられる中心的な命題について述べておく．

2.1

ライプニッツの公式

ノルム空間 S, E, F について S から E への写像 u と，S から F への写像 v が与えられたとき，これらの写像と S から E × F への写像uv : x ∈ S 7→ (u(x), v(x)) ∈ E × F(4)が定義できる．

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

4/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

ノルム空間 S, E, F, G と S の開集合 Z ，任意の自然数 n について，E × F から G への有界連続双線形写像

B : (x, y) ∈ E × F 7→ B(x, y) ∈ Gおよび，Z 上で n 階連続微分可能写像であるそれぞれ S から E への写像 u と，S から Fへの写像 v が与えられたとき，これらの写像と S から (4) 式により E × F への写像uv : x ∈ S 7→ (u(x), v(x)) ∈ E × F

を用いて合成される S から F への写像

B ◦ (uv) : x ∈ S 7→ (B ◦ (uv))(x) = B(u(x), v(x)) ∈ F

は n 階連続微分可能である．筆者らはこれを以下のように形式化した．

Listing 5. 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;

この命題の証明には微分の階数 n についての帰納法を用いる．

n = 1 についてはまず，Listing 6. NDIFF12:14
theorem :: NDIFF12:14
for f be Lipschitzian BilinearOperator of E,F,G, Z be Subset of [:E,F:]
st Z is open
holds
f is diﬀerentiable on Z & f ‘| Z is continuous on Z;

から有界連続双線形写像 B はその定義域 E × F 上連続微分可能である.
また写像 uvはListing 7. NDIFF13:29
theorem :: NDIFF13:29
for S,T,U be RealNormSpace,Z be Subset of S,
u be PartFunc of S,T, v be PartFunc of S,U,w be PartFunc of S,[:T,U:]
st u is diﬀerentiable on Z & u ‘| Z is continuous on Z
& v is diﬀerentiable on Z & v ‘| Z is continuous on Z
& w = <:u,v:>
holds
w is diﬀerentiable on Z & w ‘| Z is continuous on Z;

から Z 上連続微分可能である．
写像 B と uv の合成 B ◦ (uv) は

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

5/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

Listing 8. NDIFF13:23
theorem :: NDIFF13:23
for 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
st u .: Z c= T
& u is diﬀerentiable on Z & u ‘| Z is continuous on Z
& v is diﬀerentiable on T & v ‘| T is continuous on T
holdsv∗u is diﬀerentiable on Z & v∗u ‘| Z is continuous on Z;

から Z 上連続微分可能である．
次に帰納法の仮定により微分の階数 n について定理が成り立つものとする．以後の議論はライプニッツの公式(B ◦ (uv))′ (x) ds = B(u′ (x) ds, v(x)) + B(u(x), v ′ (x) ds)(5)による．これは以下のように形式化されている．

Listing 9. NDIFF13:35
theorem :: NDIFF13:35
for S,E,F,G be RealNormSpace,Z be Subset of S,
B be Lipschitzian BilinearOperator of E,F,G,
W be PartFunc of S,G, w be PartFunc of S,[:E,F:],u be PartFunc of S,E, v be PartFunc of S,F
st u is diﬀerentiable on Z & v is diﬀerentiable on Z
& W = B ∗ w & w = <:u,v:>
holds
W is diﬀerentiable on Z
& for x be Point of S st x in Z holds
for ds be Point of S
holds((W‘|Z)/.x).ds = B.(((u‘|Z)/.x).ds, v/.x) + B.(u/.x, ((v‘|Z)/.x).ds);(5) 式の左辺はノルム空間 S の元 ds に S から G への有界線形写像が作る空間 L(S, G) の元である有界線形写像(B ◦ (uv))′ (x)が作用していることを表している．

(B ◦ (uv))′

は S から L(S, G) への写像である.

F の元 v ∈ F に関して写像
Bv : z ∈ E 7→ B(z, v)
は E から G への有界線形写像が作る空間 L(E, G) の元である．
写像

B1 : v ∈ F 7→ Bv ∈ L(E, G)
は F から L(E, G) への有界線形写像である．

(5) 式の右辺第 1 項はMMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

6/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)B(u′ (x) ds, v(x)) = Bv(x) (u′ (x) ds)= (B1 ◦ v)(x)(u′ (x) ds)= ((B1 ◦ v)(x) ◦ u′ (x)) ds(6)と書き表せる. 同様に E の元 u ∈ E に関して写像

Bu : z ∈ F 7→ B(u, z)
は F から G への有界線形写像が作る空間 L(F, G) の元である.
写像

B2 : u ∈ E 7→ Bu ∈ L(F, G)
は E から L(F, G) への有界線形写像である.

(5) 式の右辺第 2 項はB(u(x), v ′ (x) ds) = ((B2 ◦ u)(x) ◦ v ′ (x)) ds(7)と書き表せる.

(6)(7) 式から，(5) 式は((B ◦ (uv))′ (x)) ds = ((B1 ◦ v)(x) ◦ u′ (x)) ds + ((B2 ◦ u)(x) ◦ v ′ (x)) ds(8)と書き表せる．これから(B ◦ (uv))′ (x) = (B1 ◦ v)(x) ◦ u′ (x) + (B2 ◦ u)(x) ◦ v ′ (x)

(9)

を得る．
写像 B1 ◦ v は有界線形写像 B1 と n 階連続微分可能な写像 v との合成であり，以下の命題により n 階連続微分可能である．

Listing 10. NDIFF13:26
theorem :: NDIFF13:26
for E,F,G be RealNormSpace, Z be Subset of E,
u be PartFunc of E,F,L be Lipschitzian LinearOperator of F,G
holds
for i be Nat
st u is diﬀerentiable on i,Z & diﬀ(u,i,Z) is continuous on Z
holds L∗u is diﬀerentiable on i,Z & diﬀ(L∗u,i,Z) is continuous on Z;

また，仮定から u は n + 1 階連続微分可能であるため，du/dx は n 階連続微分可能である．写像の合成は有界双線形写像であるから，帰納法の仮定から(B1 ◦ v)(x) ◦ u′ (x)は n 階連続微分可能である．同様に，(B2 ◦ u)(x) ◦ v ′ (x)MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

7/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

も n 階連続微分可能である．
以上から (9) 式により(B ◦ (uv))′

は n 階連続微分可能である.
最後にListing 11. NDIFF13:33
theorem :: NDIFF13:33
for E,F be RealNormSpace,n be Nat, Z be Subset of E,
g be PartFunc of E,F
st g‘|Z is diﬀerentiable on n,Z & g is diﬀerentiable on Z
& diﬀ(g‘|Z,n,Z) is continuous on Z
holds g is diﬀerentiable on n+1,Z & diﬀ(g,n+1,Z) is continuous on Z;

を適用して，B ◦ (uv) が n + 1 階連続微分可能であることが示される. 以上で微分の階数に関する帰納法の証明が完成する.

2.2

合成関数の微分

前項の命題を用いれば以下のように２つの連続微分可能な写像の合成写像が連続微分可能になることを示すことができる．
ノルム空間 E, F, G と部分関数 u : E → F ，v : F → G に対して，u は Z(⊂ E) 上で，

v は T (⊂ F ) 上でそれぞれ n 階連続微分可能で，u(Z) ⊆ T
を満たすものとする．このとき，u, v の合成写像v◦uは，Z 上で n 階連続微分可能写像である．これを形式化したものが以下である．

Listing 12. NDIFF13:44
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
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;

この命題の証明には微分の階数 n についての帰納法を用いる．

n = 1 については NDIFF13:23 で証明されている. 微分の階数が n の場合に成り立つものとする．u, v が n + 1 階連続微分可能であるとする．微分の階数を下げるために，合成関数の微分(v ◦ u)′ (x) = v ′ (u(x)) ◦ u′ (x) = (v ′ ◦ u)(x) ◦ u′ (x)(10)

を用いる．これは以下で形式化されている.

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

8/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

Listing 13. NDIFF13:19
theorem :: NDIFF13:19
for 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
st u.:Z c= T
& u is diﬀerentiable on Z & v is diﬀerentiable on T
holdsv∗u is diﬀerentiable on Z
& for x be Point of E st x in Z
holds ((v∗u) ‘| Z) /. x = ((v‘| T) /. (u /. x)) ∗ ((u‘| Z)/.x);u, v が n + 1 階連続微分可能であるから，u は n 階連続微分可能であり，v ′ も n 階連
続微分可能である．したがって，帰納法の仮定から，(10) 式中の関数 v ′ ◦ u も n 階連続微分可能である．これは E からノルム空間 F から G への有界線形写像が作る空間 L(F, G)への写像である．

u′ は，E からノルム空間 E から F への有界線形写像が作る空間 L(E, F ) への n 階連
続微分可能な写像である．ここで，それぞれ L(E, F )，L(F, G) の元である２つの有界線
形写像を合成し L(E, G) の元である有界線形写像を作り出す写像 B

B : (x, y) ∈ L(E, F ) × L(F, G) 7→ y ◦ x ∈ L(E, G)(11)を導入する．これは以下の命題による．

Listing 14. NDIFF13:38
theorem :: NDIFF13:38
for E,F,G be RealNormSpace
ex B be Lipschitzian BilinearOperator of
R NormSpace of BoundedLinearOperators(E,F),R NormSpace of BoundedLinearOperators(F,G),R NormSpace of BoundedLinearOperators(E,G)
stfor u be Point of R NormSpace of BoundedLinearOperators(E,F),v be Point of R NormSpace of BoundedLinearOperators(F,G)
holds B.(u,v) = v∗u;

この B と前項で述べた命題 NDIFF13:29 による写像(v ′ ◦ u)u′ : x ∈ E 7→ ((v ′ ◦ u)(x), u′ (x)) ∈ L(E, F ) × L(F, G)

を用いれば (10) 式は(v ◦ u)′ (x) = (B ◦ ((v ′ ◦ u)u′ )(x)(12)と書ける. これに前項の命題 NDIFF13:42 を適用すれば，上式の右辺の関数は n 階連続微分可能であり (v ◦ u)′ は n 階連続微分可能である．
最後に前項同様に命題 NDIFF13:33 を適用して，v ◦ u が n + 1 階連続微分可能である
ことが示される．以上で微分の階数に関する帰納法の証明が完成する．

3

陰関数定理の帰納法による証明
微分の階数 n についての帰納法を用いる [1]．n = 1 の場合は 1 章で述べた命題

NDIFF9:21 で証明済みである.

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

9/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

微分の階数 n について定理が成立しているとする．ここで，

f : (x, y) ∈ Z ⊆ E × F 7→ f (x, y) ∈ G
を Z から G への写像で Z 上で n + 1 階連続微分可能とする．また，g を A から B への写像で A に含まれる E の任意の点 x ∈ A についてf (x, g(x)) = c
かつ∂f(x, g(x))∂yが可逆であるとする．f は Z 上で n+1 階連続微分可能であるから，以下の命題 NDIFF13:37
により f の微分は Z 上で n 階連続微分可能である．

Listing 15. NDIFF13:37
theorem :: NDIFF13:37
for S,E be RealNormSpace, Z be Subset of S, u be PartFunc of S,E, i be Nat
st u is diﬀerentiable on i+1,Z & diﬀ(u,i+1,Z) is continuous on Z
holdsu‘|Z is diﬀerentiable on i,Z & diﬀ(u‘|Z,i,Z) is continuous on Z;

したがって，帰納法の仮定から g は n 階連続微分可能であり，A に含まれる E の任意の点 x ∈ A について′(

g (x) =

∂f(x, g(x))
∂y

)−1
◦

∂f
(x, g(x))∂x(13)

が成り立っている．NDIFF13:65 では

for x be Point of E, z be Point of [:E,F:]
st x in A & z = [x,g.x]
holds diff(g,x) = - (Inv partdiff‘2(f,z)) * partdiff‘1(f,z);と記述されている．
ノルム空間 E から E 自身への恒等写像

idE : x ∈ E 7→ x ∈ Eと写像 g を用いて，(4) 式の写像によりノルム空間 E から E と F の直積空間 E × F へ
の写像

idE

g : x ∈ E 7→ (x, g(x)) ∈ E × F(14)を導入する.
次に以下の命題

Listing 16. NDIFF13:66
theorem :: NDIFF13:66
for F,G be non trivial RealBanachSpace
ex I be PartFunc of

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

10/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

R NormSpace of BoundedLinearOperators(F,G),R NormSpace of BoundedLinearOperators(G,F)
st dom I = InvertibleOperators(F,G)& rng I = InvertibleOperators(G,F)& I is one−to−one& I is continuous on InvertibleOperators(F,G)& ( ex J be PartFunc of
R NormSpace of BoundedLinearOperators(G,F),R NormSpace of BoundedLinearOperators(F,G)
st J = I ” & J is one−to−one & dom J = InvertibleOperators(G,F)& rng J = InvertibleOperators(F,G) & J is continuous on InvertibleOperators(G,F) )& ( for u be Point of R NormSpace of BoundedLinearOperators(F,G)
st u in InvertibleOperators(F,G) holds I.u = Inv u )& for n be Nat holds
I is diﬀerentiable on n+1,InvertibleOperators(F,G)& diﬀ(I,n+1,InvertibleOperators(F,G)) is continuous on InvertibleOperators(F,G);を用いて，ノルム空間 E から F への有界線形写像が作る空間 L(E, F ) の元のうち可逆な元の集合を H(E, F )，同様に F から E への可逆な有界線形写像全部の集合を H(F, E) とし H(E, F ) の元 u を H(F, E) の元 u−1 を対応させる写像 I

I : u ∈ H(E, F ) 7→ u−1 ∈ H(F, E)(15)を導入する．この写像 I は任意の階数で連続微分可能である．
この I を用いると，((∂f′g (x) =I◦
◦ (idE
∂y

)

) ((
∂f
g) (x) ◦◦ (idE∂x))g) (x)(16)と書ける．ここで，

(

であり，

(

∂f
◦ (idE∂x∂f◦ (idE∂y)g) (x) ∈ L(E, G)(17))g) (x) ∈ L(F, G)であるから，(∂f◦ (idEI◦∂y)g) (x) ∈ L(G, F )

(18)

である．
さらに有界連続双線形写像

B : (h, k) ∈ L(E, G) × L(G, F ) 7→ k ◦ h ∈ L(E, F )を用いると (16),(17),(18) 式から((∂fg ′ (x) = B
I◦◦ (idE∂y)(∂fg) (x),◦ (idE∂x))g) (x)

(19)

(20)

を得る．
ノルム空間 S, E, F, G と任意の自然数 n について，E × F から G への有界連続双線形写像

B : (x, y) ∈ E × F 7→ B(x, y) ∈ G

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

11/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

および，n 階連続微分可能写像であるようなそれぞれ S から E への写像 u と，S から Fへの写像 v が与えられたとき，これらの写像と S から (4) 式により E × F への写像uv : x ∈ S 7→ (u(x), v(x)) ∈ E × F

を用いて合成される S から F への写像

B ◦ (uv) : x ∈ S 7→ (B ◦ (uv))(x) = B(u(x), v(x)) ∈ F

は前章で述べたように NDIFF13:42 により n 階連続微分可能である．
ここで，(20) を (4) で定義される写像の合成を用いて書き直すと，
(
((
) (
)))
∂f
∂f
g ′ (x) = B ◦I◦◦ (idE g)◦ (idE g)
(x)
∂y
∂x

(21)

となる．

I◦

∂f
◦ (idE
∂y

g)

(22)

は，以下の順に n 階連続微分可能であることが確認できる．
まず，(14) 式で定義される関数 Z

idE

g : x ∈ E 7→ (idg)(x) = (x, g(x)) ∈ E × F

は，恒等写像 idE が任意の階数，したがって n 階連続微分可能であり，g が n 階連続微分可能であるから idE

g も同様に n 階連続微分可能である．

これは以下の命題による．

Listing 17. 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;

次に f は n + 1 階連続微分可能であるから，以下の命題 NDIFF13:52 により ∂f /∂y は

n 階連続微分可能である．
Listing 18. NDIFF13:52
theorem :: NDIFF13:52
for i be Nat, E,F,G be RealNormSpace,
Z be non empty Subset of [:E,F:],f be PartFunc of [:E,F:],G
st f is diﬀerentiable on i+1,Z
holds
f ‘partial‘1| Z is diﬀerentiable on i,Z & f ‘partial‘2| Z is diﬀerentiable on i,Z;

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

12/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

さらに (15) 式で定義される関数 I

I : u ∈ H(E, F ) 7→ u−1 ∈ H(F, E)
は任意の階数で，したがって n 階連続微分可能である．これらの 3 つの写像は何れも n階連続微分可能であるから，前章で述べた 2 つの連続微分可能な写像に合成写像に関する命題 NDIFF13:44 を用いれば (22) 式の写像

I◦∂f
◦ (idE∂yg)

が n 階連続微分可能であることが示される．同様の手順で∂f◦ (idE
∂x

g)

(23)

についても f が n + 1 階連続微分可能であるから命題 NDIFF13:52 により ∂f /∂x はn 階連続微分可能であり，これと写像 idE g が n 階連続微分可能であることから命題
NDIFF13:44 を用いて n 階連続微分可能であることが示される．
以上により，命題 NDIFF13:42 を用いれば (21) 式
) (
(
((
∂f
∂f
g ′ (x) = B ◦I◦◦ (idE g)◦ (idE
∂y
∂x

)))
g)

(x)

の右辺の関数が n + 1 階連続微分可能であること，したがって g ′ が n 階連続微分可能であることが示される．
最後に前章で述べた NDIFF13:33 を適用して，g が n + 1 階連続微分可能であることが示される．以上で微分の階数に関する帰納法の証明が完成する．

4

帰納法による逆関数定理の証明
前章の陰関数定理 [1] の証明と同様の議論を繰り返すが，冗長性を厭わずに記述すれば以下のようになる．

n = 0 の場合は命題 NDIFF10:17 で証明済みである．
微分の階数についての帰納法の仮定により n については定理が成り立つものとする．

E, F をバナハ空間 (RealBanachSpace)，Z を E の開部分集合，
f : x ∈ Z ⊆ E 7→ f (x) ∈ F
を Z から G への写像で Z 上で n + 1 階連続微分可能とする．a, b をそれぞれ E, F の元とし，a は Z に含まれ

f (a) = b′

f (a) が可逆

(24)
(25)

とする．
このとき，f は命題 NDIFF13:37 により Z 上で n 階連続微分可能であるから，f の定義域 Z に含まれる a の開近傍 A と b の開近傍 B 及び B から A の上への写像 g が存在し，

f (A) = B, g(b) = a

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

13/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)を満たす．f の A 上への制限 f |A と g は全単射であり，互いに逆写像になっている．しかも，f |A と g はそれぞれ A,B 上 n 階連続微分可能である．
また B の任意の点 y ∈ B について

f ′ (g(y))
は可逆であり，g ′ (y) = f ′ (g(y))−1(26)

ここで前章で導入した命題 NDIFF13:66 による写像，ノルム空間 E から F への有界線形写像が作る空間 L(E, F ) の元のうち可逆な元の集合を H(E, F )，同様に F から E への可逆な有界線形写像全部の集合を H(F, E) とし H(E, F ) の元 u を H(F, E) の元 u−1 を対応させる写像 I を用いる．

I : u ∈ H(E, F ) 7→ u−1 ∈ H(F, E)(再出)(27)

前章で述べたようにこの写像 I は任意の階数で，したがって n 階連続微分可能である．
この写像 I を用いて (26) 式を書き直すと

g ′ (y) = I(f ′ (g(y))) = (I ◦ f ′ ◦ g)(y)(28)

を得る．上式の右辺の写像

I ◦ f′ ◦ g(29)について前章と同様の議論を行う．上式中の 3 つの写像

I, f ′ , gは何れも n 階連続微分可能であるから，前章で用いた２つの連続微分可能な写像に合成
写像に関する命題 NDIFF13:44 を用いれば (29) 式の写像が n 階連続微分可能であることが示される．したがって (28) 式により g ′ も n 階連続微分可能である．最後に前章同様に

NDIFF13:33 を適用して g が n + 1 階連続微分可能であることが示され，微分の階数に関する帰納法の証明が完成する．

5

まとめ
ノルム空間上の高階微分の陰関数定理及び逆関数定理とそれらの証明の形式化について報告した．筆者らは既にこれ以外に基づいて，ノルム空間上の Taylor 展開や変分法 [1]などの定理と証明を形式化した．さらに，それらの諸定理の準備の上に微分多様体の形式化を開始している．これらについては次回以降に報告する．

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

14/15

Mechanized Mathematics and Its Applications, Works in Progress

Implicit Function Theorem (Nakasho and Shidama)

参考文献[1] Schwartz L. Cours d’analyse. Hermann; 1981.
[2] Nakasho K, Shidama Y. Implicit Function Theorem. Part II. Formalized Mathematics. 2019;27(2):117–131.
[3] Nakasho K, Futa Y. Inverse Function Theorem. Part I. Formalized Mathematics.
2021;29(1):9–19.
[4] Nakasho K, Shidama Y. On Implicit and Inverse Function Theorems on Euclidean
Spaces. Formalized Mathematics. 2022;30(1):165–175.
[5] Shidama Y, Nakasho K. On The Formalizations for Higher Derivatives of Vector
Valued Functions. Mechanized Mathematics and Its Applications, Works in Progress(MMA-WiP). 2022;4(2):1–16. Available from: https://mizar-jp.org/journal/
MMA-WiP/j2022.4.2.

Mizar article information
Works in Progress
NDIFF12 Derivatives of Lipschitzian Bilinear Operators
by Kazuhisa Nakasho and Yasunari Shidama
Summary: In this article, we formalized some fundamentally important theorems for higherorder derivatives of bounded bilinear operators on normed spaces.

NDIFF13 Dif f erentiation of composite f unctions
by Kazuhisa Nakasho and Yasunari Shidama
Summary: In this article, we formalized some fundamentally important theorems for higherorder derivatives of composite functions on norm spaces. Using these theorems, we proved theinverse function theorem for norm-valued functions of normed spaces.

MMA-WiP (2023), vol.5, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.2 - ISSN 2434-5458 (Online)

15/15