〔主要な業績〕Compactness of Neural Networks
Keiichi Miyajima and Hiroshi Yamazaki, 筆頭著者
Formalized Mathematics, 2022年12月21日, ［査読有り］

〔主要な業績〕Ascoli-Arzela Theorem
Hiroshi Yamazaki; Keiichi Miyajima; Yasunari Shidama, 責任著者, University of Bialystok Institute of Informatics, Bialystok, Poland
Formalized Mathematics, 2021年07月01日, ［査読有り］

〔主要な業績〕Functional Space Consisted by Continuous Functions on Topological Space
Hiroshi Yamazaki; Keiichi Miyajima; Yasunari Shidama, 責任著者, University of Bialystok, Institute of Informatics, Bialystok, Poland
Formalized Mathematics, 2021年04月01日, ［査読有り］

Riemann integral of functions from R into n-dimensional real normed space
Keiichi Miyajima; Artur Korniłowicz; Yasunari Shidama, In this article, we define the Riemann integral on functions R into n-dimensional real normed space and prove the linearity of this operator. As a result, the Riemann integration can be applied to the wider range. Our method refers to the [21].
Formalized Mathematics, 2012年01月01日, ［査読有り］

Contracting mapping on normed linear space
Keiichi Miyajima; Artur Korniłowicz; Yasunari Shidama, In this article, we described the contracting mapping on normed linear space. Furthermore, we applied that mapping to ordinary differential equations on real normed space. Our method is based on the one presented by Schwarz [29]. © 2012 University of Bialystok.
Formalized Mathematics, 2012年, ［査読有り］

Riemann integral of functions from R into real normed space
Keiichi Miyajima; Takahiro Kato; Yasunari Shidama, In this article, we define the Riemann integral on functions from R into real normed space and prove the linearity of this operator. As a result, the Riemann integration can be applied to a wider range of functions. The proof method follows the [16].
Formalized Mathematics, 2011年01月01日, ［査読有り］

The sum and product of finite sequences of complex numbers
Keiichi Miyajima; Takahiro Kato, This article extends the [10]. We define the sum and the product of the sequence of complex numbers, and formalize these theorems. Our method refers to the [11]. © 2010 University of Białystok.
Formalized Mathematics, 2010年01月01日, ［査読有り］

Riemann integral of functions R into C
Keiichi Miyajima; Takahiro Kato; Yasunari Shidama, In this article, we define the Riemann Integral on functions R into C and proof the linearity of this operator. Especially, the Riemann integral of complex functions is constituted by the redefinition about the Riemann sum of complex numbers. Our method refers to the [19]. © 2010 University of Białystok.
Formalized Mathematics, 2010年01月01日, ［査読有り］

Riemann Integral of Functions R into R^n
Keiichi MIYAJIMA; Yasunari SHIDAMA, 1次元実数空間Rからｎ次元実数空間R^nへの関数に対するリーマン積分について、その関連する諸定理を含めて形式化を行った。
Formalized Mathematics,, 2009年, ［査読有り］

Partial differentiation on normed linear spaces Rn
Noboru Endou; Yasunari Shidama; Keiichi Miyajima, Summary. In this article, we define the partial differentiation of functions of real variable and prove the linearity of this operator [18]. © 2007 University of Bialystok.
Formalized Mathematics, 2007年, ［査読有り］

The product space of real normed spaces and its properties
Noboru Endou; Yasunari Shidama; Keiichi Miyajima, In this article, we define the product space of real linear spaces and real normed spaces. We also describe properties of these spaces. © 2007 University of Bialystok.
Formalized Mathematics, 2007年, ［査読有り］

Behavior Analyses of Phase Boundaries in the Stochastic Mean Curvature Flow by the Level Set Method
Masaaki Ishikawa; Keiichi Miyajima, 相境界とは水と氷の境界のように物理的状態が変化する境界のことである。相境界は一般に非平衡状態である。そのために相境界を動く曲面として捉え取り扱わなければならない。相境界と状態の挙動を決定する問題は、自由境界問題と呼ばれ、相境界の挙動は一般に相境界外部からの影響を受ける。しかし、材料科学における金属の焼き鈍しで見られる粒界の運動のように、その挙動が相境界の幾何学的形状のみに依存する場合も存在する。そこで本論文では、相境界の挙動が外部の状態に依存せず、相境界の幾何学的形状(曲率)のみに依存する場合を考察対象に等高面法を用いて相境界の挙動解析を行い粒界の運動を表す平均曲率流をモデル化した。また、実現象における熱揺らぎ等の不規則要素を不規則外乱として確率等高面方程式を提案した。, シミュレーション結果から３次元空間の回転体では外乱によって消滅が遅れる結果を得た。しかし外乱によって回転体に分裂が生じる場合、消滅が早まるという結果を得た。, ICIC INTERNATIONAL
International Journal of Innovative Computing, Information and Control, 2005年09月, ［査読有り］

