Lean4: ゼータ関数Re(s)＞1収束証明の例

始めるわ！

ゆっくり学び中…😅ゆっくりすぎるか？作業の合間にちょいちょい触れてはいたのだけれども、コンパイルの通らない状況が９割でさっぱり解らない。
通ってもなぜ通ったかも理解できない。関数型言語にはほとんど触れてこなかっただけに作法がいまいち解っていない。

前回の内容

最初のステップ

ここで事前調査した最初の内容に、

形式化の難易度と具体的なステップ

1. リーマンゼータ関数の完全な形式化 (難易度: 高)

   • ステップ

     • $${\mathrm{Re}(s) > 1}$$ でのディリクレ級数 $${\sum_{n=1}^{\infty}{\frac{1}{n^s}}}$$ の定義と収束の証明。

という項目がありました。
この部分だけなら mathlib に既に実装されていそうな気もします…。

難易度：高　判定😅ノーマルではない

Lean4 を真面目に覚えるために自分で実装し、コンパイルを通すことで、
この険しい道のりを歩む難易度を実体験できます。ということでこれを実装し、気づいたことを記録していきます。

きっとこの道のりは緩やかな🏕️登山ではなく🧗‍♀️🌋垂直で危険な山です…。

収束

数学では収束することが前提のような世界です。発散無限であっても構造的であれば取り扱いは可能。なのだけど、その構造を想像するのは困難です。

という事で、まずはこの「ゼータ関数 $${ζ(s)}$$ が収束する」という事を Lean4 で形式化してみます。

ゼータ関数の収束

$$
\zeta(s) = \sum_{n=1}^{\infty}{\frac{1}{n^s}}, \quad \mathrm{Re}(s) > 1
$$

ゼータ関数は上記のように定義されます。概要は以下参照してください。

$${\mathrm{Re}(s) = 1}$$ は含みません。$${s=1}$$ は発散します。

という事で $${\mathrm{Re}(s) > 1}$$ の時の収束を Lean4 で形式的に証明する記述です。

Lean4

ζ(s), Re(s)>1 証明コード

import Mathlib.Analysis.SpecificLimits.Normed -- For summable_one_div_nat_rpow
import Mathlib.Analysis.PSeries
import Mathlib.Data.Real.Basic

open Nat -- For cast
open Real

example {s : ℝ} (h_s_gt_one : 1 < s) :
    Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s) := by
  rw [summable_one_div_nat_rpow]
  exact h_s_gt_one

theorem zeta_converges (s : ℝ) (h : 1 < s) :
    Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s) := by
  rw [summable_one_div_nat_rpow]
  exact h

ζ(s), Re(s)>1 コメント付きコード

import Mathlib.Analysis.SpecificLimits.Normed -- For summable_one_div_nat_rpow
import Mathlib.Analysis.PSeries
import Mathlib.Data.Real.Basic
-- import Mathlib.Data.Complex.Basic  -- For Complex numbers, if needed

-- open BigOperators -- For notation if needed, though not directly for summability
open Nat -- For cast
open Real

-- 例：実数 s > 1 の場合に ζ(s) が収束することの証明
example {s : ℝ} (h_s_gt_one : 1 < s) :
    Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s) := by
  -- mathlib の `summable_one_div_nat_rpow` は、
  -- ∑ (1 / n^p) が p > 1 で収束することを述べています。
  -- この関数は n=0 の項を含みますが、(0:ℝ)^s は s>0 のとき0であり、1/0は0として扱われるため、
  -- 実質的に n=1 からの和の収束性を示します。
  rw [summable_one_div_nat_rpow]
  exact h_s_gt_one

-- #print axioms summable_one_div_nat_rpow -- shows no axioms if fully proven
-- 'Real.summable_one_div_nat_rpow' depends on axioms: [propext, Classical.choice, Quot.sound]

-- この例では、実数 s > 1 の場合に ζ(s) が収束することを示しています。

theorem zeta_converges (s : ℝ) (h : 1 < s) :
    Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s) := by
  rw [summable_one_div_nat_rpow]
  exact h

-- この定理は、実数 s > 1 の場合に ζ(s) が収束することを示しています。
-- mathlib の既存の `summable_one_div_nat_rpow` 定理を使用しています。
-- Riemann zeta 関数の基本的な性質を示すものです。
-- この例と定理は、実数 s > 1 の場合に ζ(s) の級数が収束することを示しています。

コード解説

Lean4 の事に詳しいリーン・フォーリアちゃんに解説してもらいます。

🔍 コード全体の意味

