Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)

Regular Paper

リーマンスティルチェス積分の形式化について
On the Formalizations of Riemann-Stieltjes Integral
師玉 康成 1,*
Yasunari Shidama1,*
1 信州大学工学部, 長野県長野市若里 4-17-1
1 Faculty of Engineering, Shinshu University. 4-17-1 Wakasato, Nagano, Japan* shidama@cs.shinshu-u.ac.jp
Proof checked by Mizar Version: 8.1.08 and MML Version: 5.53.1335
Received: November 27, 2018. Accepted: April 11, 2019.

Abstract
In this paper, the definitions and basic properties of Riemann-Stieltjes integral areformalized in Mizar. In Section 2, we defined bounded variation function, total variation,
and Riemann-Stieltjes integral of real valued function. In Section 3, we proved theorems
about linearity of Riemann-Stieltjes integral. In the last section, the basic existence
theorem of Riemann-Stieltjes integral is formalized. This theorem states that if u is acontinuous function and v is a function of bounded variation in a closed interval of realline, u is Riemann-Stieltjes integrable with respect to v.

1

はじめに
リーマンスティルチェス積分 (Riemann–Stieltjes integral) の形式化について作業経過を報告する．この積分はリーマン積分の一般化である．現在，有界変動関数とリーマン
スティルチェス積分の定義，連続関数の積分可能性定理，区間 [a, b] 上の連続関数全体が作るバナハ空間 C[a, b] の双対空間に関するリースの表現定理などの形式化が進捗している [1] [2] [3]．本稿では，連続関数の積分可能性までの概要を報告する．リーマンスティ
ルチェス積分 (Riemann–Stieltjes integral) はリーマン積分の一般化である．本稿で報告する形式化も定義や定理は微積分の基礎的な文献 [4] [5] [6] などに沿ったものであり，形式化も既になされたリーマン積分の形式化 [7] [8] [9] を基に行っている．閉区間 [a, b] の実数値関数 u, v についてリーマンスティルチェス積分は∫ bu(t)dv(t)(1)

aMMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

1/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)と表されるがこれは，[a, b] の分割 t1 = a < t2 · · · < tn = b を用いたリーマンスティル
チェス和∑u(ck ){v(tk+1 ) − v(tk )},ck ∈ [tk , tk+1 ]

(2)

1≤k<n

について [a, b] の分割幅を無限に小さくする極限操作

max{|tk+1 − tk |, 1 ≤ k < n} → 0(n → ∞)(3)を行った (2) 式の極限値として定義される．

2

積分可能性と積分の定義の形式化
v が有界閉区間 [a, b] 上の有界変動関数であるとは，正数 0 < d が存在して [a, b] の任意の分割 t1 = a < t2 < t3 · · · < tn = b について∑|v(tk+1 ) − v(tk )| ≤ d

(4)

1≤k<n

が成り立つことである．筆者らはこれを，有限列を用いて以下のように形式化した．

Listing 1. INTEGR22:def 1 def 2 def 3
Definition
let A be Subset of REAL;
let v be real−valued Function;
func vol(A,v) −> Real equals:: INTEGR22:def 1
0 if A is empty otherwisev.(upper bound A) − v.(lower bound A);
end;
definition
let A be non empty closed interval Subset of REAL;
let v be real−valued Function;
let t be Division of A;
mode var volume of v,t −> FinSequence of REAL means:: INTEGR22:def 2
len it = len t& for k be Nat st k in dom t holds it.k = |. vol (divset(t,k),v) .|;end;
definition
let A be non empty closed interval Subset of REAL;
let v be Function of A,REAL;
attr v is bounded variation means:: INTEGR22:def 3
ex d be Real st0<d&for t be Division of A, F be var volume of v,tholds Sum(F) <= d;end;(注 1) 以後 INTEGR22, INTEGR23 の形式記述をいくつか提示するが，それらと本稿の記述の対応を判りやすくするため，一部の変数名を本稿の対応するものに書き替えするなどしている．

(注 2) 区間 [a, b] の分割点列 {ti }1≤i≤n について本稿では細分された閉区間は [ti , ti+1 ]を用いるが，これに対応する INTEGER:22,23 では divset(t, i) = [ti−1 , ti ](1 < i ≤MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

2/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)

divset(t, 1) = [a, t1 ] が使われている．i = 1 の場合の例外の記述を逐一書くと∑表現が煩雑になるため本稿では添え字 i を i + 1 としている．同様に総和 1≤i<n Di な∑
ども INTEGER:22,23 では 1<i≤n Di−1 が対応する．
n),

ここで vol(divset(t,k),v) と表現されているものは，既に MML に収録されているリー
マン積分の形式化定義 [7] の流用で [a, b] の任意の分割 t1 = a < t2 < t3 · · · < tn = b についてv(tk+1 ) − v(tk )(5)を表している．また，これを用いた数列{Fk }1≤k<n ,Fk = |v(tk+1 ) − v(tk )|を導入している．[a, b] の分割 t1 = a < t2 < t3 · · · < tn = b 全てについて∑|v(tk+1 ) − v(tk )|

(6)

(7)

1≤k<n

の上限は全変動と呼ばれるが，これを以下のように形式化した．

Listing 2. INTEGR22:def 4
Definition
let A be non empty closed interval Subset of REAL;
let v be Function of A,REAL;
assumev is bounded variation;
func total vd(v) −> Real means:: INTEGR22:def 4
ex VD be non empty Subset of REAL st
VD is bounded above&
VD = { r where r is Real:ex t be Division of A, F be var volume of v,t st
r = Sum(F) }& it = upper bound VD;
end;(2) 式のリーマンスティルチェス和の表現には以下のように有限列を用いた形式化を行った．

Listing 3. INTEGR22:def 5
Definition
let A be non empty closed interval Subset of REAL;
let v be Function of A,REAL;
let u be PartFunc of REAL,REAL;
assumev is bounded variation & dom u = A;
let t be Division of A;
mode middle volume of v,u,t −> FinSequence of REAL means:: INTEGR22:def 5
len it = len t& for k be Nat st k in dom t holds ex r be Real str in rng (u|divset(t,k))& it.k = r∗(vol (divset(t,k),v));
end;

MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

3/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)

関数 u, v について分割された各小区間 [tk , tk+1 ] の元 ck は一意には定まらない．各小区間 [tk , tk+1 ] の u による像の中から適当な元 r を選び（これは ck ∈ [tk , tk+1 ] を一つ選び r = u(ck ) とすることと同じであり），それと v(tk+1 ) − v(tk ) の積を値にもつ実数の有限列を構成し，これを middle volume Sequence of v,u,T という mode で定義した．

divset(t,k) は分割された小区間 [tk , tk+1 ] を表している．
この実数の有限列 middle volume Sequence of v,u,T の和がリーマンスティルチェス
和である．区間 [a, b] の分割数を増して分割幅を無限に小さくしたときの (2) 式の極限を求める手続きを形式化するには分割の無限列を用いる．以下のように無限列を用いた形式化を行った．

Listing 4. INTEGR22:def 6
Definition
let A be non empty closed interval Subset of REAL;
let v be Function of A,REAL;
let u be PartFunc of REAL,REAL;::: assume v is bounded variation & dom u = A;
let T be DivSequence of A;
mode middle volume Sequence of v,u,T −> sequence of (REAL)∗ means:: INTEGR22:def 6
for k be Element of NAT holds it.k is middle volume of v,u,T.k;end;

この middle volume Sequence of v,u,T は区間 [a, b] の分割の無限列

T = {{Tik }1≤i≤nk }k∈N ,T1k = a < T2k < T3k · · · < Tnkk = b(8)が与えられたとき，各 k について，i 番目の値がku(cki ){v(Ti+1) − v(Tik )},kcki ∈ [Tik , Ti+1](9)である実数数列を表している．これも cki の選択が一意に決まらないため mode として定義している．

S を middle volume Sequence of v,u,T とするとき，各 k について実数数列 Sk の和を値にもつ実数数列 middle sum(S) を以下のように定義した．

Listing 5. INTEGR22:def 7
definition
let A be non empty closed interval Subset of REAL;
let v be Function of A,REAL;
let u be PartFunc of REAL,REAL;::: assume v is bounded variation & dom u = A;
let T be DivSequence of A;
let S be middle volume Sequence of v,u,T;
func middle sum(S) −> Real Sequence means:: INTEGR22:def 7
for k be Nat holds it.k = Sum(S.k);end;

MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

4/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)

この実数数列 middle sum(S) の各 k での値は，分割 T k についての u, v のリーマン
スティルチェス和∑ku(cki ){v(Ti+1) − v(Tik )},kcki ∈ [Tik , Ti+1]

(10)1≤i<nkである．
以上のもとに実数値関数 u の関数 v についてのリーマンスティルチェス積分の定義を
以下のように形式化した．u が v についてリーマンスティルチェス積分可能であるとは，
実数 I が存在し，区間 [a, b] の任意の分割の無限列

T = {{Tik }1≤i≤nk }k∈N ,T1k = a < T2k < T3k · · · < Tnkk = b

で lim delta(T) = 0，すなわち
kmax{|Ti+1− Tik |, 1 ≤ i < nk } → 0(k → ∞)(11)を満たすものについて，各 k について分割 T k による小区間の代表元の列 {cki }1≤i<nk
を任意に選んで作られるリーマンスティルチェス和の実数数列 (middle volume Sequence of

v,u,T) が収束し，いずれも I をその収束値にもつことであり，これを述語 u is RiemannStieltjes integrable with v で表現する．さらにこの条件が成り立つとき一意に存在する I を
u の v についてのリーマンスティルチェス積分∫ bu(t)dv(t)(12)

aと定義しこれを u, v を引数のもつ integral(u,v) という Functor で表す．

Listing 6. INTEGR22:def 8 def 9
Definition
let A be non empty closed interval Subset of REAL;
let v be Function of A,REAL;
let u be PartFunc of REAL,REAL;::: assume v is bounded variation & dom u = A;pred u is RiemannStieltjes integrable with v means:: INTEGR22:def 8
ex I be Real st for T being DivSequence of A,
S be middle volume Sequence of v,u,T stdelta(T) is convergent & lim delta(T) = 0 holds
middle sum(S) is convergent & lim (middle sum(S)) = I;
end;definition
let A be non empty closed interval Subset of REAL;
let v be Function of A,REAL;
let u be PartFunc of REAL,REAL;
assume v is bounded variation & dom u = A &u is RiemannStieltjes integrable with v;
func integral(u,v) −> Real means:: INTEGR22:def 9
for T being DivSequence of A,
S be middle volume Sequence of v,u,T stdelta(T) is convergent & lim delta(T) = 0 holds
middle sum(S) is convergent & lim (middle sum(S)) = it;end;

MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

5/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)

積分の線形性

3

この定義をもとに，実数値関数 u の関数 v についてのリーマンスティルチェス積分に関して，関数の加法，スカラ倍に関しての積分の線形性について以下の命題の形式化と証明を行った．例えば実数値関数 u, w が v についてリーマンスティルチェス積分可能とするとき，前節のT = {{Tik }1≤i≤nk }k∈N ,T1k = a < T2k < T3k · · · < Tnkk = b

で lim delta(T) = 0 すなわち (11) 式
kmax{|Ti+1− Tik |, 1 ≤ i < nk } → 0 (k → ∞)を満たすものについて，関数の和 u + w に関して各 k 番目の項がリーマンスティルチェス和∑k(u + ｗ)(cki ){v(Ti+1) − v(Tik )},kcki ∈ [Tik , Ti+1]

(13)

1≤i<nkになる実数列を作れば，それぞれ各 k 番目の項が∑ku(cki ){v(Ti+1) − v(Tik )},1≤i<nk∑kw(cki ){v(Ti+1) − v(Tik )},kcki ∈ [Tik , Ti+1
] (14)

1≤i<nkである実数列が作れる．(11) 式，すなわち lim delta(T) = 0 が成り立っているため，また u, w が v についてリーマンスティルチェス積分可能であることから，(14) の 2 つの級
数は k → ∞ とするとき収束する．

∑

k(u + ｗ)(cki ){v(Ti+1) − v(Tik )}=1≤i<nk∑ku(cki ){v(Ti+1) − v(Tik )}1≤i<nk+∑kw(cki ){v(Ti+1) − v(Tik )}(15)

1≤i<nkが成り立っているから，(14) の収束性により (15) 式の両辺の級数は k → ∞ とするとき
収束し，その極限は∫ b∫ b(u + w)(t)dv(t) =a∫ bu(t)dv(t) +aw(t)dv(t)aとなる（本稿の形式化では integral(u+w,v) = integral(u,v) + integral(w,v) と表される）．
以下同様の議論により以下の命題群を形式化した．

Listing 7. INTEGR22:7∼17
begin :: Linearity of Riemann−Stieltjes Integral
theorem :: INTEGR22:7
for A be non empty closed interval Subset of REAL,r be Real,v be Function of A,REAL,u,w be PartFunc of REAL,REAL stv is bounded variation & dom u = A & dom w = A &w = r(#)u & u is RiemannStieltjes integrable with v holds
w is RiemannStieltjes integrable with v &MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

6/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)

integral(w,v) = r ∗ integral(u,v);
theorem :: INTEGR22:9
for A be non empty closed interval Subset of REAL,v be Function of A,REAL,
u,s,w be PartFunc of REAL,REAL stv is bounded variation & dom u = A & dom v = A & dom s = A &w = u + s & u is RiemannStieltjes integrable with v &v is RiemannStieltjes integrable with v holdss is RiemannStieltjes integrable with v &integral(w,v) = integral(u,v) + integral(s,v);
theorem :: INTEGR22:12
for A be non empty closed interval Subset of REAL,r be Real, v,v1 be Function of A,REAL,
u be PartFunc of REAL,REAL stv is bounded variation & v1 is bounded variation & dom u = A &v = r(#)v1 & u is RiemannStieltjes integrable with v1 holds
u is RiemannStieltjes integrable with v &integral(u,v) = r ∗ integral(u,v1);
theorem :: INTEGR22:15
for A be non empty closed interval Subset of REAL,
v,v1,v2 be Function of A,REAL,
u be PartFunc of REAL,REAL stv is bounded variation & v1 is bounded variation &v2 is bounded variation & dom u = A &v = v1 + v2 & u is RiemannStieltjes integrable with v1 &u is RiemannStieltjes integrable with v2
holds
u is RiemannStieltjes integrable with v &integral(u,v) = integral(u,v1) + integral(u,v2);

なお，上記記述で v が有界変動であるという条件 v is bounded variation は不要であり，現在，MML への修正削除版を準備中である．近々削除される予定である．

4連続関数の積分可能性
閉区間上の連続な実数値関数 u と有界変動関数 v についてはリーマンスティルチェス

積分可能である．これは以下のように形式化した．

Listing 8. INTEGR23:21
theorem :: INTEGR23:21
for A be non empty closed interval Subset of REAL,v be Function of A,REAL,
u be continuous PartFunc of REAL,REAL stv is bounded variation & dom u = A
holds u is RiemannStieltjes integrable with v;

この証明には，実数 I が存在し，区間 [a, b] の任意の分割の無限列

T = {{Tik }1≤i≤nk }k∈N ,T1k = a < T2k < T3k · · · < Tnkk = b

で lim delta(T) = 0 すなわち
kmax{|Ti+1− Tik |, 1 ≤ i < nk } → 0(k → ∞)

MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

7/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)

を満たすものについて，各 k について分割 T k による小区間の代表元の列 {cki }1≤i<nk を任意に選んで作られるリーマンスティルチェス和の実数数列 middle volume Sequence ofv,u,T{Sk }k∈N ,

∑

Sk =

k
u(cki ){v(Ti+1) − v(Tik )},kcki ∈ [Tik , Ti+1]

(16)

1≤i<nkが収束し，その極限が I と一致することを示す必要がある．u は有界閉区間 [a, b] 上の連続関数だから一様連続である．

v は有界変動関数であるから任意の k について∑k|v(Ti+1) − v(Tik )| ≤ total vd(v)(17)

1≤i<nkが成り立っている．0 < ϵ を任意の正の実数とするとき，関数 u の [a, b] 上の一様連続性から，ある正数 0 < δ が存在し，任意の実数 t1 , t2 ∈ [a, b] について

|t1 − t2 | < δ|u(t1 ) − u(t2 )| < ϵ/(total vd(v) + 1)

