Mathematics In Leanから第7章 階層 7.1 基礎を勉強中です。 ここでは代数構造の階層を構成する方法を知ります。目的はその仕組みの概要を知ることで階層を使えるようになることだそうです。なので完全な理解というよりも主要な言葉や考え方などが理解できれ…

前回の記事では普通の証明としてEuclideanDomainには零因子がないことを示しました。こんな感じでした。 $a, b$を零因子、すなわち$a\ne 0, b\ne 0, a * b=0$とします。$a * b = 0$及び$r\; 0\; a$から$r\; (a*b)\; a$。これはmul_left_not_lt a bに矛盾しま…

前回疑問に思ったことはまだ解決していません。なので今回は疑問となぜそう思ったのかだけを書いておきます。 前回までの記事でgaussIntは可換環であることを示しました。またgaussIntにquotientやremainderを定義し除法の原理を示すことでEuclideanDomainと…

$i$を虚数単位とします。つまり$i=\sqrt{-1}$です。このときガウス整数とは$a+b\,i,\, a,b\in\mathbb{Z}$という形をした複素数をガウス整数と呼びます。虚部と実部が整数であるような複素数のことです。例えば$-3i,\, 17+38i$はいずれもガウス整数です。一方…

Mathematics in Lean4 もいよいよ第6章まできました。「6.1 構造の定義」は今までの知識があればとても簡単に読み進むことができました。いわゆるレコード型のような構造およびそのレコード型に付随する関数（演算）、そしてレコード型の各フィールドあるい…

Mathematics in Lean4の数論の章の３つ目のセクションではいよいよ「自然数には素数が無限個ある」ことを形式化して証明します。 証明方法として３つのやり方が説明されています。それぞれの形式化も異なるので下記に記載してみました。 ある自然数nに対して…

有限の場合の総和記号について勉強したことで任意桁数の場合の３の倍数の確認方法について形式化して証明することが出来そうです。ということでやってみました。 まず与えられた自然数が３の倍数かどうかの確認方法と普通の証明をざっと述べてみます。 ３の…

Mathmatics In Lean4の第5章 初等数論の２つ目の話題は帰納法と再帰です。自然数では定義が帰納的であること（自然数型は帰納型であること）を知ります。 inductive Nat | zero : Nat | succ (n : Nat) : Nat この意味は、0はNat型、Nat型の要素を１つとって…

まだ小学生の頃に習ったことで印象に残っているのは３の倍数の確認方法でした。各桁を足した数が３の倍数ならば元の数も３の倍数、というアレです。 倍数とか約数とかがLean4で扱えるようになり、この３の倍数の確認方法の証明を書き下してみようと思いまし…

Mathematics in Lean 4で進めてきているLean4の勉強も第4章となり、初等整数論が扱えるところまで来ました。 最初の節では$\sqrt{2}$が無理数であることを示します。とはいってもこの段階で示すことは$\sqrt{2}$が有理数であるとして矛盾を導くことまでです…

第4章「集合と関数」の最後のセクションはシュレーダー＝ベルンシュタインの定理のLean4による証明です。 初めてこの定理をきちんとした形で知りました。集合論の濃度に関する基本的な定理です。 定理：$\alpha, \beta$を集合、$f:\alpha \rightarrow\beta, …

Mathematics in Leanの第4章「集合と関数」の中の２つ目のセクションである「関数」を読みながら練習問題を解いています。その問題の中で集合族の積集合の写像と集合族の写像の積集合に関する問題がありました。全称量化子と存在量化子が絡み、なかなか手強…

Mathematics in LeanもC04 Sets and Functionsの最初の章である集合まで辿り着きました。ここでは集合に関する性質の証明方法のLean4での実現の仕方を知ります。 集合が等しいこと(A=B)を示す場合、ゴールをA=Bとして方法として、AがBの部分集合であり、かつ…

Lean4での論理記号の取り扱いの勉強も後半です。今回は論理積と論理和の扱いを見ていきます。この辺はあまり難しい話は出てきません。 ゴールが論理積A ∧ Bの形の場合にはconstructorタクティクを使うとAとBが両方ともゴールとなり両方証明するとA ∧ Bの証明…

否定が論理式に含まれているとき使えるタクティクを勉強しました。 introタクティク：ゴールがある命題の否定¬ Aである場合、intro hとすると仮定h: Aが導入されて、ゴールがFalse (矛盾)に変わります。仮定の集まりの中で適当な命題Bについてhb:Bとhbn:¬ B…