この Lean コードは、実数 `s > 1` に対して

$$
\sum_{n=1}^{\infty} \frac{1}{n^s}
$$

が収束する（＝Summableである）ことを形式的に証明してるよ。

この級数は Riemann ζ関数 ζ(s) の定義で、実部が1より大きいときに収束するのは解析学でよく知られているよね。

💻 インポート部分

import Mathlib.Analysis.SpecificLimits.Normed -- summable_one_div_nat_rpow が定義されてる
import Mathlib.Analysis.PSeries              -- p級数の収束に関する定理たち
import Mathlib.Data.Real.Basic               -- ℝ型に関する基本定理
import Mathlib.Data.Complex.Basic            -- ℂとの型互換などのため（実際は使ってない）

ここでは、必要な定理（特に `summable_one_div_nat_rpow`）を使えるようにしてる。

🌸 `open` 節

open BigOperators -- ∑ 記法用（今回は使ってないけどあると便利）
open Nat          -- (n : ℝ) の coercion を明示的に使うため
open Real         -- ℝ の関数（たとえば log, pow など）を補完しやすくする

この `open` は namespace を開いて、いちいち `Real.pow` とか書かなくても済むようにしてる。

💡 メインの定理と証明

example {s : ℝ} (h_s_gt_one : 1 < s) :
    Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s) := by
  rw [summable_one_div_nat_rpow]
  exact h_s_gt_one

説明

• `s : ℝ` という実数が与えられていて、`1 < s` が仮定。

• そして `(fun n : ℕ ↦ 1 / (n : ℝ) ^ s)` という関数（つまり、p級数の項）を引数にして `Summable` を主張してる。

ここで重要なのは rw [summable_one_div_nat_rpow] の一行！

✅ summable_one_div_nat_rpow の意味

theorem summable_one_div_nat_rpow {p : ℝ} (hp : 1 < p) :
  Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ p)

これは $${\bold{p > 1}}$$ ならば、p級数が収束するという定理。
まさにこの例で使いたいもの！

☑ Lean の細かい動作：`n = 0` 問題

普通の ζ関数定義だと `n = 1` から和を取るけど、Lean では `ℕ = {0, 1, 2, ...}` だから、`n = 0` の項も含まれそうに見えるよね？

でも大丈夫。`(0 : ℝ) ^ s = 0` で、`1 / 0` は Lean では `0⁻¹ = 0`（任意のフィールドでは `0⁻¹ = 0` by convention）として扱われるので、実質的にはゼロ項を加えても和の収束には影響しないってこと。これがコメントにも書いてあるね：

-- n=0 の項を含みますが、(0:ℝ)^s は s>0 のとき0であり、1/0は0として扱われる

📌 最後の一行

-- #print axioms summable_one_div_nat_rpow -- shows no axioms if fully proven

これは、`summable_one_div_nat_rpow` が証明付きの定理（axiom free）であることを確認するためのチェックだね。ちゃんと mathlib で証明されてるので、安心して使えるよっていう意味。

✅ まとめ読み方

example {s : ℝ} (h_s_gt_one : 1 < s) :
    Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s) := by
  rw [summable_one_div_nat_rpow]
  exact h_s_gt_one

この証明は、「p級数が1より大きいときに収束する」という mathlib の定理をそのまま使ってる。`rw` で `summable_one_div_nat_rpow` を適用できる形にしてから、仮定 `h_s_gt_one` を `exact` で使ってる。タクティク的にもシンプルで読みやすい証明だね♪

📖 example と theorem

✅ `example` とは何か？

example {s : ℝ} (h_s_gt_one : 1 < s) :
    Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s) := by
  ...

これは「仮定 `1 < s` のもとで、`∑ 1 / n^s` が収束することを示す例だよ」という意味。

✨ 特徴

🧠 Lean 的に言うと

`example : T := t` は、型 `T` の値を与える式 `t` を書くということ。つまり、命題 `T` に対する「証明項」を与えてるだけ。命題は型、証明は項、という Curry-Howard 同型対応（型＝命題、項＝証明）に基づいてる。

🛠 例を theorem に書き換えると

theorem zeta_converges (s : ℝ) (h : 1 < s) :
    Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s) := by
  rw [summable_one_div_nat_rpow]
  exact h

こうすれば `zeta_converges` という名前がついて、あとから `apply zeta_converges` とかで使えるようになるよ。

✨ まとめ

• `example` は証明のスニペットを書くための 無名の証明ブロック。

• 学習やテスト、ちょっとした確認に便利。