ならば

(18)

が成り立っている．一方，lim delta(T) = 0 が成り立っているから自然数 m が存在し，m ≤ k である任意の自然数 k についてkmax{|Ti+1− Tik |, 1 ≤ i < nk } < δ(19)が成り立っている．
ここで m ≤ k である任意の自然数 k について (18), (19) 式から｜Sk − Sm｜< ϵが成り立っていることを示せば，リーマンスティルチェス和の列 {Sk }k∈N がコーシー列になることから，実数空間の完備性により {Sk }k∈N は収束することが証明できる．
しかしながらSk − Sm=∑∑ku(cki ){v(Ti+1) − v(Tik )} −1≤i<nkmmu(cmj ){v(Tj+1 ) − v(Tj )}1≤j<nmの評価はそれ程容易ではない．区間分割数 nk と nm が等しいとは限らないし，i = jkm], [Tjm , Tj+1
] やそれらの代表元 cki , cm
であっても，それぞれの区間 [Tik , Ti+1
j が同じであるとは限らない．第 2 節で述べた表記方法を用いるとdivset(T k , i)kvol(divset(T k , i), v) = v(Ti+1) − v(Tik )k= [Tik , Ti+1],mvol(divset(T m , j), v) = v(Tj+1) − v(Tjm )mdivset(T m , j) = [Tjm , Tj+1],

であり，Sk , Sm はそれぞれ

Sk

=

∑

u(cki )vol(divset(T k , i), v)

(20)

m
u(cm
j )vol(divset(T , j), v)(21)

1≤i<nkSm=∑1≤j<nm

MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

8/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)と書ける．ここで∪[a, b] =∪m]=[Tjm , Tj+1

divset(T m , j)1≤j<nm1≤j<nmから

divset(T k , i) = divset(T k , i) ∩ [a, b]==

divset(T k , i) ∩ {∪∪divset(T m , j)}1≤j<nm{divset(T k , i) ∩ divset(T m , j)} (22)1≤j<nmであり∑vol(divset(T k , i), v) =vol(divset(T k , i) ∩ divset(T m , j), v)(23)

vol(divset(T k , i) ∩ divset(T m , j), v)(24)

1≤j<nm

全く同様にして∑vol(divset(T m , j), v) =i≤i<nkを得る．
km
ここで区間 [Tik , Ti+1
] と [Tjm , Tj+1
] が共通部分をもたないか，あるいは端点一点のみを共有する場合には

vol(divset(T k , i) ∩ divset(T m , j), v) = 0kmであり，[Tik , Ti+1
] と [Tjm , Tj+1
] が共通部分を持つ場合は (18), (19) 式から|u(cki ) − u(cmj )| < ϵ/(total vd(v) + 1)(25)が従う．以下の補題 INTEGR22:2

Listing 9. INTEGR22:2
theorem :: INTEGR22:2
for n,m be Nat, a be Function of [:Seg n,Seg m:],REAL
for p,q be FinSequence of REAL st( dom p = Seg n& for i be Nat st i in dom p holds
ex r be FinSequence of REAL st(dom r = Seg m & p.i = Sum r& for j be Nat st j in dom r holds r.j=a.(i,j) ) )& ( dom q = Seg m& for j be Nat st j in dom q holds
ex s be FinSequence of REAL st(dom s = Seg n & q.j = Sum s& for i be Nat st i in dom s holds s.i=a.(i,j) ) )holds Sum p = Sum q;を用いれば総和∑1≤j<nm と∑1≤i<nk の順序を変えることができ，(20), (21), (23), (24)式からSk − Sm =

∑

∑

k
m
(u(cki ) − u(cmj ))vol(divset(T , i) ∩ divset(T , j), v)(26)

1≤i<nk 1≤j<nm

MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

9/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)

である．また，∑∑|vol(divset(T k , i) ∩ divset(T m , j), v)| ≤ total vd(v)1≤i<nk 1≤j<nmである．この評価式と (26), (25) 式から目的の|Sk −Sm | ≤∑ϵ/(total vd(v)+1)∑|vol(divset(T k , i)∩divset(T m , j), v)| < ϵ1≤i<nk 1≤j<nmを得る．これらは下記のように補題として書かれている．

