Maxima で綴る数学の旅

紙と鉛筆の代わりに、数式処理システムMaxima / Macsyma を使って、数学を楽しみましょう

数学

-数学- Lean4のお勉強 シュレーダー=ベルンシュタインの定理

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

-数学- Lean4のお勉強 関数

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

-数学- Lean4のお勉強 集合を扱う

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

-数学- Lean4のお勉強 論理積∧ と 論理和∨

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

-数学- Lean4のお勉強 否定

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

-数学- Lean4のお勉強 タオ教授のブログより

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

-数学- Lean4のお勉強  存在量化子 ∃

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

-数学- Lean4のお勉強  全称量化子 ∀

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

-数学- Lean4のお勉強 calcモード

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

-数学- Lean4のお勉強 証明支援、applyタクティク、have

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

-数学- Lean4のお勉強 証明支援、rw, applyタクティク

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

-数学- Lean4のお勉強 関数型プログラミング

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

-数学- 有界閉集合と一様収束と広義一様収束の復習

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

-数学- 複素関数論 補足 リュービルの定理と代数学の基本定理

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

-数学- 複素関数論(18) リーマンのゼータ関数の解析接続

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

-数学- 複素関数論(17) ガンマ関数の無限乗積と逆数の整関数性

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

-数学- 複素関数論(16) ガンマ関数の複素平面上の有理型関数への解析接続

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

-数学- 複素関数論(15) ガンマ関数の右半平面の正則関数への解析接続

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

-数学- 複素関数論(14) ガンマ関数

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

-数学- 複素関数論(13) 積分で定義された関数の正則性

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

-数学- 複素関数論(12) 有理型関数

ついに有理型関数の定義を理解するところまでやってきました。嬉しいことです。ただその前に有理関数を述べたいと思います。有理関数は複素数係数の多項式の商であるような関数です。$P(z),Q(z)$を複素係数の多項式として$f(z)=\frac{P(z)}{Q(z)}$ならば$f:\…

-数学- 複素関数論(11) 留数定理と積分計算

前回記事で紹介した留数の定義を復習してから留数定理を述べます。 留数の定義:関数$f$のローラン展開を $$f(z)=\sum_{n=0}^{\infty}a_n(z-c)^n + \sum_{n=1}^{\infty}\frac{a_{-n}}{(z-c)^n},\, z\in A(c;R_1,R_2)$$ $$ a_n=\frac1{2\pi\,i}\int_{|z-c|=r}…

-数学- 複素関数論(10) ローラン展開と孤立特異点

円盤領域で正則な関数は冪級数展開ができましたが、円環領域で正則な関数はローラン展開ができます。今回は明治大学の桂田氏の講義資料をベースにこの辺の定義と定理を確認していきます。 円環領域の定義:同じ中心を持つ2つの円盤の間に挟まれた領域を円環…

-数学- 複素関数論(9) 一致の定理と解析接続

ここまでの知識を使って「一致の定理」と「解析接続の定義」を述べることが出来ます。Wikipediaによれば一致の定理には2つの形があると書いてあり、本当にその通りです。解析概論と名古屋大学の柳田さんの講義資料がそれぞれの形で書いてあります。 一致の…

-数学- 複素関数論(8) 一様収束、項別積分、Mテスト

ちょっとだけ寄り道して一様収束関連の話題をまとめておきます。今回は「複素関数」桂田 祐史氏 明治大学を基にして説明していきます。 一様収束は適当な集合上で定義された複素数値関数の列が、その集合上で一様にある関数に収束することを言います。 一様…

-数学- 複素関数論(7) 正則関数の冪級数展開の証明

ある領域で正則な関数は領域内の任意の点で冪級数に展開できることを証明します。証明に必要な設定を含む版で証明を進めます。 定理54(すごく複雑):関数$f$が領域$K$で正則とする。$K$内の任意の点$a\in K$を中心として領域$K$の最も近い境界点を通る円を$K…

-数学- 複素関数論(6) コーシーの積分表示(公式)と正則関数の冪級数展開

コーシーの積分公式を使うことで、正則関数が冪級数に展開できることを示すことができます。今回も主に解析概論を参考にしています。 定理の述べ方が色々あり、なぜそうしているのかを考えてみました。あっているかはわかりませんが、今回はその辺を書いてみ…

-数学- 複素関数論(5) コーシーの積分表示(積分公式)

複素関数論の入り口で最も重要な定理と言われているコーシーの積分表示です。ある領域で正則な関数を積分を使って表示する方法を学びます。今回はその証明まで述べます。重要な応用は次回とします。 コーシーの積分表示(積分公式):単純閉曲線$C$の内部及…

-数学- 複素関数論(4) コーシーの積分定理

いよいよコーシーの積分定理について述べていきます。ここでは主に解析概論の57. コーシーの積分定理、に基づいて記載しています。 前回、原始関数を使った積分計算の定理を紹介しました。この定理から、ある関数の積分の計算は原始関数がある場合はそれを求…

-数学- 複素関数論(3) 複素積分

複素積分の定義をします。今回は特に、 2021年度現代数学基礎CIII 講義ノート 柳田 伸太郎氏 名古屋大学 を参考にしました。 複素積分の定義:$C$を滑らかな曲線として$C$上で定義された関数$f$ について、$f$の積分路$C$上での複素積分$\int_C f(x)dx$を次…