• 再利用したいなら `theorem` や `def` を使おう！

Lean 書いてると `example` で気軽に試してから、あとで `theorem` に昇格させるってのがよくある流れだよ〜。

✍️ rw (rewrite)

`rw`（`rewrite` の略）は、Lean の tactic スクリプトで「等式を使って式を書き換える」ための基本的な戦術だよ！

たとえばこんな感じ：

example (a b c : ℕ) (h : a = b) : a + c = b + c := by
  rw [h]

この場合、`h : a = b` っていう仮定を使って、`a + c` の中の `a` を `b` に書き換えてる。

ポイントまとめ

• `rw [h]` は 「等式 `h : lhs = rhs` を使って、式中の `lhs` を `rhs` に書き換える」

• 複数同時に書ける： `rw [h1, h2, ← h3]`

  • `←` をつけると逆方向に書き換える（`rhs = lhs` を使う）

• コンテキストにある仮定も使えるし、定理の名前も使える

例：定理を使う場合

example (x : ℝ) : x + 0 = x := by
  rw [add_zero]

この `add_zero : ∀ x, x + 0 = x` という定理を使って書き換えてるよ。

もっと複雑な構造の中で rewrite をする場合は、`rw` よりも `simp` とか `conv` を使った方がいいこともあるけど、`rw` は基本でよく使う！

他にも気になる動作とかあれば教えて〜

✍️ #print axioms

この出力は Lean が `summable_one_div_nat_rpow` の証明に どんな公理（axioms） を使っているかを教えてくれるもので、とっても大事な情報だよ！

🔍 出力の意味

'Real.summable_one_div_nat_rpow' depends on axioms: [propext, Classical.choice, Quot.sound]

これは「この定理（`Real.summable_one_div_nat_rpow`）の証明には以下の3つの公理が使われてるよ」という意味：

１、propext

• 意味：命題 `P ↔ Q` が証明されたら、それを同値として使って `P = Q` と見なせる、という公理。

• 用途：`Prop` 型の等号を扱うときに必要。

• 安全性：Lean の標準公理で、純粋な構成的意味では問題ない。基本的に使ってても安心。

２、Classical.choice

• 意味：選択公理 `∀ α (p : α → Prop), (∃ x, p x) → (∃ f : ℕ → α, ∀ n, p (f n))` のバージョン。

• 用途：明示的に構成できないけど存在は言える要素（たとえば補題で「存在する」とだけ言ってるようなやつ）を「選ぶ」時に使われる。

• 安全性：これは 構成的でない（非constructive） けど、解析や実数の収束性の話にはよく使われる。ζ関数とかにも普通に出てくるから問題ない。

３、Quot.sound

• 意味：`Quot` 型（同値類）における等価性の扱いを保証するための公理。

• 用途：型の quotient（たとえば有理数 ℚ = ℤ × ℕ / ~）みたいなのを扱う時に登場する。

• 安全性：これも mathlib の中でよく使われていて、依存していても普通は問題なし。

🧠 つまり何がわかる？

• `summable_one_div_nat_rpow` は mathlib 内で 完全に証明済み
  （＝admittedとか未証明じゃない）。

• でも証明の過程では、「構成的でない原理」や「等価関係の quotient」など、現代数学でごく普通に使われる原理を仮定している。

• とくに解析的な話題では `Classical.choice` はほぼ不可避だから、心配いらないよ。

✅ 実用上のまとめ

• この定理は信頼できる（"axiom-free" ではないけど、"数学的に健全"）。

• 形式的には `Prop` と `Setoid` の扱いに関するちょっとした非構成的部分が含まれているだけ。

• ζ関数や級数収束の形式化においては、この程度の axioms 使用は
  全く問題なし！

他に気になる定理があったら `#print axioms` でチェックしていくと楽しいよ〜。Lean の公理依存を追うのは証明の「健全性保証」の目安にもなるし！

💡 仮定からの exact

exact は Lean の証明タクティックの中でもとっても基本的かつ大事なやつ！とくに「仮定からゴールをそのまま満たせるとき」に使うよ。

✅ exact の基本形

example (h : P) : P := by
  exact h

これは「仮定 `h : P` があるから、そのまま `P` を証明できるよね」ってこと。証明すべき型（命題）と、与えられた項の型が一致しているときに使える。

🔎 今回の例で見ると

example {s : ℝ} (h_s_gt_one : 1 < s) :
    Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s) := by
  rw [summable_one_div_nat_rpow]
  exact h_s_gt_one

ここでの `exact h_s_gt_one` の意味は：

