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