Listing 10. INTEGR23:17 INTEGR23:18
theorem :: INTEGR23:17
for A be non empty closed interval Subset of REAL,
rho be Function of A,REAL,
T,S be Division of A
st rho is bounded variation holds
ex ST be FinSequence of REAL
st len ST = len S& Sum ST <= total vd(rho)& for j be Nat st j in dom S holds
ex p be FinSequence of REAL
st ST.j = Sum p& len p = len T& for i be Nat st i in dom T holds
p.i = |. vol(divset(T,i) /\ divset(S,j),rho) .|;theorem :: INTEGR23:18
for A be non empty closed interval Subset of REAL,
rho be Function of A,REAL,
u be PartFunc of REAL,REAL
st rho is bounded variation& dom u = A& u|A is uniformly continuous
holds
for T being DivSequence of A, S be middle volume Sequence of rho,u,T
st delta T is convergent & lim delta T = 0
holds middle sum(S) is convergent;

証明の詳細は http://www.mizar.org/version/current/html/integr23.html に公開されている．証明記述の殆どが，有限列と無限列の構成と，それらに関する手続きの正当性を示すための数学的帰納法によって占められている．
次に，この極限値が lim delta(T) = 0 を満たす区間 [a, b] の分割と分割された各小区間の代表元の選び方に依存しないで，一意に決まることを示す．それぞれ lim delta(P) =0, lim delta(Q) = 0 を満たす区間 [a, b] の分割の無限列 {P k }k∈N , {Qk }k∈N
P1k = a < P2k < P3k · · · < Pnkk = b, Qk1 = a < Qk2 < Qk3 · · · < Qkｍk = b(27)と分割される小区間の代表元の列{{dki }1≤i<nk }k∈N ,kdki ∈ [Pik , Pi+1
] (1 ≤ i < nk ){{eki }1≤i<mk }k∈N ,eki ∈ [Qki , Qki+1 ](1 ≤ i < mk )MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

(28)

10/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)

が任意に与えられたとする．これによるリーマンスティルチェス和の列

Uk =

∑

k
u(dki ){v(Pi+1) − v(Pik )},

∑

Wk =

u(eki ){v(Qki+1 ) − v(Qki )}(29)

1≤i<mk1≤i<nkは前述のようにコーシー列になることから収束する．証明するべきことは

lim Uk = lim Wk

k→∞

k→∞

である．上の分割の無限列から分割の無限列 {T k }k∈N を

T 2k = P k ,T 2k+1 = Qk

(30)として構成すると，lim delta(T) = 0 を満たしている．さらにこの {T k }k∈N により分割された各小区間の代表元の列 {{cki }1≤i<lk }k∈N を以下のように作る(1 ≤ i < l2k ) l2k = nkic2ki = dk

c2k+1
= eik
i

(1 ≤ i < l2k+1 ) l2k+1 = mk

(31)

これらから作られるリーマンスティルチェス和の列{Sk }k∈N ,

Sk =

∑

k
u(cki ){v(Ti+1) − v(Tik )}(32)

1≤i<lkを作ると，前述のとおり {Sk }k∈N はコーシー列であるため収束する．さらに分割の無限列{P k }k∈N , {Qk }k∈N と分割される小区間の代表元の列 {{dki }1≤i<nk }k∈N , {{eki }1≤i<mk }k∈Nから作られる (29) 式のリーマンスティルチェス和の列は

S2k = Uk ,S2k+1 ＝ Wkとなるので {Sk }k∈N の部分列である．収束列 {Sk }k∈N の部分列 {Uk }k∈N , {Wk }k∈N の
極限はいずれも {Sk }k∈N の極限と一致する．
以下はこの証明に使用された補題の形式化の一部である．

Listing 11. INTEGR23:21

