Mathematics in Lean4の数論の章の3つ目のセクションではいよいよ「自然数には素数が無限個ある」ことを形式化して証明します。 証明方法として3つのやり方が説明されています。それぞれの形式化も異なるので下記に記載してみました。 ある自然数nに対して必ずnよりも大きな素数が存在する（作れる）ことを示す。theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by... 素数が有限個しかないとして、それらの積に1を足した数を考えるとその素因数が元の素数の集合に含まれることから矛盾を導く（ユークリッド）。theorem primes…
有限の場合の総和記号について勉強したことで任意桁数の場合の3の倍数の確認方法について形式化して証明することが出来そうです。ということでやってみました。 まず与えられた自然数が3の倍数かどうかの確認方法と普通の証明をざっと述べてみます。 3の倍数の確認方法：$N, i, a_i$を自然数として$a_i$は各桁の数を表します。従って$\sum_{i=0}^{N-1} a_i\cdot 10^i$が与えられた自然数です。確認方法は、$$3 \sum_{i=0}^{N-1} a_i\cdot 10^i \iff 3 \sum_{i=0}^{N-1} a_i$$が成り立つので、右辺の和（各桁の数…
Mathmatics In Lean4の第5章 初等数論の2つ目の話題は帰納法と再帰です。自然数では定義が帰納的であること（自然数型は帰納型であること）を知ります。 inductive Nat zero : Nat succ (n : Nat) : Nat この意味は、0はNat型、Nat型の要素を1つとってnとするとsucc nもNat型です。そしてsucc n=0となるようなnはありません。ちなみにsucc nはn+1とも書かれます。 次にこの型の上で階乗関数を再帰的に定義します。 def fac : ℕ → ℕ 0 => 1 n + 1 => (n + 1) * fac …
まだ小学生の頃に習ったことで印象に残っているのは3の倍数の確認方法でした。各桁を足した数が3の倍数ならば元の数も3の倍数、というアレです。 倍数とか約数とかがLean4で扱えるようになり、この3の倍数の確認方法の証明を書き下してみようと思いました。自分で定理を形式化して証明を与えることを一通りやるには良いのではないかと思ったのです。 任意桁数の3の倍数で証明しようとすると、その数の10進数展開がk桁あるとして各桁を$a_n$とすると$\sum_{n=0}^{k-1} a_n\,10^n$と表すことができるところから始める必要があります。まだ$\sum$記号を勉強していないこともあり、えいやで3…
-数学- Lean4のお勉強 $\sqrt{2}$が無理数であること
Mathematics in Lean 4で進めてきているLean4の勉強も第4章となり、初等整数論が扱えるところまで来ました。 最初の節では$\sqrt{2}$が無理数であることを示します。とはいってもこの段階で示すことは$\sqrt{2}$が有理数であるとして矛盾を導くことまでです。$\sqrt{2}$が実数の中に存在することまで示すわけではありません。 証明は古代ギリシャから知られているものです。$\sqrt{2}=\frac{m}{n}$となる互いに素な自然数$m,n$が存在するとします。すると $$m^2=2\,n^2$$ です。ここから$m$が偶数であることがわかります。$m=2\…
-数学- Lean4のお勉強 シュレーダー＝ベルンシュタインの定理
第4章「集合と関数」の最後のセクションはシュレーダー＝ベルンシュタインの定理のLean4による証明です。 初めてこの定理をきちんとした形で知りました。集合論の濃度に関する基本的な定理です。 定理：$\alpha, \beta$を集合、$f:\alpha \rightarrow\beta, g:\beta\rightarrow\alpha$が両方とも単射である時、$\alpha$から$\beta$への全単射がある。 集合の濃度に関して$ \alpha \ge \beta , \beta \ge \alpha $のとき$ \alpha = \beta $が成り立つということで確かに基本的です…
Mathematics in Leanの第4章「集合と関数」の中の2つ目のセクションである「関数」を読みながら練習問題を解いています。その問題の中で集合族の積集合の写像と集合族の写像の積集合に関する問題がありました。全称量化子と存在量化子が絡み、なかなか手強かったので、紹介したいと思います。 練習問題とその証明は下記のとおりです。 example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i := by01 intro y h102 simp at h103 simp04 have : (∃ x, (∀ (j : …
-その他- macOSとbluetooth イヤフォンの現状と音質の改善方法
しばらく前のmacOSではbluetoothイヤフォンで音楽を楽しむ際、コーデック選択の問題で音質が悪い状況がありました。私もiMacとソニーのWF-1000MX4 の組み合わせでこの辺について色々と試してきています。 最近知ったのですが、この状況は少なくともmacOS Sonomaでは大きく改善された面もあり改善されていない面もあります。 以前のmacOSではbluetoothイヤフォンの(正確にはA2DPプロファイルで使う)デフォルトのコーデックがSBCでした。このためたとえイヤフォンがAACをサポートしていてもSBCで繋がってしまい、音が悪い、ということが発生していました。よく知られた改…
Mathematics in LeanもC04 Sets and Functionsの最初の章である集合まで辿り着きました。ここでは集合に関する性質の証明方法のLean4での実現の仕方を知ります。 集合が等しいこと(A=B)を示す場合、ゴールをA=Bとして方法として、AがBの部分集合であり、かつBがAの部分集合であることを示すこと AがBの部分集合であることを示すにはAの任意の要素がBの要素であることを示すこと 空集合と全体集合の性質 和集合と積集合をメンバーシップの論理和と論理積 集合族の積集合と和集合 のようなことがここでは解説されています。ここでは上記の初めの2つについて簡単な命題を示し…
Lean4を証明支援系として使っていても、型と証明の対応や関数型言語が突然現れることがあります。このことを知っていないと証明が読めないことがありました。 具体的には例えばある定理がこんな形だったとします。 def P (x:ℕ) : Prop := sorrytheorem theoA : ∀ x > 3, P x := sorry P xを命題としてxが3より大きい場合はP xが成り立つ、というのがtheoAという定理です。 当然P 4は4>3なので成り立つはずです。証明は普通はこんなふうにやると思うのです。 example : P 4 := by apply theoA -- ⊢ 4 > …
Lean4での論理記号の取り扱いの勉強も後半です。今回は論理積と論理和の扱いを見ていきます。この辺はあまり難しい話は出てきません。 ゴールが論理積A ∧ Bの形の場合にはconstructorタクティクを使うとAとBが両方ともゴールとなり両方証明するとA ∧ Bの証明が終わります。 仮定にh:A ∧ Bがある場合には仮定としてAとBが成り立つのですからバラしてそれぞれを仮定としたいですよね。仮定にh1:Aとh2:Bを入れるにはrcases h with <h1,h2>とかhave <h1,h2>:=hなどとすれば良いです。 ゴールが論理和A∨ Bの形の場合にはAかBのどちらかを証明できれば良い…
否定が論理式に含まれているとき使えるタクティクを勉強しました。 introタクティク：ゴールがある命題の否定¬ Aである場合、intro hとすると仮定h: Aが導入されて、ゴールがFalse (矛盾)に変わります。仮定の集まりの中で適当な命題Bについてhb:Bとhbn:¬ Bを両方含むようにできれば最後にapply hb hbnで矛盾を導いて証明が終わります。 by_contraタクティク：ゴールが特に否定の形ではない場合でも、by_contra hとすることでゴールの否定を仮定hとして導入するとともに、ゴールをFlase(矛盾)にすることができます。仮定の中で矛盾を導くことで証明を終了させ…
現役で最高の数学者のお一人で情報発信にも熱心なテレンスタオ教授のブログがあります。 terrytao.wordpress.com 残念ながら難しすぎて普段はほとんど見ない数学ブログですが、Lean4の勉強をしていたら検索で記事が1つヒットしました！ A slightly longer Lean 4 proof tour What's new 実数の2つの無限数列に関するある補題の証明をLean4を使って形式化して確認する、というものです。証明自体は望遠鏡和(telescoping sum)という手法を使ったものです。有限和をうまく作ると、実は隣り合った項が打ち消しあって最初と最後の項だけが…
ゴールに存在量化子が入っている場合、存在量化子がついた変数に値を入ることでゴールの論理式を証明することができます。useタクティクを使うと、「この値を使え」ということができます。例えばこんな感じです。 example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 -- ⊢ 2 < 5 / 2 ∧ 5 / 2 < 3 norm_num -- No goals ゴールの論理式の意味は「2より大きくて3より小さい実数xが存在する」です。まあ当たり前ですがどうやって証明するかです。この場合xが$\frac{5}{2}$であればこの不等式は確かに成立するので、xが存在…
今勉強しているMILの第3章「論理」では仮定の論理式やゴールの論理式に登場する論理記号をタクティクでどのように取り扱えば良いのかを説明しています。 この章の最初の方で説明されるのは全称量化子 ∀ です。ゴールの論理式にこの論理記号がついている場合、その変数や中身の式を証明することができません。そこで多くの場合には全称量化子 ∀を外してその中身にアクセスできるようにすることが証明の第一歩となります。 全称量化子 ∀がゴールの論理式に登場している場合、introタクティクを使うとその変数がラベル付きで導入されて、以降の証明で使えるようになります。 例えば前回見たcalcモードの説明の記事では偶関数…
前の記事でcalcモードがわかっていないと書きました。calcは便利そうなのでとりあえず簡単なユースケースを勉強しました。理解できたと思うのでメモを残しておきます。 Quantifiers and Equality - Theorem Proving in Lean 4にある説明を中心にして理解しました。最も典型的なユースケースは等式A=Bを証明する場合です。式Aから始めてタクティクを使って変形し、式Bを導ければ等式証明が成功します。等式変形なので使うタクティクはrwで、仮定や既知の定理を使って式変形します。 現在勉強中の第3章「論理」の中ので分かり易い例があったので紹介します。偶関数と奇関数…
数学の記事では普通は環境について書かないのですが、Lean4はプログラミング環境でもあるし、一応概要を記しておきます。 パソコン：M1 iMac (主記憶16GB), macOS 14.2.1 Lean (version 4.5.0-rc1) VS Code バージョン1.85.1 VS Code機能拡張Lean4 v0.0.124 起動中のVSCodeの様子はこんな感じです。縦分割の左から、フォルダ階層、Mathematics In Lean、練習ファイル、証明ゴール が表示されています。 MILの「2章 基本」の最後の練習問題である「距離関数は常にゼロ以上」の証明が終わったところが練習ファ…
-数学- Lean4のお勉強 証明支援、applyタクティク、have
"Mathematics In Lean"に沿ってLean4の証明支援系の勉強を進めています。まだ基本編で、今やっているのはmin, maxの性質の証明です。具体的には全順序集合上の関数min a b （a, bの小さい方を返す）について次の性質の証明です。 min a (min b c) = min (min a b) c 直感的には結局両辺ともa,b,cのうち最小の値を返しますから等しくなるのは納得です。一方この学習では以下の4つの性質だけから上記の性質を示すことが課題です。 le_antisymm : a $\le$ b $\land$ b $\le$ a $\iff$ a=b min_…
-数学- Lean4のお勉強 証明支援、rw, applyタクティク
これからしばらくの間はLean4の証明支援系の勉強の話をシリーズ的に記事にします。相変わらず自分の勉強メモのような感じです。つまづいたところや感動したところを中心に書いていきます。 使用するテキストはMathematics In Lean(通称MIL)にしました。 Mathematics in Lean — Mathematics in Lean 0.1 documentation もう1つ、"Theorem Proving In Lean4"(通称TPIL)というテキストもありそちらは有志の皆様による日本語版もあります。両者の最大の違いは、MILはmathlib4という証明ライブラリも利用し…
年末は帰省していたのですが、有休含めて1/8までお休みにしたこともあり時間ができました。そこでLean 4を勉強してみることにしました。 Lean 4は以前このブログで紹介したLean 3と呼ばれる定理証明支援システムの後継システムです。 Lean 4からは関数型プログラミング言語としても使える、という触れ込みのようです。そこで今回はまず関数型プログラミング言語としてのLean 4を勉強してみました。勉強に使ったテキストは Functional Programming in Lean - Functional Programming in Lean です。このテキストを1章から4章まで読んでみ…
今年もこのブログをよろしくお願いします。 昨年の12月に最初は数日おきに、途中から毎日CISSPの練習問題を作成して投稿する、という企画を実行してみました。 CISSP資格試験の問題は巨大なテスト問題のバンクからほぼランダムに選んで各受験者に対して出題されるため、「2023年の試験問題のコピー」というようなものは概念的にも実際にも存在しません。受験希望者は有料や無料の練習問題を入手して頑張って解く練習をします。私も独学で勉強する中で練習問題を購入して解きました。 この企画の動機としては2つあります。公式な動機は、CISSPの練習問題づくりが自分の復習や能力の維持に役立ちそうだし、他の人の参考に…
-セキュリティ- コントロールのタイプ CISSP練習問題 ドメイン1
今回が「CISSP練習問題」の最終回です。途中からアドベントカレンダー風に毎日投稿してきました。ただコントロールの話はぜひ出題したいと思っていて、クリスマスをはみ出して投稿を続けていました。 最終回はセキュリティコントロールの5つのタイプの分類を意識した問題を出題します。 セキュリティ上の有害なイベントの発生後、システムを通常の運用の状態に戻すために使用されるコントロールはどれですか？ a. セキュリティ監査 b. 入力検証 c. ソフトウェアのパッチ d. ミラーサイト 正解：d ミラーサイト 正答が正しい理由 ミラーサイトは復旧コントロールの1つでセキュリティ上の有害な事象の発生後、システ…
-セキュリティ- 管理コントロール CISSP練習問題 ドメイン2
情報セキュリティのコントロールの3つの種類に関する問題です。この話はドメイン1に書かれるべきだと思うのですが、データセキュリティと絡めてドメイン2に書かれています。 管理コントロール(Administrative Control)は何を使用して組織の資産を守りますか？ a. 物理的なアクセス制御 b. ポリシー c. 情報の分類 d. コンピュータの機能と自動化 正解：b. ポリシー 正答が正しい理由 管理コントロールは組織のメンバーが従うべきポリシーやそれに紐づく規則を使って資産の保護を行います。 他の選択肢が間違っている理由 a. 物理的なアクセス制御：管理コントロールからの要請で物理的な…
ドメイン3からASLRの効果に関する問題を出題します。 攻撃者が自身のテストマシンで成功した悪用コードを対象システムで実行する際のASLR(Address Space Layout Randomization)の影響は何ですか？ a. 悪用コードが失敗する可能性が高まる b. セキュリティポリシーが無効になる c. ファイアウォールが遮断する d. ユーザーアカウントがロックアウトされる 正解：a 悪用コードが失敗する可能性が高まる 正答が正しい理由 ASLRによってメモリアドレスがランダム化されるため、攻撃者が特定のアドレスに依存することが難しくなり、悪用コードが他のシステムで失敗する可能性…
-セキュリティ- ブロック暗号モード CISSP練習問題 ドメイン3
暗号に関してはCBKにも結構専門的なことが記載されています。ここは頑張って勉強しなければなりません。 カウンター（CTR）モードの主な特徴は何ですか？ a. フィードバックに前の暗号文を使用する b. 同じ平文は同じ暗号文を生成する c. 同じ平文は同じ暗号文を生成せず、暗号化・復号化が並列処理できる d. エラーが発生するとそれが連鎖し、後続のブロックに影響を与える 正解：c 暗号化・復号化が並列処理できる 正答が正しい理由 CTRモードはナンス付きカウンターを使用して暗号化を行い、同じ平文が同じ暗号文を生成しない特徴があります。また、暗号化に前のブロックのデータを使用しないため、各ブロック…
-セキュリティ- リスク対応 CISSP練習問題 ドメイン1
アドベントカレンダーはクリスマスまでのものですが、このシリーズは12月28日までは続けようと思います。 ドメイン1からの出題です。リスクが識別されて分析・評価された後に組織としての対応を決める必要があります。このリスク対応に関する問題です。 特定のリスクを取り除くために、そのリスクを引き起こす活動や技術を停止または取り除く戦略は何ですか？ a. 回避する b. 緩和する c. 転送する d. 受け入れる 正解：a 回避する 正答が正しい理由 リスク回避は、特定のリスクを完全に排除するために、リスクを引き起こす活動や技術を停止または取り除く戦略です。 他の選択肢が間違っている理由 b. リスク緩…
-セキュリティ- パッチ管理 CISSP練習問題 ドメイン7
ドメイン7はセキュリティ運用に関するドメインです。すでにそれ以前のドメインで紹介されているセキュリティの概念やシステムを現場で運用する方法を述べています。パッチもドメイン3やドメイン6ですでに部分的に述べられています。ドメイン7では脆弱性管理と関連してパッチ管理について述べられています。 情報セキュリティにおいてパッチ管理プロセスが重要な理由は何でしょうか？ a. システムの性能向上を図るために必要なプロセスである。 b. セキュリティポリシーの策定を支援するための手段である。 c. 特定の脆弱性や問題に対処し、セキュリティを維持するための手法である。 d. インシデント対応の一環として必要な…
個人的の感想ですが、ドメイン5は割とタフで勉強が大変な印象です。IAAAの基本概念、ID連携、シングルサインオン、LDAP, Kerberos, RADIUS, SAML, OAuthなど認証/認可のシステム、MAC, DAC, RBAC, ABACなどの認可の仕組み、type1〜3 の認証要素、ID管理とライフサイクル、物理アクセス制御、、、日常的に使われている技術や概念であるがゆえに自分の経験に基づいた理解に頼ると間違いやすいところでもあります。 ネットワーク認証システムの中で、LDAP（Lightweight Directory Access Protocol）はどのような役割を果たして…
ドメイン5からフェデレーテッドアイデンティティ(ID連携)に関する問題を出します。 フェデレーテッドアイデンティティ管理（FIM）においてセキュリティ専門家が検討すべき重要な要素は？ a. フェデレーションのビジネス利益 b. アイデンティティ管理の複雑性 c. フェデレーション参加組織のセキュリティプラクティス d. ユーザーのアクセスの簡素化 正解：c フェデレーション参加組織のセキュリティプラクティス 正答が正しい理由 他の組織のセキュリティプラクティスが不足している場合、フェデレーションによってアクセスが許可されるシステムのリスクが増加します。 他の選択肢が間違っている理由 a ビジネ…
-セキュリティ- データ分類 CISSP練習問題 ドメイン2
ドメイン2からデータ分類に関する問題です。データ分類は地味ですが重要なセキュリティ施策です。 データ分類ポリシーと手順を持つことは、情報を最も効率的かつ効果的に保護するためのどの段階で役立ちますか？ a. データの分類を行う前 b. データの分類中 c. データの分類が完了した後 d. データ分類が不要な場合 正解：c データの分類が完了した後 正答が正しい理由 データ分類ポリシーと手順が整備されていると、データが適切に分類された後に適用するデータ保護のためのセキュリティコントロールを効果的かつ効率的に設計できます。データ分類が完了する前では、重要なデータの保護が不十分になる可能性があります。…
-セキュリティ- IoTセキュリティ CISSP練習問題 ドメイン3
CISSPのCBK (Common Body of Knowledge)のドメイン3には新しい技術もいくつか記載されておりIoT機器も取り上げられています。今回はそのIoT機器のセキュリティの問題です。 セキュリティ専門家がIoTデバイスの脆弱性を評価する際、最も重要な要因は何でしょうか？ a. デバイスのハードウェア仕様 b. ユーザーの対話パターン c. デフォルトの設定と認証メカニズム d. デバイスの物理的な保護手段 正解：c. デフォルトの設定と認証メカニズム 正答が正しい理由 IoTデバイスの脆弱性はデフォルトの設定が容易に推測されるか、実際には広く知られていることが挙げられます。…
-セキュリティ- 組織とセキュリティ CISSP練習問題 ドメイン1
もう一問ドメイン1から出題します。現代では組織をつくり社会的な活動をするときには最初からセキュリティを考慮する必要があります。それを実際にやり始めるにはどうしたら良いか、考えてみて下さい。 組織にセキュリティ機能を実装する際にトップダウンアプローチにおいて、シニアリーダーシップはどのように始めますか？ a. IT部門のセキュリティニーズの特定 b. 組織が直面する規制とセキュリティ脅威の理解 c. セキュリティポリシーの策定 d. セキュリティ機能の開発 正解：b 組織が直面する規制とセキュリティ脅威の理解 正答が正しい理由 トップダウンアプローチでは、シニアリーダーシップは組織が直面する規制…
-セキュリティ- セキュリティの目的 CISSP練習問題 ドメイン1
ドメイン1からの設問です。組織の中でのセキュリティ機能の位置付けに関する問題です。 セキュリティガバナンスにおいて、組織が最も行うべき活動には次のうちどれが含まれますか？ a. 組織のセキュリティ機能を特定のプロジェクトにのみ適用すること b. 組織のセキュリティ機能を他社の機能と統合すること c. 組織のセキュリティ機能を組織のビジネス戦略に整合させること d. 組織のセキュリティ機能を組織の最優先事項として扱うこと 正解：c 組織のセキュリティ機能を組織のビジネス戦略に整合させること 正答が正しい理由 セキュリティガバナンスでは、組織はセキュリティ機能をビジネス戦略に整合させ、組織の目標と…
ドメイン1からの出題です。情報セキュリティにおいて最も基本となる概念であるCIAに関する問題です。 情報が正確であること、妥当であること、および欠落がないこと、を維持する概念は何ですか？ a. 完全性 b. 可用性 c. 信頼性 d. 機密性 正解：a 完全性 正答が正しい理由 完全性の主な目標は、データが権限のある目的を持つ権限のある当事者以外によって操作されず、権限のない操作が容易に特定できるようにすることです。データの完全性を適切に保護しないと、不正確な情報に基づいて不適切な意思決定や潜在的に有害な行動が起こる可能性があります。 他の選択肢が間違っている理由 - 可用性は、データが必要な…
ソフトウェアの開発を理解しその中で必要なセキュリティ対策を実施していくことは非常に重要です。 SDLCのどのフェーズで、システムの要件が文書化され、システムの設計と必要なアーキテクチャが行われますか？ a. 初期化 b. 開発 c. 配備と納品 d. 運用と保守 正解：b 正答が正しい理由 開発フェーズでは、システムの要件が文書化され、システムの設計と必要なアーキテクチャが行われます。これに基づいてシステムが開発されます。 他の選択肢が間違っている理由 a. 初期化フェーズではビジネスニーズが表明され、要件が文書化される段階です。 c. 配備と納品フェーズではシステムが実際の運用環境に配置され…
-セキュリティ- インシデント対応 CISSP練習問題 ドメイン7
ドメイン7からインシデント対応プロセスにおける検知に関する問題です。 セキュリティインシデントを検知するために、組織はどのような手段を使用するべきですか？ a. インシデントを手動で報告する b. SIEMツールを使用してログを監視する c. セキュリティアナリストによる手動監視 d. ファイアウォールのログを毎日確認する 正解：b 正答が正しい理由 SIEMツールはセキュリティインシデントを検知し、アラートや信号を生成するための効果的なツールです。ログの監視を自動化し、検知速度を向上させる役割を果たします。 他の選択肢が間違っている理由 a. インシデントの手動報告は遅延が生じる可能性があり…
ドメイン6からセキュリティテストの問題です。 コードの開発段階へのフィードバックが容易であるため、セキュリティの観点から最も望ましいとされるテストアプローチは何ですか？ a. システムテスト b. グレーボックステスト c. ホワイトボックステスト d. ブラックボックステスト 正解：c ホワイトボックステストはソースコードへのアクセスがあり、コード開発段階へのフィードバックが容易です。変更が容易な段階でのテストが重要です。 他の選択肢が間違っている理由 a. システムテストはアプリケーション全体の動作をテストし、コード開発へのフィードバックが難しい場合があります。 b. グレーボックステスト…
-セキュリティ- ペンテスト CISSP練習問題 ドメイン6
ドメイン6からペンテストの実施手順（5つのフェーズ）に関する問題です。各フェーズとその目的がわかることが必要です。 ペネトレーションテスターが、Metasploitなどのツールを使用して、同定された脆弱性を悪用しアクセスを試みる際の目的は何ですか？ a. システムのパフォーマンス向上 b. システムの脆弱性の特定 c. システムのセキュリティ評価 d. システムへの不正アクセスの確立 正解：d ペネトレーションテスターがExploitationフェーズでツールを使用して脆弱性を悪用するのは、システムへの不正アクセスを確立するためです。 他の選択肢が間違っている理由 a. ペネトレーションテスト…
-セキュリティ- 脆弱性評価 CISSP練習問題 ドメイン6
特定された脆弱性の評価には、組織の固有の構成や状況を考慮した何が含まれていますか？ a. 攻撃者が実施する前の脆弱性スキャン b. 脆弱性に対する優先順位付けと対応策の評価 c. 組織のフィジカルセキュリティの評価 d. インシデント発生時の対応計画の構築 正解：b 組織の固有の構成や状況に基づいて、特定された脆弱性の影響を評価し、それに優先順位をつけて対応策を評価することが含まれます。 他の選択肢が間違っている理由 a. 攻撃者が実施する前の脆弱性スキャンは関連性が低いため、正しくありません。 c. 組織のフィジカルセキュリティの評価は脆弱性に焦点を当てておらず、正しくありません。 d. イ…
-セキュリティ- アカウント管理 CISSP練習問題 ドメイン5
だんだんノリとしてはアドベントカレンダー的になってきました。このCISSP資格試験のための練習問題シリーズを、毎日少なくともクリスマスまで続けたいと思います。 定期的なアクセスレビューの目的は何ですか？ a. アクセスの承認 b. データの暗号化 c. プロビジョニングの実施 d. アカウントが正しいことの確認 正解：d 定期的なレビューは、プロビジョンされたアカウントが依然として正確であるかどうかを確認するために行われます。不要なアカウントや過剰な権限を持つアカウントは、撤廃アクションを使用して終了する必要があります。 他の選択肢が間違っている理由 a. アクセスの承認はレビューの目的ではあ…
Mandatory Access Control (MAC) モデルにおいて、ラベルが使用される目的は何ですか？ a. ユーザーの認証情報を表示するため b. オブジェクトの機密度を示し、アクセスを制御するため c. ネットワーク通信の暗号化を実現するため d. ファイルの物理的な保管場所を指定するため 正解：b MAC モデルでは、ラベルがオブジェクトに関連付けられ、そのオブジェクトの機密度を示します。これにより、ユーザーに与えられるアクセス権が厳格に制御されます。 他の選択肢が間違っている理由 a. ラベルはユーザーの認証情報とは直接関係ありません。 c. ラベルは通信の暗号化とは異なりま…
もう一問ドメイン5からIAM関連の問題を出します。問題文に登場する物理的な証明書(IDカードなど)には顔写真と名前などが記載された組織発行のものを考えて下さい。単純のためにICチップなどの組み込まれていないものとして下さい。 IAMシステムにおいて、ユーザーが物理的な証明書（IDカードなど）を使用してアイデンティティを主張するプロセスは何ですか？ a. 識別 b. 認証 c. 認可 d. 説明責任 正解：a 識別は、ユーザーがアイデンティティを主張するプロセスを指します。物理的な証明書を使用する場合もこれに該当します。 他の選択肢が間違っている理由 b. 認証はアイデンティティを確認するプロセ…
-セキュリティ- IAM CISSP練習問題 ドメイン5 ID管理
IAM(Identity Access Management)の四つの基本要素は何ですか？ a. 識別、認証、認可、説明責任 (IAAA) b. 情報セキュリティ、アクセス制御、ユーザー管理、コンプライアンス (IAUC) c. 完全性、可用性、機密性、非否認 (IACN) d. 暗号化、復号化、キー管理、ハッシング (EDKH) 正解：a IAMは識別、認証、認可、および説明責任の四つの基本要素から成り立っています。これらの要素は、リソースへのアクセスを管理し、アクセスを要求するエンティティを識別し、検証し、その行動に責任を持たせるために必要です。 正答の理由 IAMは識別、認証、認可、およ…
TPM（Trusted Platform Module）についての説明文から、TPMが担当する最も主要な機能は次のうちどれでしょうか？ a. 機密データの暗号化 b. ハードウェアおよびソフトウェアの状態の暗号的ハッシュの生成 c. 攻撃からのデータのバックアップ d. デジタル署名の生成 正解：b TPMはアタステーション（Attestation）機能により、システムの正常なハードウェアおよびソフトウェアの状態の暗号的ハッシュを生成し、これによりサードパーティがシステムの整合性を検証できます。 以下の選択肢は間違っています。 a. 機密データの暗号化はTPMの一機能ですが、主要な機能ではあり…
-セキュリティ- メモリ保護、CISSP練習問題 ドメイン3 セキュリティアーキテクチャとエンジニアリング
メモリ保護に関する基本的なセキュリティコントロールとして、何が可能になるのでしょうか？ a. プログラムの同時実行 b. メモリアクセスの拒否 c. 特権モードの制御 d. オペレーティングシステムの終了 正解：a メモリ保護は、オペレーティングシステムが複数のプログラムを同時にメインメモリにロードし、各プログラムが割り当てられたメモリ以外にアクセスできなくするセキュリティコントロールです。 以下の選択肢は間違っています。 b. メモリアクセスの拒否はメモリ保護の一部ではありますが、それだけが目的ではありません。メモリ保護は、他のプログラムのメモリに不正にアクセスできないようにすることも含まれ…
-セキュリティ- メモリ保護、CISSP練習問題 ドメイン3 セキュリティアーキテクチャとエンジニアリング
あちらこちらのブログではこの時期アドベントカレンダー記事が盛んですね。この練習問題シリーズは毎日は無理ですが、ある程度の量ができるまで継続的に出していくつもりです。 メモリ保護をサポートするために必要な関連ハードウェア機能は何でしょうか？ プロセッサの単一モード プロセッサのデュアルモード メモリの単一アクセス メモリの共有モード 回答 正解: b. プロセッサのデュアルモード メモリ保護を実現するためには、プロセッサが特権（またはカーネル）モードと非特権（またはユーザ）モードの少なくとも2つのモードで動作できるデュアルモードが必要です。 以下は間違っている理由です。 a. プロセッサの単一モ…
-セキュリティ- CISSP練習問題 ドメイン3 セキュリティアーキテクチャとエンジニアリング
なぜ、暗号技術においては、適切な暗号アルゴリズムが将来にわたり確認される必要がありますか？ 暗号化の効果が低下する可能性があるため 複雑なアルゴリズムが使用されると理解が難しくなるため コンピューティングの進歩によりwork factorが減少するため すべての暗号アルゴリズムが一律に強固であるため 回答 正解：c. コンピューティングの進歩によりwork factorが減少するため 暗号解読に必要なwork factorは、コンピューティングの進歩により縮小する可能性があります。そのため、将来にわたって情報を保護するためには、適切な暗号アルゴリズムの選択が重要です。 以下は間違っている理由で…
-セキュリティ- CISSP練習問題 ドメイン3 セキュリティアーキテクチャとエンジニアリング
非否認性（nonrepudiation）を実現するために、どの暗号学的概念が利用されますか？ 公開鍵暗号 デジタル署名 ハッシュ関数 対称鍵暗号 回答 正解: b. デジタル署名 非否認性は通信当事者が行動やメッセージを否認できないことを指します。デジタル署名はメッセージの署名者を確認し、否認を防ぐために使用されます。 以下は間違っている理由です。 a. 公開鍵暗号: 公開鍵暗号は機密性や認証に関連していますが、非否認性の要件を直接満たすものではありません。 c. ハッシュ関数: ハッシュ関数は整合性を確保するために使用されますが、非否認性には直接関連していません。 d. 対称鍵暗号: 対称鍵…
-セキュリティ- CISSP練習問題 ドメイン2 資産のセキュリティ
情報資産の特定と分類に関して、どの記述が最も適切ですか？ 機密性の高い情報は常に特定しやすく、簡単に分類できます. 情報特定と分類が行われない場合、すべての情報が同じセキュリティ対策で保護されることになります. データがクラウドに保存されている場合、分類は不要です. 情報分類はセキュリティ対策には関与せず、主に法的な要件に従うものです. 正解：b 情報特定と分類が行われない場合、すべての情報が同じセキュリティ対策で保護されることになります. 情報の特定と分類が行われないと、組織はどの情報が重要で、どの情報が追加のセキュリティ対策が必要かを判断できません。結果として、一律の対策が適用され、リソー…
-セキュリティ- CISSP練習問題 ドメイン2 資産のセキュリティ
CISSPの練習問題を出題し、解説していくシリーズを始めます。各記事はまず問題文と選択肢が表示されています。「回答」ボタンを押すと正解とその理由が表示されます。 問題に対して色々コメントをいただけると嬉しいです。答えが変、こっちが正しい、意味不明、などなど。では早速初回の問題を出題します。 情報資産の特定と分類に関して、どの記述が最も適切ですか？ 機密性の高い情報は常に特定しやすく、簡単に分類できます。 情報特定と分類が行われない場合、すべての情報が同じセキュリティ対策で保護されることになります。 データがクラウドに保存されている場合、分類は不要です。 情報分類はセキュリティ対策には関与せず、…
有界閉集合では連続関数に最大・最小が存在という良い性質があります。一方、有界であっても開集合の場合にはそのような性質はありませんし、有界でない閉集合にもそのような性質はありません。 ある有界閉集合$S\subset\mathbb{C}$で連続関数列$f_n$が各点収束で$\lim_{n\to\infty}f_n=f$とします。$S$での$f_n-f$の最大値・最小値を$Max_n, Min_n$とすると$n\to\infty$の時に$max( Max_n , Min_n )\to 0$であればこの有界閉集合上で$f_n$は$f$に一様収束しています。一様収束であればさまざまな良い性質が証明で…
-数学- 複素関数論 補足 リュービルの定理と代数学の基本定理
この記事では複素関数論の応用として代数学の基本定理を証明します。この辺の話は勉強していて興味深い話だったのですが、今回の予定のストーリーからは横道に逸れる感じだったので、補足として今回記事にすることにしました。 リュービルの定理は以前に楕円関数の性質の証明で使ったこともあり、その証明がきっちりと数式で示せる事を知り楽しかったです。 代数学の基本定理：定数を除く複素数係数の1変数代数方程式は複素根を持つ。 この証明に使う次の定理も証明します。 リュービルの定理：有界な整関数は定数関数に限る。 この証明に使うコーシーの不等式も証明します。 コーシーの不等式：$D$を中心$z$、半径$R$の開円板、…
-数学- 複素関数論(18) リーマンのゼータ関数の解析接続
このブログでは過去にリーマンのゼータ関数については色々と取り上げてきました。一方その複素解析的な話はいつもちょっと傍に置いてました。 今回は複素関数論シリーズの最後にリーマンのゼータ関数の複素解析的な部分について基本的な定理を並べていきます。今までと同じレベルで証明していくと結構大変なので定理を正確に理解する＋証明の方針、というレベルの話です。 リーマンのゼータ関数の定義：$s\in \mathbb{R}, s\gt 1$に対してリーマンのゼータ関数$\zeta(s)$を以下の級数で定義する。 $$\zeta(s)=\sum_{n=1}^{\infty}\frac1{n^s}$$ 命題A ゼー…
-数学- 複素関数論(17) ガンマ関数の無限乗積と逆数の整関数性
今回はガンマ関数のガウスによる無限積表示を実解析の範囲で示します。またこれとワイエルストラスによる無限乗積が同値であることを示します。 そしてガンマ関数のワイエルストラスの無限乗積の逆数が整関数であることを紹介します。 ガウスによるガンマ関数の無限積表示定理：任意の$z\in\mathbb{C}$に対して、 $$\frac1{\Gamma(z)}=\lim_{n\to\infty}\frac{z(z+1)\cdots (z+n)}{n! n^z}$$ ここではいったん任意の正の実数$x$について証明します。 $$\gamma_n(x)=\int_0^n t^{x-1}f_n(t)dt, f_n…
-数学- 複素関数論(16) ガンマ関数の複素平面上の有理型関数への解析接続
ガンマ関数を正の実数軸から正の右半平面に解析接続する際には、表示式は変わらず、より広い領域での収束と正則性を証明したため、結構面倒でした。 今回はガンマ関数を更に複素平面上の有理型関数に解析接続します。今回はガンマ関数が満たす関数方程式を使うことで左半面でも値が一意に決まることで、正則性、極の位置などが決定されます。 ガンマ関数の解析接続定理2：$\Gamma(s)$は$\mathbb{C}$上の有理型関数に解析接続される。極は$0$及び全ての負の整数であって全て1位の極で$s=-n$での留数は$\frac{(-1)^n}{n!}$である。 証明は以下の通りです。まずガンマ関数の積分による定義…
-数学- 複素関数論(15) ガンマ関数の右半平面の正則関数への解析接続
今回は柳田氏の講義録を参考にしています。とても分かりやすく助かっています。 ガンマ関数の解析接続の定理1：ガンマ関数は複素数平面の右半平面$\mathbb{H}_r=\{s\in\mathbb{C} Re(s)\gt 0\}$で定義された正則関数に解析接続できる。その表示式は正の実数上の定義式と同じである。 $$\Gamma(s)=\int_0^{\infty}e^{-t}t^{s-1}dt$$ 証明はまず収束を示したのちに正則性を示します。 この定義を明確にするためには複素数を指数とする冪乗の定義が必要ですが、ちょっと省略して以下の事実だけを使うことにします。$t$を実数、$s$を複素数…
ガンマ関数は階乗の一般化で数学のあちらこちらで登場する関数です。階乗は自然数$n$に対して$n!=n\cdot(n-1)\cdot(n-2)\cdots 2\cdot 1$のように定義されます。例えば$3!=3\cdot 2\cdot 1=6$です。 これを正の実数に対して拡張したのがガンマ関数で下記の広義積分によって定義されます。$s\gt 0$として $$\Gamma(s)=\int_0^{\infty}e^{-t} t^{s-1}dt$$ この広義積分の収束は次のように分かります。$0\lt a \lt 1 \lt b$として $$\int_0^{\infty} e^{-t} t^{s-…
ガンマ関数やゼータ関数の解析接続や解析的な性質を述べるために必要な複素関数論の定理を述べます。 正則な関数列の定理：関数列$\{f_n\}_{n\in\mathbb{N}}$が開集合$U$上で正則で、$U$の任意の有界閉集合で関数$f$に一様収束する（このとき広義一様収束という）とき、$f$は$U$上で正則である。 一様連続の定理：有界閉集合で連続な関数は一様連続である。 正則な積分関数の定理：$U\subset\mathbb{C}$を開集合として$F(z,s)$を$(z,s)\in U \times [a,b]\subset\mathbb{R}$で定義された関数で次の2つの条件を満たすものと…
ついに有理型関数の定義を理解するところまでやってきました。嬉しいことです。ただその前に有理関数を述べたいと思います。有理関数は複素数係数の多項式の商であるような関数です。$P(z),Q(z)$を複素係数の多項式として$f(z)=\frac{P(z)}{Q(z)}$ならば$f:\{z\in\mathbb{C} Q(z)\neq 0\}\to \mathbb{C}$は有理関数です。 有理型関数は有理関数の定義の多項式を正則関数に置き換えたものになります。しかし定義はちょっと違った形で与えられます。 有理型関数の定義：関数$f$が開集合$U\subset \mathbb{C}$上有理型であるとは…
前回記事で紹介した留数の定義を復習してから留数定理を述べます。 留数の定義：関数$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}\frac{f(z)}{(z-c)^{n+1}}dz\,,(n\in \mathbb{Z})$$ として、$a_{-1}$を$f$の$c$における留数とよび$Res(f;c)$で表す。 留数定理：領域$K$において1…
円盤領域で正則な関数は冪級数展開ができましたが、円環領域で正則な関数はローラン展開ができます。今回は明治大学の桂田氏の講義資料をベースにこの辺の定義と定理を確認していきます。 円環領域の定義：同じ中心を持つ2つの円盤の間に挟まれた領域を円環領域と呼ぶ。領域は開集合だったので、中心を$c$、2つの円盤の半径$0\le R_1 \lt R_2 \le +\infty$に対して、記号$A(c;R_1,R_2)=\{z\in\mathbb{C} R_1 \lt z-c \lt R_2\}$で円環領域を表す。さらに境界を含めた閉集合を記号$\overline{A}(c;R_1,R_2)=\{z\…
ここまでの知識を使って「一致の定理」と「解析接続の定義」を述べることが出来ます。Wikipediaによれば一致の定理には2つの形があると書いてあり、本当にその通りです。解析概論と名古屋大学の柳田さんの講義資料がそれぞれの形で書いてあります。 一致の定理（解析概論）：領域$K$において関数$f(z), g(z)$が正則で、$K$内の小領域$K_0$( あるいは$K$に集積点を持つ$K$の部分集合$K_0$)で$f(z)=g(z)$であれば、$K$で常に$f(z)=g(z)$である。 一致の定理（柳田さん講義資料）：$f$を領域$K$上の正則関数として、$K$に集積点を持つ相異なる点の列$\{ z…
ちょっとだけ寄り道して一様収束関連の話題をまとめておきます。今回は「複素関数」桂田 祐史氏 明治大学を基にして説明していきます。 一様収束は適当な集合上で定義された複素数値関数の列が、その集合上で一様にある関数に収束することを言います。 一様収束の定義：$K$を空でない集合、関数$f, f_n$は$f:K\to\mathbb{C}, f_n:K\to\mathbb{C}$で、$\{f_n\}_{n\ge 0}$は関数列とする。$f_n$が$f$に$K$で一様収束する、とは次式が成り立つことをいう。 $$\lim_{n\to\infty} \sup_{x\in K} f_n(x)-f(x) =…
ある領域で正則な関数は領域内の任意の点で冪級数に展開できることを証明します。証明に必要な設定を含む版で証明を進めます。 定理54(すごく複雑)：関数$f$が領域$K$で正則とする。$K$内の任意の点$a\in K$を中心として領域$K$の最も近い境界点を通る円を$K_0$、その半径を$r_0$とする。この円の中の任意の点を$\zeta$とすると、 $ \zeta - a = \rho $として中心$a$, 半径$r, (\rho \lt r\lt r_0)$の円周$c$を考える。この時$f$は$\zeta$で以下のようにテイラー級数に展開される。 $$f(\zeta)=\sum_{n=0…
-数学- 複素関数論(6) コーシーの積分表示(公式)と正則関数の冪級数展開
コーシーの積分公式を使うことで、正則関数が冪級数に展開できることを示すことができます。今回も主に解析概論を参考にしています。 定理の述べ方が色々あり、なぜそうしているのかを考えてみました。あっているかはわかりませんが、今回はその辺を書いてみます。 その解析概論の58. コーシーの積分公式．解析関数のテイラー展開ではこの定理は次のように述べられています。 定理54：解析関数は，それが正則な領域内の任意の点においてテイラー級数に展開される。 （解析関数は正則な関数と同義で、1回微分可能の意味。冪級数展開とテイラー展開も同じ意味）。 見ればわかるとおりこの定理そのものでは冪級数の係数、定義域（収束円…
複素関数論の入り口で最も重要な定理と言われているコーシーの積分表示です。ある領域で正則な関数を積分を使って表示する方法を学びます。今回はその証明まで述べます。重要な応用は次回とします。 コーシーの積分表示（積分公式）：単純閉曲線$C$の内部及び周上で$f$が正則で$a$が$C$の内部の任意の点ならば $$f(a)=\frac1{2\,\pi\,i}\int_{C}\frac{f(z)}{z-a} dz$$ 証明してみましょう。そのために$a$を中心とした半径$R\gt 0$の円を描き、その円周を$C'$、開円板を$D$とします。この状況を絵にするとこんな感じです。 前回のコーシーの積分定理の拡…
いよいよコーシーの積分定理について述べていきます。ここでは主に解析概論の57. コーシーの積分定理、に基づいて記載しています。 前回、原始関数を使った積分計算の定理を紹介しました。この定理から、ある関数の積分の計算は原始関数がある場合はそれを求めて、$C$の終点と始点での$F$の値の差で計算できることがわかりました。特に$C$が閉曲線の場合$w_0=w_1$なので $$\int_C f(x) dx=F(w_1)-F(w_0)=F(w_0)-F(w_0)=0$$ でした。 原始関数を使った積分計算の定理にしろ、上記の等式にしろ、被積分関数$f$に原始関数があればそれを使って計算できる、という話で…
複素積分の定義をします。今回は特に、 2021年度現代数学基礎CIII 講義ノート 柳田 伸太郎氏 名古屋大学 を参考にしました。 複素積分の定義：$C$を滑らかな曲線として$C$上で定義された関数$f$ について、$f$の積分路$C$上での複素積分$\int_C f(x)dx$を次のように定義する。 $p:[a,b]\to \mathbb{C}$を$C$のパラメータの1つとして、 $$\int_C f(x)dx = \int_a^b f(p(t))p'(t)dt$$ ただし右辺はリーマン積分の意味とする。 さらに区分的に滑らかな曲線$C$に対しては$[a,b]$を分割して各区間で$C$が滑ら…
-数学- 複素関数論(2) 積分路のための複素平面上の曲線について
複素積分に必要な積分路をしっかりと定義するのはとても大変だということを知りました。 複素積分では積分路に沿って複素関数を積分します。この積分路は複素平面上の曲線であり、曲線をうまく定義できている必要があります。 このためにまずパラメータ付き曲線及び滑らかなパラメータ付き曲線を定義します。次に区分的に滑らかなパラメータ付き曲線を定義し、その間の同値関係を定義して、同値類を区分的に滑らかな曲線と定義します。 パラメータ付き曲線：実数の閉区間$[a,b]\subset \mathbb{R}$から複素平面$\mathbb{C}$への連続写像。 滑らかなパラメータ付き曲線：パラメータ付き曲線$p:[a,…
まずはともあれ微分と正則関数です。 微分と正則の定義：複素数の集合を$\mathbb{C}$とする。$\mathbb{C}$の開部分集合$U$上の関数$f$が$U$の点$z$で微分可能である、とは極限 $$\lim_{h \to 0}\frac{f(z+h)-f(z)}{h}$$ が存在することを言う。この時 $$f'(z)=\lim_{h \to 0}\frac{f(z+h)-f(z)}{h}$$ と書き、$f$の$z$における微分という。 $U$の全ての点で微分可能である時、関数$f$は$U$で正則である、という。 関数$f$が$U$のある点$z$のある近傍で正則である時、関数$f$は$U…
この夏、毎日暑い日がつづています。そんな中、少し基本的な数学の勉強をしています。遠い昔、大学生の頃に多分一応勉強したと思うのですが、結構曖昧な部分も多いまま、なんとなく知っているふりをしてきた、複素関数のことです。 正則関数から初めて有理型関数を理解し、ある複素関数が有理型かどうかをわかるようになることが目標です。ものすごく具体的には、 「$\Gamma(s)$ は $C$ 上の有理型関数に解析接続される. 極は $s = 0, −1, −2, \cdots$ にあって全て1 位であり, $s = −n$ での留数は$ \frac{(−1)^n}{n!} $である。」 「$\frac1{\Ga…
問題 $p$を任意の奇素数とします。$p$が奇数なので$\sqrt{2}^{p-1}$は自然数になります。このとき$\sqrt{2}^{p-1}$を$p$で割るとその余りは$1$あるいは$p-1$になります。この事を証明してください。 例 $p=7$の時$\sqrt{2}^{7-1}=8$。$8$を$p=7$で割ると商は$1$で余りも$1$です。 $p=13$の時$\sqrt{2}^{13-1}=64$。$64$を$p=13$で割ると商は$4$で余りは$12$です。この場合は$12=13-1=p-1$になってます。 証明 オイラーの基準から任意の整数$a$と奇素数$p$について $$\left…
今回の勉強をしていて、これはちょっと面白い問題が作れそうと思ったことがありました。それが以下の問題です。回答編は明日載せます。それまで考えてみてください！ 問題 $p$を任意の奇素数とします。$p$が奇数なので$\sqrt{2}^{p-1}$は自然数になります。このとき$\sqrt{2}^{p-1}$を$p$で割るとその余りは$1$あるいは$p-1$になります。この事を証明してください。 例 $p=7$の時$\sqrt{2}^{7-1}=8$。$8$を$p=7$で割ると商は$1$で余りも$1$です。 $p=13$の時$\sqrt{2}^{13-1}=64$。$64$を$p=13$で割ると商は$…
-数学- 有限体のガウス和による平方剰余の相互法則の証明(10)命題4.19の証明
この記事では平方剰余の相互法則の証明に必要な補助定理である命題4.19を証明します。そためにまず命題4.18を補題として示します。 命題4.18$p,q$を相異なる奇素数、有限体$F_p$上で$1$の原始$q$乗根の1つを$\zeta$とします。法$q$に関する平方剰余記号の値を係数とする$\zeta$のガウス和を$ G_q=\sum_{a=1}^{q-1}\left( \frac{a}{q} \right)\zeta^a $と定義します。この時任意の整数$k$について次が成り立ちます。$$\sum_{a=1}^{q-1}{\left( \frac{a}{q}\right)\,\zeta^{k…
-数学- 有限体のガウス和による平方剰余の相互法則の証明(9)命題4.16の証明
この記事では補助定理の1つである命題4.16 $G_q^2=q^{\ast}$ を証明します。そのためにまず、補題4.17 を示します。 補題4.17$a$を整数、$\mu \neq 1$を$1$の$n$乗根とするとき、$$\sum_{k=1}^{n-1}{\mu^{a\,k}}= \begin{cases}n-1 & (a \equiv 0\,(mod\,n))\\-1 & (a \not\equiv 0\,(mod\,n))\end{cases}$$ 証明 1) $a \equiv 0\,(mod\,n)$の場合、すなわち$a$が$n$の倍数の場合には$\mu^{a\,k}=(\mu^a)…
-数学- 有限体のガウス和による平方剰余の相互法則の証明(8)
いよいよ山本先生の本数論入門 (現代数学への入門)による相互法則の証明を見ていきます。有限体$F_p$におけるフロべニウス写像とガウス和を用いた証明です。今回はいくつかの補助定理を紹介し、それらを使った相互法則の証明を紹介します。それぞれの補助定理の証明は次回以降にしましょう。 まずは平方剰余の相互法則を再掲します。 命題4.9 相互法則 $p,q$を奇素数とします。$$\left(\frac{q}{p}\right)\,\left(\frac{p}{q}\right)=(-1)^{\frac{p-1}{2}\,\frac{q-1}{2}}=\begin{cases}1 & p\equiv 1…
-数学- 有限体のガウス和による平方剰余の相互法則の証明(7) 第2補充則の証明
今回はいきなり第2補充則の証明から行きます。前回の記事 では第2補充則において$\sqrt{2}^p$の指数の$p$が変化するとそれに伴って平方剰余記号の値$\left(\frac{2}{p}\right)$が周期$8$で変化することを観察しました。 今回は山本先生の数論入門 (現代数学への入門)で紹介されている証明を見ていきます。ここでは$\sqrt{2}$を有限体$F_{p^2}$の中の$1$の原始$8$乗根の適当な和で表しています。これを$p$乗すると和の$p$乗は$p$乗の和を使い、$\sqrt{2}^p$を$1$の$8$乗根の$p$乗の適当な和で表すことができます。 これが周期$8$…
-数学- 有限体のガウス和による平方剰余の相互法則の証明 (6) フロべニウス写像と2つの補充則
以下の式は$F_p$のフロべニウス写像によって$a$がいつ平方剰余になるのかを特徴づけているとも見えます。 $$\sqrt{a}^p=\left(\frac{a}{p}\right)\,\sqrt{a}\tag{A}$$ それが前回の記事の最後のステートメントでした。それらを再掲します。 「このことから第1補充則、第2補充則、相互法則をフロべニウス写像の言葉で言うと次のようになります。 $\sqrt{-1}^p=\sqrt{-1}$となる$p$の条件を求めること。 $\sqrt{2}^p=\sqrt{2}$となる$p$の条件を求めること。 $\sqrt{q^{\ast}}^p=\sqrt{q^…
-数学- 有限体のガウス和による平方剰余の相互法則の証明 (5) フロべニウス写像と平方剰余
ちょっとだけおさらいから入りましょう。 $p$を素数、$F_p$を 位数$p$の有限体とします。$F_p$の$0$以外の元の集合$F_p^{\times}$は位数$p-1$の巡回群になります。そうするとフェルマーの定理から任意の$x\in F_p$について$x^{p-1}=1$が分かります。両辺に$x$を掛ければ$x^p=x$となります。この式は$x=0$も含めて$F_p$の全ての元で成り立ちます。また$x^p=x$を$F_p$あるいはその拡大体での方程式と見た時、その解の個数は多項式の理論から高々$p$個です。一方、実際に$p$個の要素を持つ有限体$F_p$の元は全てこの方程式の解となってい…
-数学- 有限体のガウス和による平方剰余の相互法則の証明 (4) 平方剰余の定義と相互法則
いよいよこのシリーズも核心に入っていきます。今回は平方剰余の定義を与え、平方剰余記号を定義します。また平方剰余の基本的な性質を示した後、平方剰余の相互法則と関連する補充則などを紹介し、簡単なものには証明をつけます。最後に平方剰余の相互法則をより対称な形で表した命題を提示し、それが成り立つことをMaximaで再確認してみます。 定義 \(p\)を奇素数として\(a\)を\(p\)と互いに素な整数とします。\(a\)がある整数\(n\)の平方と法\(p\)で合同である時、\(a\)を\(p\)の平方剰余であるといいます。式で書けば、方程式\(X^2\equiv a\,(mod\,p)\)が解を持つ…
-数学- -数学- 有限体のガウス和による平方剰余の相互法則の証明 (3) GFパッケージ
window.addEventListener('message', function(e) { var iframe = document.getElementById("tako"); var eventName = e.data[0]; var data = e.data[1]; switch(eventName) { case 'setHeight': console.log(data); iframe.style.height = data + "px"; break; } }, false); 前の記事で有限体\(F_p\)やその拡大体\(F_{p^f}\)で成り立つ幾つかの命題と…
-数学- 有限体のガウス和による平方剰余の相互法則の証明(2) 有限体入門
駆け足で有限体を復習しましょう。 定義 有限体\(F_p\) 整数をある素数\(p\)で割った余りの集合\(\{0,1,\cdots,p-1\}\)には整数の加算や乗算の結果を\(p\)で割った余りとして自然に加算、乗算が定義でき、それらの単位元は\(0,1\)です。また全ての元に対して加算の逆元があり、\(0\)を除く全ての元に対して乗算の逆元があります。従って\(\{0,1,\cdots,p-1\}\)は体になります。この集合は要素数\(p\)の有限体であり記号\(F_p\)で表します。 具体的に\(p=3\)の有限体を例として考えてみましょう。\(F_3=\{0,1,2\}\)です。加算…
-数学- 有限体のガウス和による平方剰余の相互法則の証明(1)
小島寛之先生のブログ記事 で山本芳彦先生の著書「数論入門」 数論入門 (現代数学への入門) 作者:山本 芳彦 岩波書店 Amazon が絶賛されていました。その中で印象に残ったのが、有限体を使った平方剰余の相互法則の証明が秀逸、という点でした。 山本先生のこの本にはこのブログの以前の記事でも色々とお世話になっていますが、平方剰余は個人的に苦手意識もありちゃんと読んでいませんでした。改めて第3章剰余環から読んでみました。1週間くらいかけて有限体の復習、平方剰余と\(F_p\)とフロべニウス写像\(x^p\)、有限体のガウス和、そして平方剰余の相互法則の証明を理解することができました。 その過程で…
-その他- M1 Mac上の新しい仮想環境 VMware Fusion Player 13（とKali Linux）
昨年の11月にVMwareからVMware Fusion Player 13がリリースされました。VMware Fusion PlayerはmacOS上で仮想マシンを実行できるソフトウェアで、UTMやVirtualboxなどと同様のカテゴリの製品です。 store-jp.vmware.com セキュリティ関係でKali Linuxを使いたくてUTMにインストールしたのですが、Apple virtualizationではキーボードのマッピングが変で や_が入力できずshell操作がろくに出来ません。QEMUではキーボードはいいのですがスピードが遅くて困りました。 VMware Fusion Pl…
-その他- ラブソングの中の数学 Answers by Da-iCE
今年最後の記事は最近よく聴く楽曲の話です。 www.youtube.com Da-iCEのAnswersという楽曲です。最近お気に入りでよく聞いていたのですが、歌詞の中に「円周率」という言葉が聞こえることに気がつきました。おっ！と思って歌詞を調べてみると数学の用語が散りばめられていることがわかりました。 以下は数学に関係する単語とフレーズを抜き出してみたものです。 確率を知る為の公式、方程式、割り切れない円周率、導き出した答え、 理解して解くまでなどでもやり直そう 0をかけて台無しにしない 自然数、定義、数学 そもそも曲のタイトルがAnswersですね。数学をとても意識して作詞されたのでしょう…
この記事では最も簡単なシンギュラーモジュリ\(x_2\)を求めてみます。この値は前回の記事で求めた式 $$\frac{2}{\pi}=\sum_{k=0}^{\infty}(-1)^k\,A_k\,(4\,k+1), ただしA_k=\frac{\left( \frac12\right)_k^3}{k!^3}$$ でも使いました。 シンギュラーモジュリ\(x_2\)を求めるにあたりもう一度その定義を復習しておきましょう。アイゼンシュタイン級数の議論では一貫して次のような記号を定義して使ってきました。 $$q=e^{-y}, f(-q)=\prod_{n=1}^{\infty}(1-q^n), z…
-数学- 2次変換公式を取り替えて、さらに別のラマヌジャンの円周率公式を証明しよう(2)
P3C 今回は次の公式を証明します。 $$\frac{2}{\pi}=\sum_{k=0}^{\infty}(-1)^k\,A_k\,(4\,k+1), ただしA_k=\frac{\left( \frac12\right)_k^3}{k!^3}$$ Nayandeepさんの論文 "EISENSTEIN SERIES AND RAMANUJAN-TYPE SERIES FOR 1/π" では多くの円周率公式についてその証明が一定のフォーマットで与えられています。このシリーズではそのフォーマットをフレームワークと呼び、その一部を取り替えることで円周率公式とその証明が量産される様を見てきています。 …
-数学- 2次変換公式を取り替えて、さらに別のラマヌジャンの円周率公式を証明しよう(1)
以下の記事でNayandeepさんによるラマヌジャンの円周率公式の証明の構造を示し、フレームワークと呼んでみました。 maxima.hatenablog.jp このフレームワークの中でポイントとなる部分を変更すると異なる円周率公式を得ることができます。そのポイントの1つがガウス超幾何関数の2次変換公式を別のものに取り替えることです。 すると、「クローゼンの公式の特別な場合」の式が影響を受け別のものになります。そのため\(z^2\)が違う式になります。その微分も変わるためアイゼンシュタイン級数の変換公式に代入する式が変わり、得られる\(P(e^{-2\,\pi\,\sqrt{n}})\)の式も変…
-数学- Number Theory in the Spirit of Ramanujan, by Bruce C. Berndt
ラマヌジャン型の円周率公式の証明を理解する上で、\(q\)級数、超幾何関数、楕円積分、テータ関数、アイゼンシュタイン級数などをある程度理解しておくことが必要です。このためにとても役に立ったのが、このシリーズでも何度も紹介しているBerndtさんの次の本です。 Number Theory in the Spirit of Ramanujan (Student Mathematical Library) 作者:Berndt, Bruce C. Amer Mathematical Society Amazon この本の5章と6章に証明の細かいところまでが書いてあり、非常に勉強になりました。 一方、ち…
このシリーズでも折に触れて紹介してきたNayandeep BaruahさんとBerndtさんの論文 "EISENSTEIN SERIES AND RAMANUJAN-TYPE SERIES FOR 1/π" には多くの\(\frac{1}{\pi}\) 級数公式とその証明がフレームワークに基づいて示されています。今回はその中から次の公式の証明を紹介します。 $$\frac{1}{\pi}=\sum_{k=0}^{\infty}((8-5\,\sqrt{2})\,k+3-2\,\sqrt{2})\,A_k\,(2\,\sqrt{2}-2)^{3\,k}\, ただし A_k=\frac{\left…
ラマヌジャンの円周率公式のひとつである $$\frac{16}{\pi}=\sum_{k=0}^{\infty }{\frac{\left(42\,k+5\right)\,A_{k}}{2^{6\,k}}}$$ の証明を調べてMaximaで式変形を追いながら理解することができました。2021年10月21日に書いた記事 から始まるこの1年間の数学の記事は全てこの証明に関係した記事になっています。 参考文献としては以下の3つを参照しました。 メインは平田典子氏の「数理科学2020年8月号」の記事「ラマヌジャンと円周率近似公式」です。証明の全体の流れを日本語で把握できたのは貴重でした。 また楕円積分…
-数学- ラマヌジャンの円周率公式の証明（アイゼンシュタイン級数とその応用）
今回は今までに得られたアイゼンシュタイン級数の公式を元にして、ラマヌジャンの円周率公式のひとつを証明します。今回証明するのは次の式です。 $$\frac{16}{\pi}=5+ \frac{47}{64}\,\left(\frac12\right)^3 + \frac{89}{64^2}\,\left(\frac{1\cdot 3}{2\cdot 4}\right)^3+ \frac{131}{64^3}\,\left(\frac{1\cdot 3\cdot 5}{2\cdot 4\cdot 6}\right)^3 + \cdots$$ この式を総和記号、ポッホハマー記号などを使って書くと、\…
今回は今までに求めてきた2つの\(P(q)\)に関する数式を、\(n\)を適当な自然数として\(q=e^{-2\,\pi\,\sqrt{n}}\)の場合に特化した数式として計算してみます。とは言ってもおおむね代入して整理するだけです。 その系として次の式がほぼ自明に得られることも示します。 $$1-24\,\sum_{n=1}^{\infty }{\frac{n\,e^ {- 2\,\pi\,n }}{1-e^ {- 2\,\pi\,n }}}=\frac{3}{\pi}$$ 7年前に書いた記事: maxima.hatenablog.jp で示した$$ \sum_{n=1}^{\infty }…
庭で見つけた足長蜂の巣。業者の方に退治してもらいました。 今回は次の公式を証明します。 \(P(q)=1-24\,\sum_{n=1}^{\infty}\frac{n\,q^n}{1-q^n}, a\,b=\pi^2\)として、 $$ 6-a\,P\left(e^{-2\,a}\right)=b\,P\left(e^{-2\,b}\right)$$ 参考文献としては以前のブログ記事 maxima.hatenablog.jp でも紹介した、Nayandeep Deka BaruahさんとBruce C. Berndtさんの論文Eisenstein series and Ramanujan-typ…
ひとつ前の記事 maxima.hatenablog.jp を書き終えてからひとつ心に引っ掛かっていることがありました。普通は保型性を関数が\( z+1 \)や\(1/z\)で不変という形で表します。しかしラマヌジャンは\(a, b \gt 1, a\,b=\pi^2\)ならば\(h(a)=h(b)\)のような形で表している、という話をどこかで読んだという記憶が蘇ってきたのです。 多分黒川先生の本だろうと思い、家にある黒川先生の本を全て確認してみたところありました！ ラマヌジャンζの衝撃 (双書―大数学者の数学) 作者:黒川 信重 現代数学社 Amazon この本の第9章「保型性の展開」のp12…
今回はラマヌジャンのテータ関数の変換公式と呼ばれる次の式を証明します。次回以降でこの式からアイゼンシュタイン級数の変換公式を導きます。 $$ b^{\frac{1}{4}}\,e^ {- \frac{b}{12} }\,f\left(-e^{- 2\,b\,n }\right)=a^{\frac{1}{4}}\,e^ {- \frac{a}{12} }\,f\left(1-e^ {- 2\,a\,n }\right) $$ ただし\( f(-q)=\prod_{n=1}^{\infty}(1-q^n) \)及び\( a,b\gt 1, \, a\,b=\pi^2 \)です。 証明はデデキントの…
前回、アイゼンシュタインの変換公式を証明しました。この公式は数理科学2020年8月号の平田典子さんの記事においても、そのほかのラマヌジャンの円周率公式の証明の論文を見ていても基本的な式となっています。 今回はアイゼンシュタインの変換公式の応用として次の式を証明します。 $$P(q^2)=(1-2\,x)\sum_{k=0}^{\infty}(3\,k+1)A_k\,X^k\, ただし A_k=\frac{\left(\frac12\right)_k^3}{k!^3}$$ ここまでくると平田さんの記事や、このブログの以前の記事 maxima.hatenablog.jp でも紹介した、次のような式…
前回の記事 maxima.hatenablog.jp ではラマヌジャンの円周率公式の証明を理解したい、という動機を説明し、そこで使われるアイゼンシュタイン級数の変換公式について説明しました。 この記事ではその証明をMaximaで追っていきます。 window.addEventListener('message', function(e) { var iframe = document.getElementById("tako"); var eventName = e.data[0]; var data = e.data[1]; switch(eventName) { case 'setHeig…
ラマヌジャンの円周率公式は少なくとも17種類がラマヌジャンのノートブックに記載があり、さらにその後の研究で大量に類似の公式が見つかっています。それらの証明はいろいろな手法が使われており難易度も様々なようですが、数学愛好家としてはその1つくらいは理解したい、と思います。 多くの証明に共通する基本的な道具立ての部分として以下があります。 楕円積分 \(K(k)=\int_{0}^{\frac{\pi}{2}}{\frac{1}{\sqrt{1-k^2\,\sin ^2\vartheta}}\;d\vartheta}\) 超幾何関数\({}_pF_q(a_1,,,a_p;b_1,,,b_q,;z)\…
-その他- maxima-jupyterのインストールでエラー invalid number of arguments: 5 （直りました）
このブログのmaximaの記事を書くにあたって多用してきたmaxima-jupyterですが、最近新たにインストールしようとするとエラーが発生するようになってしまいました。例えば以前に掲載した次の記事の手順でもエラーが発生します。 maxima.hatenablog.jp (%i2) jupyter_install(); を実行するとinvalid number of arguments: 5というエラーが発生します。このエラーに気が付いたのが七夕の頃で、作者のロバートさんに連絡したり、github上でissueを登録したり、、、色々とコードを読んで原因はわかって来たので修正を作ってテストして…
「ブログリーダー」を活用して、jurupapaさんをフォローしませんか？
Mathematics in Lean4の数論の章の3つ目のセクションではいよいよ「自然数には素数が無限個ある」ことを形式化して証明します。 証明方法として3つのやり方が説明されています。それぞれの形式化も異なるので下記に記載してみました。 ある自然数nに対して必ずnよりも大きな素数が存在する（作れる）ことを示す。theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by... 素数が有限個しかないとして、それらの積に1を足した数を考えるとその素因数が元の素数の集合に含まれることから矛盾を導く（ユークリッド）。theorem primes…
有限の場合の総和記号について勉強したことで任意桁数の場合の3の倍数の確認方法について形式化して証明することが出来そうです。ということでやってみました。 まず与えられた自然数が3の倍数かどうかの確認方法と普通の証明をざっと述べてみます。 3の倍数の確認方法：$N, i, a_i$を自然数として$a_i$は各桁の数を表します。従って$\sum_{i=0}^{N-1} a_i\cdot 10^i$が与えられた自然数です。確認方法は、$$3 \sum_{i=0}^{N-1} a_i\cdot 10^i \iff 3 \sum_{i=0}^{N-1} a_i$$が成り立つので、右辺の和（各桁の数…
Mathmatics In Lean4の第5章 初等数論の2つ目の話題は帰納法と再帰です。自然数では定義が帰納的であること（自然数型は帰納型であること）を知ります。 inductive Nat zero : Nat succ (n : Nat) : Nat この意味は、0はNat型、Nat型の要素を1つとってnとするとsucc nもNat型です。そしてsucc n=0となるようなnはありません。ちなみにsucc nはn+1とも書かれます。 次にこの型の上で階乗関数を再帰的に定義します。 def fac : ℕ → ℕ 0 => 1 n + 1 => (n + 1) * fac …
まだ小学生の頃に習ったことで印象に残っているのは3の倍数の確認方法でした。各桁を足した数が3の倍数ならば元の数も3の倍数、というアレです。 倍数とか約数とかがLean4で扱えるようになり、この3の倍数の確認方法の証明を書き下してみようと思いました。自分で定理を形式化して証明を与えることを一通りやるには良いのではないかと思ったのです。 任意桁数の3の倍数で証明しようとすると、その数の10進数展開がk桁あるとして各桁を$a_n$とすると$\sum_{n=0}^{k-1} a_n\,10^n$と表すことができるところから始める必要があります。まだ$\sum$記号を勉強していないこともあり、えいやで3…
Mathematics in Lean 4で進めてきているLean4の勉強も第4章となり、初等整数論が扱えるところまで来ました。 最初の節では$\sqrt{2}$が無理数であることを示します。とはいってもこの段階で示すことは$\sqrt{2}$が有理数であるとして矛盾を導くことまでです。$\sqrt{2}$が実数の中に存在することまで示すわけではありません。 証明は古代ギリシャから知られているものです。$\sqrt{2}=\frac{m}{n}$となる互いに素な自然数$m,n$が存在するとします。すると $$m^2=2\,n^2$$ です。ここから$m$が偶数であることがわかります。$m=2\…
第4章「集合と関数」の最後のセクションはシュレーダー＝ベルンシュタインの定理のLean4による証明です。 初めてこの定理をきちんとした形で知りました。集合論の濃度に関する基本的な定理です。 定理：$\alpha, \beta$を集合、$f:\alpha \rightarrow\beta, g:\beta\rightarrow\alpha$が両方とも単射である時、$\alpha$から$\beta$への全単射がある。 集合の濃度に関して$ \alpha \ge \beta , \beta \ge \alpha $のとき$ \alpha = \beta $が成り立つということで確かに基本的です…
Mathematics in Leanの第4章「集合と関数」の中の2つ目のセクションである「関数」を読みながら練習問題を解いています。その問題の中で集合族の積集合の写像と集合族の写像の積集合に関する問題がありました。全称量化子と存在量化子が絡み、なかなか手強かったので、紹介したいと思います。 練習問題とその証明は下記のとおりです。 example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i := by01 intro y h102 simp at h103 simp04 have : (∃ x, (∀ (j : …
しばらく前のmacOSではbluetoothイヤフォンで音楽を楽しむ際、コーデック選択の問題で音質が悪い状況がありました。私もiMacとソニーのWF-1000MX4 の組み合わせでこの辺について色々と試してきています。 最近知ったのですが、この状況は少なくともmacOS Sonomaでは大きく改善された面もあり改善されていない面もあります。 以前のmacOSではbluetoothイヤフォンの(正確にはA2DPプロファイルで使う)デフォルトのコーデックがSBCでした。このためたとえイヤフォンがAACをサポートしていてもSBCで繋がってしまい、音が悪い、ということが発生していました。よく知られた改…
Mathematics in LeanもC04 Sets and Functionsの最初の章である集合まで辿り着きました。ここでは集合に関する性質の証明方法のLean4での実現の仕方を知ります。 集合が等しいこと(A=B)を示す場合、ゴールをA=Bとして方法として、AがBの部分集合であり、かつBがAの部分集合であることを示すこと AがBの部分集合であることを示すにはAの任意の要素がBの要素であることを示すこと 空集合と全体集合の性質 和集合と積集合をメンバーシップの論理和と論理積 集合族の積集合と和集合 のようなことがここでは解説されています。ここでは上記の初めの2つについて簡単な命題を示し…
Lean4を証明支援系として使っていても、型と証明の対応や関数型言語が突然現れることがあります。このことを知っていないと証明が読めないことがありました。 具体的には例えばある定理がこんな形だったとします。 def P (x:ℕ) : Prop := sorrytheorem theoA : ∀ x > 3, P x := sorry P xを命題としてxが3より大きい場合はP xが成り立つ、というのがtheoAという定理です。 当然P 4は4>3なので成り立つはずです。証明は普通はこんなふうにやると思うのです。 example : P 4 := by apply theoA -- ⊢ 4 > …
Lean4での論理記号の取り扱いの勉強も後半です。今回は論理積と論理和の扱いを見ていきます。この辺はあまり難しい話は出てきません。 ゴールが論理積A ∧ Bの形の場合にはconstructorタクティクを使うとAとBが両方ともゴールとなり両方証明するとA ∧ Bの証明が終わります。 仮定にh:A ∧ Bがある場合には仮定としてAとBが成り立つのですからバラしてそれぞれを仮定としたいですよね。仮定にh1:Aとh2:Bを入れるにはrcases h with <h1,h2>とかhave <h1,h2>:=hなどとすれば良いです。 ゴールが論理和A∨ Bの形の場合にはAかBのどちらかを証明できれば良い…
否定が論理式に含まれているとき使えるタクティクを勉強しました。 introタクティク：ゴールがある命題の否定¬ Aである場合、intro hとすると仮定h: Aが導入されて、ゴールがFalse (矛盾)に変わります。仮定の集まりの中で適当な命題Bについてhb:Bとhbn:¬ Bを両方含むようにできれば最後にapply hb hbnで矛盾を導いて証明が終わります。 by_contraタクティク：ゴールが特に否定の形ではない場合でも、by_contra hとすることでゴールの否定を仮定hとして導入するとともに、ゴールをFlase(矛盾)にすることができます。仮定の中で矛盾を導くことで証明を終了させ…
現役で最高の数学者のお一人で情報発信にも熱心なテレンスタオ教授のブログがあります。 terrytao.wordpress.com 残念ながら難しすぎて普段はほとんど見ない数学ブログですが、Lean4の勉強をしていたら検索で記事が1つヒットしました！ A slightly longer Lean 4 proof tour What's new 実数の2つの無限数列に関するある補題の証明をLean4を使って形式化して確認する、というものです。証明自体は望遠鏡和(telescoping sum)という手法を使ったものです。有限和をうまく作ると、実は隣り合った項が打ち消しあって最初と最後の項だけが…
ゴールに存在量化子が入っている場合、存在量化子がついた変数に値を入ることでゴールの論理式を証明することができます。useタクティクを使うと、「この値を使え」ということができます。例えばこんな感じです。 example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 -- ⊢ 2 < 5 / 2 ∧ 5 / 2 < 3 norm_num -- No goals ゴールの論理式の意味は「2より大きくて3より小さい実数xが存在する」です。まあ当たり前ですがどうやって証明するかです。この場合xが$\frac{5}{2}$であればこの不等式は確かに成立するので、xが存在…
今勉強しているMILの第3章「論理」では仮定の論理式やゴールの論理式に登場する論理記号をタクティクでどのように取り扱えば良いのかを説明しています。 この章の最初の方で説明されるのは全称量化子 ∀ です。ゴールの論理式にこの論理記号がついている場合、その変数や中身の式を証明することができません。そこで多くの場合には全称量化子 ∀を外してその中身にアクセスできるようにすることが証明の第一歩となります。 全称量化子 ∀がゴールの論理式に登場している場合、introタクティクを使うとその変数がラベル付きで導入されて、以降の証明で使えるようになります。 例えば前回見たcalcモードの説明の記事では偶関数…
前の記事でcalcモードがわかっていないと書きました。calcは便利そうなのでとりあえず簡単なユースケースを勉強しました。理解できたと思うのでメモを残しておきます。 Quantifiers and Equality - Theorem Proving in Lean 4にある説明を中心にして理解しました。最も典型的なユースケースは等式A=Bを証明する場合です。式Aから始めてタクティクを使って変形し、式Bを導ければ等式証明が成功します。等式変形なので使うタクティクはrwで、仮定や既知の定理を使って式変形します。 現在勉強中の第3章「論理」の中ので分かり易い例があったので紹介します。偶関数と奇関数…
数学の記事では普通は環境について書かないのですが、Lean4はプログラミング環境でもあるし、一応概要を記しておきます。 パソコン：M1 iMac (主記憶16GB), macOS 14.2.1 Lean (version 4.5.0-rc1) VS Code バージョン1.85.1 VS Code機能拡張Lean4 v0.0.124 起動中のVSCodeの様子はこんな感じです。縦分割の左から、フォルダ階層、Mathematics In Lean、練習ファイル、証明ゴール が表示されています。 MILの「2章 基本」の最後の練習問題である「距離関数は常にゼロ以上」の証明が終わったところが練習ファ…
"Mathematics In Lean"に沿ってLean4の証明支援系の勉強を進めています。まだ基本編で、今やっているのはmin, maxの性質の証明です。具体的には全順序集合上の関数min a b （a, bの小さい方を返す）について次の性質の証明です。 min a (min b c) = min (min a b) c 直感的には結局両辺ともa,b,cのうち最小の値を返しますから等しくなるのは納得です。一方この学習では以下の4つの性質だけから上記の性質を示すことが課題です。 le_antisymm : a $\le$ b $\land$ b $\le$ a $\iff$ a=b min_…
これからしばらくの間はLean4の証明支援系の勉強の話をシリーズ的に記事にします。相変わらず自分の勉強メモのような感じです。つまづいたところや感動したところを中心に書いていきます。 使用するテキストはMathematics In Lean(通称MIL)にしました。 Mathematics in Lean — Mathematics in Lean 0.1 documentation もう1つ、"Theorem Proving In Lean4"(通称TPIL)というテキストもありそちらは有志の皆様による日本語版もあります。両者の最大の違いは、MILはmathlib4という証明ライブラリも利用し…
年末は帰省していたのですが、有休含めて1/8までお休みにしたこともあり時間ができました。そこでLean 4を勉強してみることにしました。 Lean 4は以前このブログで紹介したLean 3と呼ばれる定理証明支援システムの後継システムです。 Lean 4からは関数型プログラミング言語としても使える、という触れ込みのようです。そこで今回はまず関数型プログラミング言語としてのLean 4を勉強してみました。勉強に使ったテキストは Functional Programming in Lean - Functional Programming in Lean です。このテキストを1章から4章まで読んでみ…
今回はいきなり第2補充則の証明から行きます。前回の記事 では第2補充則において$\sqrt{2}^p$の指数の$p$が変化するとそれに伴って平方剰余記号の値$\left(\frac{2}{p}\right)$が周期$8$で変化することを観察しました。 今回は山本先生の数論入門 (現代数学への入門)で紹介されている証明を見ていきます。ここでは$\sqrt{2}$を有限体$F_{p^2}$の中の$1$の原始$8$乗根の適当な和で表しています。これを$p$乗すると和の$p$乗は$p$乗の和を使い、$\sqrt{2}^p$を$1$の$8$乗根の$p$乗の適当な和で表すことができます。 これが周期$8$…
以下の式は$F_p$のフロべニウス写像によって$a$がいつ平方剰余になるのかを特徴づけているとも見えます。 $$\sqrt{a}^p=\left(\frac{a}{p}\right)\,\sqrt{a}\tag{A}$$ それが前回の記事の最後のステートメントでした。それらを再掲します。 「このことから第1補充則、第2補充則、相互法則をフロべニウス写像の言葉で言うと次のようになります。 $\sqrt{-1}^p=\sqrt{-1}$となる$p$の条件を求めること。 $\sqrt{2}^p=\sqrt{2}$となる$p$の条件を求めること。 $\sqrt{q^{\ast}}^p=\sqrt{q^…
ちょっとだけおさらいから入りましょう。 $p$を素数、$F_p$を 位数$p$の有限体とします。$F_p$の$0$以外の元の集合$F_p^{\times}$は位数$p-1$の巡回群になります。そうするとフェルマーの定理から任意の$x\in F_p$について$x^{p-1}=1$が分かります。両辺に$x$を掛ければ$x^p=x$となります。この式は$x=0$も含めて$F_p$の全ての元で成り立ちます。また$x^p=x$を$F_p$あるいはその拡大体での方程式と見た時、その解の個数は多項式の理論から高々$p$個です。一方、実際に$p$個の要素を持つ有限体$F_p$の元は全てこの方程式の解となってい…
いよいよこのシリーズも核心に入っていきます。今回は平方剰余の定義を与え、平方剰余記号を定義します。また平方剰余の基本的な性質を示した後、平方剰余の相互法則と関連する補充則などを紹介し、簡単なものには証明をつけます。最後に平方剰余の相互法則をより対称な形で表した命題を提示し、それが成り立つことをMaximaで再確認してみます。 定義 \(p\)を奇素数として\(a\)を\(p\)と互いに素な整数とします。\(a\)がある整数\(n\)の平方と法\(p\)で合同である時、\(a\)を\(p\)の平方剰余であるといいます。式で書けば、方程式\(X^2\equiv a\,(mod\,p)\)が解を持つ…
window.addEventListener('message', function(e) { var iframe = document.getElementById("tako"); var eventName = e.data[0]; var data = e.data[1]; switch(eventName) { case 'setHeight': console.log(data); iframe.style.height = data + "px"; break; } }, false); 前の記事で有限体\(F_p\)やその拡大体\(F_{p^f}\)で成り立つ幾つかの命題と…
駆け足で有限体を復習しましょう。 定義 有限体\(F_p\) 整数をある素数\(p\)で割った余りの集合\(\{0,1,\cdots,p-1\}\)には整数の加算や乗算の結果を\(p\)で割った余りとして自然に加算、乗算が定義でき、それらの単位元は\(0,1\)です。また全ての元に対して加算の逆元があり、\(0\)を除く全ての元に対して乗算の逆元があります。従って\(\{0,1,\cdots,p-1\}\)は体になります。この集合は要素数\(p\)の有限体であり記号\(F_p\)で表します。 具体的に\(p=3\)の有限体を例として考えてみましょう。\(F_3=\{0,1,2\}\)です。加算…
小島寛之先生のブログ記事 で山本芳彦先生の著書「数論入門」 数論入門 (現代数学への入門) 作者:山本 芳彦 岩波書店 Amazon が絶賛されていました。その中で印象に残ったのが、有限体を使った平方剰余の相互法則の証明が秀逸、という点でした。 山本先生のこの本にはこのブログの以前の記事でも色々とお世話になっていますが、平方剰余は個人的に苦手意識もありちゃんと読んでいませんでした。改めて第3章剰余環から読んでみました。1週間くらいかけて有限体の復習、平方剰余と\(F_p\)とフロべニウス写像\(x^p\)、有限体のガウス和、そして平方剰余の相互法則の証明を理解することができました。 その過程で…
昨年の11月にVMwareからVMware Fusion Player 13がリリースされました。VMware Fusion PlayerはmacOS上で仮想マシンを実行できるソフトウェアで、UTMやVirtualboxなどと同様のカテゴリの製品です。 store-jp.vmware.com セキュリティ関係でKali Linuxを使いたくてUTMにインストールしたのですが、Apple virtualizationではキーボードのマッピングが変で や_が入力できずshell操作がろくに出来ません。QEMUではキーボードはいいのですがスピードが遅くて困りました。 VMware Fusion Pl…
今年最後の記事は最近よく聴く楽曲の話です。 www.youtube.com Da-iCEのAnswersという楽曲です。最近お気に入りでよく聞いていたのですが、歌詞の中に「円周率」という言葉が聞こえることに気がつきました。おっ！と思って歌詞を調べてみると数学の用語が散りばめられていることがわかりました。 以下は数学に関係する単語とフレーズを抜き出してみたものです。 確率を知る為の公式、方程式、割り切れない円周率、導き出した答え、 理解して解くまでなどでもやり直そう 0をかけて台無しにしない 自然数、定義、数学 そもそも曲のタイトルがAnswersですね。数学をとても意識して作詞されたのでしょう…
この記事では最も簡単なシンギュラーモジュリ\(x_2\)を求めてみます。この値は前回の記事で求めた式 $$\frac{2}{\pi}=\sum_{k=0}^{\infty}(-1)^k\,A_k\,(4\,k+1), ただしA_k=\frac{\left( \frac12\right)_k^3}{k!^3}$$ でも使いました。 シンギュラーモジュリ\(x_2\)を求めるにあたりもう一度その定義を復習しておきましょう。アイゼンシュタイン級数の議論では一貫して次のような記号を定義して使ってきました。 $$q=e^{-y}, f(-q)=\prod_{n=1}^{\infty}(1-q^n), z…