現役で最高の数学者のお一人で情報発信にも熱心なテレンスタオ教授のブログがあります。 terrytao.wordpress.com 残念ながら難しすぎて普段はほとんど見ない数学ブログですが、Lean4の勉強をしていたら検索で記事が１つヒットしました！ A slightly longer L…

ゴールに存在量化子が入っている場合、存在量化子がついた変数に値を入ることでゴールの論理式を証明することができます。useタクティクを使うと、「この値を使え」ということができます。例えばこんな感じです。 example : ∃ x : ℝ, 2 < x ∧ x < 3 := by us…

今勉強しているMILの第3章「論理」では仮定の論理式やゴールの論理式に登場する論理記号をタクティクでどのように取り扱えば良いのかを説明しています。 この章の最初の方で説明されるのは全称量化子 ∀ です。ゴールの論理式にこの論理記号がついている場合…

前の記事でcalcモードがわかっていないと書きました。calcは便利そうなのでとりあえず簡単なユースケースを勉強しました。理解できたと思うのでメモを残しておきます。 Quantifiers and Equality - Theorem Proving in Lean 4にある説明を中心にして理解しま…

"Mathematics In Lean"に沿ってLean4の証明支援系の勉強を進めています。まだ基本編で、今やっているのはmin, maxの性質の証明です。具体的には全順序集合上の関数min a b （a, bの小さい方を返す）について次の性質の証明です。 min a (min b c) = min (min…

これからしばらくの間はLean4の証明支援系の勉強の話をシリーズ的に記事にします。相変わらず自分の勉強メモのような感じです。つまづいたところや感動したところを中心に書いていきます。 使用するテキストはMathematics In Lean(通称MIL)にしました。 Math…

年末は帰省していたのですが、有休含めて1/8までお休みにしたこともあり時間ができました。そこでLean 4を勉強してみることにしました。 Lean 4は以前このブログで紹介したLean 3と呼ばれる定理証明支援システムの後継システムです。 Lean 4からは関数型プロ…

有界閉集合では連続関数に最大・最小が存在という良い性質があります。一方、有界であっても開集合の場合にはそのような性質はありませんし、有界でない閉集合にもそのような性質はありません。 ある有界閉集合$S\subset\mathbb{C}$で連続関数列$f_n$が各点…

この記事では複素関数論の応用として代数学の基本定理を証明します。この辺の話は勉強していて興味深い話だったのですが、今回の予定のストーリーからは横道に逸れる感じだったので、補足として今回記事にすることにしました。 リュービルの定理は以前に楕円…

このブログでは過去にリーマンのゼータ関数については色々と取り上げてきました。一方その複素解析的な話はいつもちょっと傍に置いてました。 今回は複素関数論シリーズの最後にリーマンのゼータ関数の複素解析的な部分について基本的な定理を並べていきます…

今回はガンマ関数のガウスによる無限積表示を実解析の範囲で示します。またこれとワイエルストラスによる無限乗積が同値であることを示します。 そしてガンマ関数のワイエルストラスの無限乗積の逆数が整関数であることを紹介します。 ガウスによるガンマ関…

ガンマ関数を正の実数軸から正の右半平面に解析接続する際には、表示式は変わらず、より広い領域での収束と正則性を証明したため、結構面倒でした。 今回はガンマ関数を更に複素平面上の有理型関数に解析接続します。今回はガンマ関数が満たす関数方程式を使…

今回は柳田氏の講義録を参考にしています。とても分かりやすく助かっています。 ガンマ関数の解析接続の定理１：ガンマ関数は複素数平面の右半平面$\mathbb{H}_r=\{s\in\mathbb{C} | Re(s)\gt 0\}$で定義された正則関数に解析接続できる。その表示式は正の実…

ガンマ関数は階乗の一般化で数学のあちらこちらで登場する関数です。階乗は自然数$n$に対して$n!=n\cdot(n-1)\cdot(n-2)\cdots 2\cdot 1$のように定義されます。例えば$3!=3\cdot 2\cdot 1=6$です。 これを正の実数に対して拡張したのがガンマ関数で下記の広…

ガンマ関数やゼータ関数の解析接続や解析的な性質を述べるために必要な複素関数論の定理を述べます。 正則な関数列の定理：関数列$\{f_n\}_{n\in\mathbb{N}}$が開集合$U$上で正則で、$U$の任意の有界閉集合で関数$f$に一様収束する（このとき広義一様収束と…