• `rw [summable_one_div_nat_rpow]` をしたことで、ゴール（証明すべき命題）が `1 < s` に変わった。

• それとちょうど同じ仮定 `h_s_gt_one : 1 < s` を持ってる。

• だから `exact h_s_gt_one` で証明完了！

💡 一歩踏み込むと…

`exact t` は「今のゴールを満たす型の項 `t` を明示的に与える」という意味で、証明の最終ステップにぴったり。

たとえばこの例：

example (x : ℕ) (h : x = 3) : x = 3 := by
  exact h

ゴールが `x = 3`、仮定が `h : x = 3`。ピッタリ一致。だから `exact`！

❌ 一致しない場合は？

もし型が一致してないときに `exact` を使おうとすると、Lean は：

type mismatch, term has type A but is expected to have type B

って言ってくる。これは「ゴールと与えた項の型が違うよ」って意味ね。

🎓 練習っぽい例

example (a b : ℝ) (h : a = b) : b = a := by
  exact h.symm

ここでは仮定 `a = b` をそのまま使えないけど、`h.symm : b = a` にすれば使える。`exact` は「その型の証明項を直接与える」っていう性質上、使うには型をぴったり合わせる必要があるんだ。

✨ まとめ

慣れてくると `exact` は証明の「終止符」みたいな感じで、綺麗にピタッとゴールを閉じると気持ちいいよ♡

🥅⚽ タクティック(tactic) というもの

tactic（タクティック）は、Lean の証明環境で「ゴールを操作するための命令（コマンド）」のことだよ。証明の途中で出てくるゴール（証明すべき命題）を、簡単なものに分解したり、前提を使って証明したりするために使うの。

例えば：

example (P Q : Prop) (h : P) : P ∨ Q := by
  left
  exact h

ここで使ってる `left` や `exact h` が tactic だよ。

ざっくり言うと、tactic にはこういう役割があるの：

• ゴールを分解：`intro`, `cases`, `split` など

• ゴールを解決：`exact`, `apply`, `rfl`, `refl`, `assumption` など

• ゴールや仮定を変形：`rewrite`, `simp`, `rw` など

• 複数のゴールを管理：`all_goals`, `any_goals`, `focus` など

Lean では証明を `term mode`（項で直接書く）と `tactic mode`（by 以下で手続き的に書く）に分けられて、tactic mode は直感的に操作できるから人気だよ。

まとめ

こんな短い内容に情報豊富…。

ここまでの実装で四苦八苦しながら解ったこと

1. mathlib の実装内容を知っていなければならない！という前提知識🧠

2. mathlib の実装状況が現在どうなっているか？
   📃最新ドキュメントと実装、そしてそれらが数学の、

   • 補題・定理 (lemma, theorem)

   • 定義 (def)

   • 証明 (tactic)
     これらとの関連を知る必要がある。

3. バージョンの違いにより実装が大きく異なる
   AI のサンプルコードの大半がそのまま動かないのは、このライブラリのバージョン差異（学習時期や状況の違いからか？）提示されたコードには存在しない定理が使われていたり未定義エラーとして出てくる事が多い。

...
@[deprecated (since := "2025-02-17")] alias abs_cpow_of_ne_zero := norm_cpow_of_ne_zero
@[deprecated (since := "2025-02-17")] alias abs_cpow_of_imp := norm_cpow_of_imp
@[deprecated (since := "2025-02-17")] alias abs_cpow_le := norm_cpow_le
@[deprecated (since := "2025-02-17")] alias abs_cpow_real := norm_cpow_real
@[deprecated (since := "2025-02-17")] alias abs_cpow_inv_nat := norm_cpow_inv_nat
@[deprecated (since := "2025-02-17")] alias abs_cpow_eq_rpow_re_of_pos :=
  norm_cpow_eq_rpow_re_of_pos

@[deprecated (since := "2025-02-17")] alias abs_cpow_eq_rpow_re_of_nonneg :=
  norm_cpow_eq_rpow_re_of_nonneg
...

VSCode 拡張機能 LEAN4 の LoogleSearch を活用してそれらを探し当てる
見つかっても、記述された定理などの内容が理解できなければどれか判別不可能なので数学の知識が要求される😅

当然、数学未解明の問題についてはライブラリ化されていない。
抽象数学などの最新数学理論も実装されていない。

つまりこれからやろうとすることは、この未実装の実装を行う。という話。
そりゃ険しい道のりなわけですよ…。😨

どこまでやれるのだろう…。