INTEGR23:22( excerpt )theorem Th21:
for A be non empty closed interval Subset of REAL,v be Function of A,REAL,
u be PartFunc of REAL,REAL,
T0,T,T1 be DivSequence of A,
S0 be middle volume Sequence of v,u,T0,
S be middle volume Sequence of v,u,T
st for i be Nat holds T1.(2∗i) = T0.i & T1.(2∗i+1) = T.i
ex S1 be middle volume Sequence of v,u,T1
st for i be Nat holds S1.(2∗i) = S0.i & S1.(2∗i+1) = S.i
theorem Th22:
for Sq0,Sq,Sq1 be Real Sequence
st Sq1 is convergent& for i be Nat holds Sq1.(2∗i) = Sq0.i & Sq1.(2∗i+1) = Sq.i holds
Sq0 is convergent & lim Sq0 = lim Sq1& Sq is convergent & lim Sq = lim Sq1

MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

11/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)

以上が形式化証明の概要であるが，区間の無限分割に関する議論で，分割，結合，再分割の操作などで読者の直観に訴えるような方法は厳密な形式化証明では許容されない．
有限回, 無限回の操作に対応した，有限列，無限列 [10] [11] の構成が必要になる．繰り返し操作の正当性は数学的帰納法 [12] によっている．

5

終わりに
本稿ではリーマンスティルチェス積分 (Riemann–Stieltjes integral) の形式化について

作業経過を報告した. 有界変動関数とリーマンスティルチェス積分の定義，連続関数の積
分可能性定理の形式化の状況を解説した．区間 [a, b] 上の連続関数全体が作るバナハ空間

C[a, b] の双対空間に関するリースの表現定理などの形式化が進捗しているが，これについては次回に報告する．

参考文献[1] Narita K, Nakasho K, Shidama Y. Riemann-Stieltjes Integral. Formalized Mathematics. 2016;24(3):199–204.
[2] Nakasho K, Narita K, Shidama Y. The Basic Existence Theorem of RiemannStieltjes Integral. Formalized Mathematics. 2016;24(4):253–259.
[3] Narita K, Nakasho K, Shidama Y. F. Riesz Theorem. Formalized Mathematics.
2017;25(3):179–184.
[4] Gupta SL, Rani N. Fundamental Real Analysis. Vikas Pub.; 1986.
[5] Kestelman H. Methods in classical and functional analysis. Addison-Wesley Publishing Co.; 1960.
[6] Stroock DW. A Concise Introduction to the Theory of Integration. Springer Scienceand Business Media; 1999.
[7] Endou N, Kornilowicz A. The Definition of the Riemann Definite Integral andsome Related Lemmas. Formalized Mathematics. 1999;8(1):93–102. Available from:http://fm.mizar.org/1999-8/pdf8-1/integra1.pdf.
[8] Endou N, Wasaki K, Shidama Y. Darboux’s Theorem. Formalized Mathematics. 2001;9(1):197–200. Available from: http://fm.mizar.org/2001-9/pdf9-1/
integra3.pdf.
[9] Miyajima K, Shidama Y. Riemann Integral of Functions from R into R\ . Formalized Mathematics. 2009;17(2):179–185.
[10] Bancerek G, Hryniewiecki K. Segments of Natural Numbers and Finite Sequences.
Formalized Mathematics. 1990;1(1):107–114. Available from: http://fm.mizar.
org/1990-1/pdf1-1/finseq_1.pdf.

MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

12/13

Mechanized Mathematics and Its Applications, Works in Progress

Riemann-Stieltjes Integral (Shidama Y.)[11] Kotowicz J. Real Sequences and Basic Operations on Them. Formalized Mathematics. 1990;1(2):269–272. Available from: http://fm.mizar.org/1990-1/pdf1-2/
seq_1.pdf.
[12] Bancerek G. The Fundamental Properties of Natural Numbers. Formalized Mathematics. 1990;1(1):41–46. Available from: http://fm.mizar.org/1990-1/pdf1-1/
nat_1.pdf.

Mizar article information
Works in Progress
INTEGR22 Riemann-Stieltjes Integral
by Keiko Narita, Kazuhisa Nakasho, and Yasunari Shidama
INTEGR23 The Basic Existence Theorem of Riemann-Stieltjes Integral
by Kazuhisa Nakasho, Keiko Narita, and Yasunari Shidama
DUALSP05

F. Riesz Theoremby Keiko Narita, Kazuhisa Nakasho, and Yasunari Shidama

MMA-WiP (2019), vol.1, no.2 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.2 - ISSN 2434-5458 (Online)

13/13