Analyses of Pattern Formation Processes in Stochastic Activator-Inhibitor Systems with Saturation in Growth Domains
Masaaki Ishikawa; Keiichi Miyajima, パターン形成については多くの研究が成されているが、本論文では特に生命工学の観点から貝殻模様のパターン形成過程について考察した。貝殻模様を生成する数学モデルとして反応拡散方程式の一種である活性－抑制系と呼ばれる偏微分方程式系を採用し、自然界に必ず存在する外乱の影響を考慮した新たな確率活性－抑制系を提案し、外乱の影響について考察した。さらに、一般の化学物質はその化学的制約から飽和値が存在するので、物質の濃度の飽和値も考慮に入れた新たな確率モデルを提案した。そして数値シミュレーションを通じて、外乱と飽和値がパターン形成過程にどのような影響を与えるかを考察した。, その結果、貝殻模様のパターンには、外乱によってパターンは多少乱されるもののパターンの特徴そのものは破壊されないといった、ロバスト性があることが分かった。このことは、自然界にある貝殻は個々の貝殻模様は異なっていても同種の貝殻であればパターンの特徴は変わらないという性質に対応していると考えられる。, ICIC INTERNATIONAL
International Journal of Innovative Computing, Information and Control, 2005年09月, ［査読有り］

有界領域におけるTuringパターンへの不規則外乱の影響解析　　　　　　　　　　　　　　　
石川昌明; 宮島啓一, パターン形成については多くの研究が成されているが、それらは外乱による影響が無視できるという仮定に基づいた確定反応拡散方程式によるモデリングと解析である。しかし、従来の確定モデルでは実際問題では必ず発生する外乱のパターン形成過程への影響を考察することはできない。そこで、本論文では特にTuringパターンと呼ばれる空間パターンを考察対象として、外乱の影響を考慮した確率モデルを提案し、また現実の多くの問題は有界領域で考察されるため、有界領域におけるパターン形成過程への外乱の影響をシミュレーションにより解析した。, その結果、Turingパターンは領域のサイズに依存し、外乱に対してはロバスト性を有することが明らかになった。しかし、外乱の強度によっては波数の変化やパターンの揺らぎが大きくなり、Turing系のロバスト性が失われる場合があることが分かった。
シミュレーション, 2004年06月, ［査読有り］

BZ反応の確率的モデリングと外乱のパターン形成過程への影響　　　　　　　　　　　　　　　
石川昌明; 宮島啓一; 平野雅彦, 今日、パターン形成に関する様々な研究がなされているが、それらの研究で使われているモデルは確定モデルである。しかしながら、実際の状況では不純物の混入や周囲の環境の変化など不確定な外乱が存在し、その外乱がパターン形成過程にどのような影響を及ぼすのか考察する場合には妥当なモデルとはいえない。そこで本論文では、BZ反応について取り上げ、外乱の影響を白色雑音でモデル化したBZ反応の確率モデルを提案し、数値シミュレーションを通じて、パターン形成における外乱の影響を考察した。,シミュレーション結果から、外乱によりパターンに多少の揺らぎは生じるものの、全体的なパターン形成過程への影響は少ないことが分かった。これはBZ反応系が有する興奮性、不応性に起因するものである。
シミュレーション, 2002年09月, ［査読有り］

不規則外乱下の相転移現象のモデリングとシミュレーションによる挙動解析　　　　　　　　　　　　　　　
宮島啓一; 石川昌明, 2成分混合物の相転移は原子間の相互作用力の特性により、相分離と秩序・無秩序転移に分類することができる。相分離過程や秩序・無秩序転移過程において熱揺らぎや物質中の不純物などによる外乱は重要な役割を果たしていると考えられる。また、一般に外乱の時間・空間的変化は不規則であることを考慮して、本論文では外乱の不規則性を空間・時間白色雑音でモデル化し、2成分合金を対象に相分離と秩序・無秩序転移の確率偏微分モデルを提案する。次に提案したモデルを用い、相分離と秩序・無秩序転移における不規則外乱の影響を数値シミュレーションを通して考察した。, シミュレーション結果から、相分離過程においても秩序・無秩序過程においても不規則外乱は相転移を促進する方向に働くことがわかった。特に、秩序・無秩序転移においては外乱による促進効果が相分離よりも顕著であった。このことから、秩序・無秩序転移は相分離よりも外乱の影響を受けやすく、外乱には相分離や秩序化を促進する効果があると思われる。
シミュレーション, 2001年12月, ［査読有り］

A numerical calculation method for optimal control problems having control restrictions and adjustable parameters with constraint　　　　　　　　　　　　　　　
Keiichi Miyajima; Hiroo Yamaura; Dawei Cai; Yasunari Shidama, 本論文では、制御制約と制約付きの調整可能なパラメータのある最適制御問題に対する数値計算法について述べる。調整可能なパラメータとは、例えば電気回路の時定数のような、システム設計時には調整可能であるがシステムが稼働中の時は定数となるパラメータであり、その最適解は未知であるようなものをいう。そして、どのような制御工学上の問題であっても、このパラメータは必要に応じて適当な制御制約を持つ。,本論文では、このパラメータが上界と下界にそれぞれ制御制約を持つ最適制御問題に対して、新たな数値計算アルゴリズムを提案した。このアルゴリズムは連続系におけるDyerの計算法を改良したもので、特に制御制約を持つパラメータを取り扱う点に特徴がある。制御制約に対しては、新たな関数ηを導入し、パラメータの不等式制約をsin関数を用いた等式制約に変換し、この変数は新たなパラメータと見なして計算を行った。最後に３種類の条件下におけるシミュレーションを通じて、このアルゴリズムの有効性を検証した。
Scientiae Mathematicae, 2000年04月