（2025/06/01 14:23 追記）

実装結果

最初のステップを乗り越えた！無事コンパイルの通るコードが書けました。

実行結果

この証明以外に、偏角変換や π-Jump 検索、観測など、いままでのリーマン予想解明で使用したリーマン予想原理的構造の部分実装済みのコードに追記したのでいろんな出力が出てますが、こちらも追々紹介と解説交えて書いていこうと思います。

info: ././././ZetaLogic/RZF.lean:19:0: Real.summable_one_div_nat_rpow {p : ℝ} : (Summable fun n ↦ 1 / ↑n ^ p) ↔ 1 < p
info: ././././ZetaLogic/RZF.lean:31:0: 'Real.summable_one_div_nat_rpow' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ././././ZetaLogic/RZF.lean:38:0: 'zeta_converges_real' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ././././ZetaLogic/RZF.lean:52:0: Complex.norm_natCast_cpow_of_re_ne_zero (n : ℕ) {s : ℂ} (hs : s.re ≠ 0) : ‖↑n ^ s‖ = ↑n ^ s.re
info: ././././ZetaLogic/RZF.lean:53:0: Complex.abs_re_eq_norm {z : ℂ} : |z.re| = ‖z‖ ↔ z.im = 0
info: ././././ZetaLogic/RZF.lean:54:0: norm_div.{u_2} {α : Type u_2} [NormedDivisionRing α] (a b : α) : ‖a / b‖ = ‖a‖ / ‖b‖
info: ././././ZetaLogic/RZF.lean:55:0: Real.summable_one_div_nat_rpow {p : ℝ} : (Summable fun n ↦ 1 / ↑n ^ p) ↔ 1 < p
info: ././././ZetaLogic/RZF.lean:87:0: 'Complex.norm_natCast_cpow_of_re_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ././././ZetaLogic/RZF.lean:108:0: 'zeta_converges_complex' depends on axioms: [propext, Classical.choice, Quot.sound]

Build completed successfully.
lake exe zetalogic
Zeta sum at t=14.134725: -0.644382 + -2.141575i
Arg: -1.863071
Scanning for phase jumps near known zero t ≈ 14.134725...
unwrap: Scanning from 13.000000 to 15.000000 with step 0.000100 and N = 1000...
Phase jump detected: t = 14.310600, Δarg ≈ 6.282461
Orig: Scanning from 13.000000 to 15.000000 with step 0.000100 and N = 1000...
Phase jump detected: t = 13.438900, Δarg ≈ 6.282400
Phase jump detected: t = 14.310600, Δarg ≈ 6.282461
unwrap: Scanning from 13.000000 to 15.000000 with step 0.000100 and N = 5000...
Phase jump detected: t = 13.832700, Δarg ≈ 6.282310
Phase jump detected: t = 14.557100, Δarg ≈ 6.282315
Orig: Scanning from 13.000000 to 15.000000 with step 0.000100 and N = 5000...
Phase jump detected: t = 13.103100, Δarg ≈ 6.282261
Phase jump detected: t = 13.832700, Δarg ≈ 6.282310
Phase jump detected: t = 14.557100, Δarg ≈ 6.282315
Orig: Scanning from 10.000000 to 11.000000 with step 0.000100 and N = 1000...
Orig: Scanning from 11.000000 to 12.000000 with step 0.000100 and N = 1000...
Orig: Scanning from 12.000000 to 13.000000 with step 0.000100 and N = 1000...
Phase jump detected: t = 12.543900, Δarg ≈ 6.282204
Orig: Scanning from 13.000000 to 14.000000 with step 0.000100 and N = 1000...
Phase jump detected: t = 13.438900, Δarg ≈ 6.282400
Orig: Scanning from 14.000000 to 15.000000 with step 0.000100 and N = 1000...
Phase jump detected: t = 14.310600, Δarg ≈ 6.282461
Orig: Scanning from 15.000000 to 16.000000 with step 0.000100 and N = 1000...
Phase jump detected: t = 15.170200, Δarg ≈ 6.282350
Orig: Scanning from 16.000000 to 17.000000 with step 0.000100 and N = 1000...
Orig: Scanning from 17.000000 to 18.000000 with step 0.000100 and N = 1000...
Orig: Scanning from 18.000000 to 19.000000 with step 0.000100 and N = 1000...
Orig: Scanning from 19.000000 to 20.000000 with step 0.000100 and N = 1000...
Result a: -0.644008 + -2.141710i
Result b: -0.638643 + -2.126892i

2025/06/01  5:16

D.