フタ ユウイチ   Futa Yuichi
  布田 裕一
   所属   コンピュータサイエンス学部 コンピュータサイエンス学科
   職種   教授
言語種別 英語
発行・発表の年月 2018/12
形態種別 学術論文
査読 査読あり
標題 Continuity of Bounded Linear Operators on Normed Linear Spaces
執筆形態 共著
掲載誌名 Formalized Mathematics
掲載区分国外
出版社・発行元 De Gruyter
巻・号・頁 26(3),pp.231-237
著者・共著者 Kazuhisa Nakasho, Yuichi Futa and Yasunari Shidama
概要 An analysis attack with distributions is one of attacks against cipher schemes. The attack need mathematical tools such as implicit functions and their properties. On the other hand, formalization has become important for security evaluation against the attack. In this paper, we formalize properties of bounded linear operators on normed linear spaces in the formal proof verification system Mizar.