• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2005 Fiscal Year Annual Research Report

プルーフチェッカー(Mizar)を用いた数理工学理論の形式化

Research Project

Project/Area Number 16700156
Research InstitutionGifu National College of Technology

Principal Investigator

遠藤 登  岐阜工業高等専門学校, 電子制御工学科, 助教授 (30342497)

Keywords証明の形式化 / ルベーグ積分 / 関数空間
Research Abstract

Mizarシステムにより複素ノルム空間上の一様連続関数の空間について、その定義および各種命題について証明を行った。具体的にはまず実及び複素ノルム空間上の関数の一様連続性とリプシッツ連続性を定義し、一様(またはリプシッツ)連続な関数同士の和等について連続性の各種命題を証明した。さらに複素ノルム空間上の連続関数について、ドメインがコンパクトな場合についても考察し、最後に複素ノルム空間上の縮小写像原理を示した。
また、昨年度の成果である単純関数のルベーグ積分論の拡張として、単純関数のルベーグ積分に対する線形性を取り上げ、これについて証明した。この過程において単純関数のルベーグ積分に関して、昨年度より緩い条件により積分が定義できることを示した。
さらに、n次元実ユークリッド空間として、現在までは距離による空間の定義がなされていたが、今回新たに内積空間としてn次元実ユークリッド空間を再定義し、従来の空間構造との同値性を示すと共にそれらが完備であることを示した。言い換えれば距離による実ユークリッド空間がBanach空間であることを示し、内積による実ユークリッド空間がHilbert空間であることを示した。
上記3つの内容はそれぞれ論文としてFormalized Mathematicsに掲載された。
現在はこれらを元に、n次元ユークリッド空間上のルベーグ測度の定義と(単純関数でない)一般の可測関数について引き続きルベーグ積分論の証明を行っている。

  • Research Products

    (3 results)

All 2005

All Journal Article (3 results)

  • [Journal Article] Uniform Continuity of Functions on Normed Complex Linear Spaces2005

    • Author(s)
      Noboru Endou
    • Journal Title

      Formalized Mathematics 13・1

      Pages: 93-98

  • [Journal Article] Linearity of Lebesgue Integral of Simple Valued Function2005

    • Author(s)
      Noboru Endou, Yasunari Shidama
    • Journal Title

      Formalized Mathematics 13・4

      Pages: 463-466

  • [Journal Article] Completeness of the Real Euclidean Space2005

    • Author(s)
      Noboru Endou, Yasunari Shidama
    • Journal Title

      Formalized Mathematics 13・4

      Pages: 577-581

URL: 

Published: 2007-04-02   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi