〔Major achievements〕Compactness of Neural Networks
Keiichi Miyajima and Hiroshi Yamazaki, Lead
Formalized Mathematics, 21 Dec. 2022, [Reviewed]

〔Major achievements〕Ascoli-Arzela Theorem
Hiroshi Yamazaki; Keiichi Miyajima; Yasunari Shidama, Corresponding, University of Bialystok Institute of Informatics, Bialystok, Poland
Formalized Mathematics, 01 Jul. 2021, [Reviewed]

〔Major achievements〕Functional Space Consisted by Continuous Functions on Topological Space
Hiroshi Yamazaki; Keiichi Miyajima; Yasunari Shidama, Corresponding, University of Bialystok, Institute of Informatics, Bialystok, Poland
Formalized Mathematics, 01 Apr. 2021, [Reviewed]

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, 01 Jan. 2012, [Reviewed]

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, [Reviewed]

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, 01 Jan. 2011, [Reviewed]

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, 01 Jan. 2010, [Reviewed]

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, 01 Jan. 2010, [Reviewed]

Riemann Integral of Functions R into R^n
Keiichi MIYAJIMA; Yasunari SHIDAMA, In this article, we define the Riemann Integral of functions from R into R<
sup>
n<
/sup>
, and prove the linearity of this operator. The presented method is based on [21].
Formalized Mathematics,, 2009, [Reviewed]

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, [Reviewed]

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, [Reviewed]

Behavior Analyses of Phase Boundaries in the Stochastic Mean Curvature Flow by the Level Set Method
Masaaki Ishikawa; Keiichi Miyajima, An influence of a random noise on a mean curvature flow of a phase boundary is investigated. The phase boundary is defined as a curve or a surface separating different physical states such as a water-ice interface. The mean curvature flow is a motion that the phase boundary moves with a normal velocity equals the mean curvature at each point on the phase boundary. Since we consider the influence of the random noise on the mean curvature flow, we need to treat the system formulated by a stochastic level set equation, which is a nonlinear stochastic partial differential equation with a unique solution in the sense of a stochastic viscosity solution. In numerical simulations, sample behaviors of the stochastic mean curvature flows of barbell and torus shapes are studied. It is numerically shown that the sample behaviors of the phase boundary in stochastic mean curvature flows have a possibility of changing topologically by the random noise without any fattening phenomena., ICIC INTERNATIONAL
International Journal of Innovative Computing, Information and Control, Sep. 2005, [Reviewed]

Analyses of Pattern Formation Processes in Stochastic Activator-Inhibitor Systems with Saturation in Growth Domains
Masaaki Ishikawa; Keiichi Miyajima, In the natural world, we often observe many kinds of spatio-temporal patterns such as patterns of animal coat, crystals of snow, etc. An analysis of generation processes of such patterns is very important as a basic problem in various fields of engineering including biological and material engineering. Among many spatio-temporal patterns; we study the pattern formation processes of sea shells from, the viewpoint of biological engineering. As the mathematical model to generate the sea shells patterns, we consider an activator-inhibitor system, which is one of the reaction diffusion systems. Taking into consideration the fact that some kind of disturbance exists to a greater or lesser degree in the natural world, we Propose stochastic activator-inhibitor systems as the mathematical model of pattern formation processes of sea shells. We analyze the influence of the random noise on the shell pattern formations and show that spatio-temporal patterns generated by the proposed model are robust for the random disturbance., ICIC INTERNATIONAL
International Journal of Innovative Computing, Information and Control, Sep. 2005, [Reviewed]

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

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

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

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

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

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

Contracting Mapping and Ordinary Differential Equation Theories　　　　　　　　　　　　　　　
坂本祥崇; 宮島啓一
日本Mizar学会2012年度秋季総会, Oct. 2012, 日本Mizar学会

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

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

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

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

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

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

1変数ベクトル値関数のリーマン積分の形式化　　　　　　　　　　　　　　　
芳賀功治; 宮島啓一
Technical Symposium and General Assembly of Mizar JAPAN, Spring 2008, Jun. 2008, 日本Mizar学会

実ノルム線形空間$R^n$における偏微分についての形式化　　　　　　　　　　　　　　　
宮島啓一; 遠藤登; 師玉康成
Proceedings of the Technical Symposium and General Assembly of Mizar JAPAN, May 2007, 日本Mizar学会

ノルム線形空間の直積空間の形式化表現について　　　　　　　　　　　　　　　
宮島啓一; 遠藤登; 師玉康成
Online Proceedings of the Technical Symposium ,and General Assembly of Mizar JAPAN, Sep. 2006, 日本mizar学会

山口大学工学部

茨城大学工学部

茨城大学工学部