不規則外乱の影響を考慮した秩序化過程のモデリングについて　　　　　　　　　　　　　　　
石川昌明; 宮島啓一; 中津留毅, 相転移現象には多種の成分が混合した一様状態(無秩序状態)からそれぞれの成分に分離する相分離や無秩序状態からある種の構造が形成される秩序・無秩序転移などがあるが、本論文では秩序・無秩序転移を対象にしてモデリングと解析を行った。特に現実の現象には熱雑音や物質中の不純物といった予測不可能な外乱が存在するため、このような不確定要因の影響も考慮した秩序化過程のモデリングおよびシミュレーションによる挙動解析を行った。,シミュレーションにより高温における無秩序状態から原子間の相互力により秩序が形成される過程を明らかにした。シミュレーション結果から、熱雑音などの外乱は秩序化を促進することが判明した。
日本AEM学会論文誌, 2000年01月, ［査読有り］

中心多様体と弱非線形系H∞制御　　　　　　　　　　　　　　　
宮島 啓一; 和崎 克己; 鈴木 彦文; 師玉 康成; 江口 正義, 弱非線形系において、Ｈ∞制御の評価関数の鞍点条件を満たす、弱非線形連立微分方程式の解を安定な中心多様体の内部に閉じこめる十分条件を求めた。これから得られる解は弱非線形系Ｈ∞レギュレータ問題の状態フィードバック解として用いられる。リカッチ行列式の解Ｐを用いることで、状態フィードバック則を得るための十分条件が、中心多様体の議論の結果から導出された。これらは系の非線形関数の有界条件やリプシッツ条件であった。また、これらの条件から非線形項の大きさεと非線形関数のリプシッツ係数及び外乱に対する許容度γに関する不等式を得られた。,そして、簡単な系にてシミュレーションを行い、提案した弱非線形系フィードバックの有効性を確認した。,また、リアプノフ関数を用いて、このフィードバック則によって得られる閉ループ系が内部安定であるか評価した。
電子情報通信学会論文誌, 1999年05月, ［査読有り］

縮小写像と常微分方程式論　　　　　　　　　　　　　　　
坂本祥崇,宮島啓一
日本Mizar学会2012年度秋季総会, 2012年10月, 日本Mizar学会

ノルム線形空間上の縮小写像の形式化　　　　　　　　　　　　　　　
坂本祥崇,宮島啓一
日本Mizar学会2011年度秋季総会, 2011年11月, 日本Mizar学会

実数からｎ次元実ノルム空間への関数に関するリーマン積分と微分の形式化　　　　　　　　　　　　　　　
加藤高広; 宮島啓一
日本Mizar学会2010年度夏季総会, 2010年09月

実数から複素数への関数に関するリーマン積分の形式化　　　　　　　　　　　　　　　
加藤高広; 宮島啓一
日本Mizar学会2009年度秋季総会, 2009年11月

為替レートの統計的解析　　　　　　　　　　　　　　　
堀籠陽; 宮島啓一
電子情報通信学会2009年基礎・境界ソサエティ大会, 2009年09月, 電子情報通信学会

1変数実ベクトル値関数のリーマン積分　　　　　　　　　　　　　　　
加藤高広; 宮島啓一
日本Mizar学会2009年度春季総会, 2009年06月, 日本Mizar学会

為替レートの変化率に対する統計解析　　　　　　　　　　　　　　　
堀籠陽; 宮島啓一; 和田達明
第16回電気学会東京支部茨城支所研究発表会, 2008年12月, 電気学会東京支部茨城支所

1変数ベクトル値関数のリーマン積分の形式化　　　　　　　　　　　　　　　
芳賀功治; 宮島啓一
日本Mizar学会2008年度春季総会, 2008年06月, 日本Mizar学会

実ノルム線形空間$R^n$における偏微分についての形式化　　　　　　　　　　　　　　　
宮島啓一,遠藤登,師玉康成
日本Mizar学会2007年春期総会, 2007年05月, 日本Mizar学会

ノルム線形空間の直積空間の形式化表現について　　　　　　　　　　　　　　　
宮島啓一; 遠藤登; 師玉康成
日本mizar学会2006年秋季総会, 2006年09月, 日本mizar学会

プログラミング　　　　　　　　　　　　　　　
山口大学工学部

微分積分II　　　　　　　　　　　　　　　
茨城大学工学部

アルゴリズムとデータ構造　　　　　　　　　　　　　　　
茨城大学工学部