見出し画像

Lean4: ゼータ関数の収束性を形式的証明するコードのレビュー(Gemini 2.5 Pro)

D.

最適化、リファクタリング前のコードですがコンパイルが通って証明が完成したので、ここでどういうコードに仕上がったのかを説明してもらいました

Gemini によるコード解説

このLEAN4コードは、リーマンゼータ関数 $${\zeta(s) = \sum_{n=1}^{\infty} \frac{1}{n^s}}$$ が $${Re(s) > 1}$$ で収束することを証明するものです。実数の場合と複素数の場合に分けて、mathlibの既存の定理を活用して丁寧に証明を構築しています。

解説

以下にコードの各部分の分析と解説を示します。

１、インポートと準備

コードの冒頭では、証明に必要なmathlibの各種ライブラリをインポートしています。

import Mathlib.Analysis.SpecificLimits.Normed -- ノルム空間における極限や級数
import Mathlib.Analysis.PSeries -- べき級数、Real.summable_one_div_nat_rpow を含む
import Mathlib.Data.Real.Basic -- 実数
import Mathlib.Data.Complex.Basic -- 複素数
import Mathlib.Analysis.NormedSpace.Basic -- ノルム空間の基本、Summable.of_norm を含む
-- (ユーザーコメント: Mathlib.Analysis.NormedSpace.Real の代わりに .Basic が適切)
import Mathlib.Analysis.Normed.Field.Basic -- ノルム体、norm_div, norm_one を含む
import Mathlib.Analysis.Normed.Group.Basic -- ノルム群
import Mathlib.Analysis.SpecialFunctions.Pow.Real -- べき関数、Complex.norm_natCast_cpow_of_re_ne_zero を含む
import Mathlib.Analysis.SpecialFunctions.Gamma.Basic -- ガンマ関数 (このコードでは直接使用されていない)

open BigOperators Nat Real Complex -- 主要な記法や型を開く

これらのインポートにより、級数の収束性 (`Summable`)、ノルム (`norm`)、実数や複素数のべき (`^`)、および関連する定理（p級数テスト、絶対値の性質など）が利用可能になります。

２、実数 $${s > 1}$$ の場合の収束性

まず、変数が実数 $${s}$$ で $${s > 1}$$ の場合に、級数 $${\sum_{n=1}^{\infty} \frac{1}{n^s}}$$ が収束することを示しています。

-- 例：実数 s > 1 の場合に ζ(s) が収束することの証明
example {s : ℝ} (h_s_gt_one : 1 < s) :
    Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s) := by
  rw [Real.summable_one_div_nat_rpow]
  exact h_s_gt_one

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

  • 証明のポイント:

    • `Real.summable_one_div_nat_rpow` はmathlibの定理で、「級数 $${\sum_{k=0}^{\infty} \frac{1}{k^p}}$$ が収束することと $${p > 1}$$ は同値である」という内容です（`(Summable fun n => 1 / ↑n ^ p) ↔ 1 < p`）。

    • `rw [Real.summable_one_div_nat_rpow]` によって、証明すべきゴール `Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s)` が `1 < s` に書き換えられます。

    • 仮定 `h_s_gt_one` (または `h`) が `1 < s` そのものであるため、証明が完了します。

  • $${n=0}$$ の項について:

    • `fun n : ℕ` は $${n=0, 1, 2, \dots}$$ を動きます。

    • $${n=0}$$ のとき、項は `1 / (0 : ℝ) ^ s` となります。$${s > 1}$$ の仮定から $${s > 0}$$ なので、`(0 : ℝ) ^ s` は `0` です。LEAN4の除算の定義では `1 / 0` は `0` となるため、この $${n=0}$$ の項は `0` として扱われます。

    • したがって、この `Summable` は実質的に $${\sum_{n=1}^{\infty} \frac{1}{n^s}}$$ の収束性を示しており、リーマンゼータ関数の議論と整合します。

３、ゼータ関数の定義 (参考)

コードにはゼータ関数の定義も含まれています。

noncomputable def zeta_function (s : ℂ) : ℂ := tsum (fun n : ℕ+ ↦ 1 / (n : ℂ) ^ s)

  • この定義は `ℕ+` (正の自然数、つまり $n=1, 2, \dots$) を使っており、標準的なリーマンゼータ関数の定義 $${\sum_{n=1}^{\infty} \frac{1}{n^s}}$$ と一致しています。

  • `tsum` は級数の和を表します。この定義自体は収束性を保証するものではなく、収束する場合にその値を返します。

４、複素数 $${s}$$ で $${Re(s) > 1}$$ の場合の収束性

次に、変数が複素数 $${s}$$ で、その実部 $${Re(s)}$$ が $${1}$$ より大きい場合に、級数 $${\sum_{n=1}^{\infty} \frac{1}{n^s}}$$ が収束することを示しています。証明は絶対収束を利用します。つまり、$${\sum_{n=1}^{\infty} \left|\frac{1}{n^s}\right|}$$ が収束することを示し、それにより元の級数の収束を導きます。

example {s : ℂ} (hs_re_gt_one : 1 < s.re) :
    Summable (fun n : ℕ ↦ 1 / (n : ℂ) ^ s) := by
  -- 絶対収束、すなわち ∑ |1/n^s| の収束を示す。
  have h_abs_summable : Summable (fun n : ℕ ↦ norm (1 / (n : ℂ) ^ s)) := by
    have hs_re_pos : 0 < s.re := by linarith [hs_re_gt_one] -- 1 < s.re implies 0 < s.re
    have hs_re_ne_zero : s.re ≠ 0 := ne_of_gt hs_re_pos   -- 0 < s.re implies s.re ≠ 0
    simp_rw [norm_div] -- norm (1/z) = norm(1) / norm(z) = 1 / norm(z)
    
    -- 各自然数nに対してノルムを計算する補助的な等式
    have h_norm_pow (n : ℕ) : norm ((n : ℂ) ^ s) = (n : ℝ) ^ s.re := by
      apply Complex.norm_natCast_cpow_of_re_ne_zero n hs_re_ne_zero
    simp_rw [h_norm_pow] -- norm((n:ℂ)^s) を (n:ℝ)^s.re に書き換え
    simp_rw [norm_one]   -- norm(1) = 1 (分子の norm(1) を処理)
    
    -- ゴールは: Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s.re)
    rw [Real.summable_one_div_nat_rpow] -- 実数のp級数テストに帰着
    exact hs_re_gt_one -- 1 < s.re を使用

  -- 絶対収束するならば収束する (Summable.of_norm を使用)
  exact Summable.of_norm h_abs_summable

-- 同様の証明で定理も定義
theorem zeta_converges_complex (s : ℂ) (hs : 1 < s.re) :
    Summable (fun n : ℕ ↦ 1 / (n : ℂ) ^ s) := by
  -- (上記 example と同様の証明)
  have h_abs_summable : Summable (fun n : ℕ ↦ norm (1 / (n : ℂ) ^ s)) := by
    simp_rw [norm_div]
    have hs_re_pos : 0 < s.re := by linarith [hs]
    have hs_re_ne_zero : s.re ≠ 0 := ne_of_gt hs_re_pos
    have h_norm_pow (n : ℕ) : norm ((n : ℂ) ^ s) = (n : ℝ) ^ s.re := by
      apply Complex.norm_natCast_cpow_of_re_ne_zero n hs_re_ne_zero
    simp_rw [h_norm_pow, norm_one]
    rw [Real.summable_one_div_nat_rpow]
    exact hs
  exact Summable.of_norm h_abs_summable

  • 証明のステップ:

    1. 絶対収束の目標設定: `h_abs_summable` として `Summable (fun n : ℕ ↦ norm (1 / (n : ℂ) ^ s))` を示すことを目標にします。

    2. ノルムの変形:

      • `simp_rw [norm_div]` により `norm (1 / z)` を `norm 1 / norm z` (つまり `1 / norm z`) に変形します。

      • `h_norm_pow` という補助的な等式 `norm ((n : ℂ) ^ s) = (n : ℝ) ^ s.re` を証明し、適用します。

        • この証明には `Complex.norm_natCast_cpow_of_re_ne_zero n hs_re_ne_zero` が使われます。この定理は `‖(↑n : ℂ) ^ s‖ = (↑n : ℝ) ^ s.re` という等式を、$${s.re \neq 0}$$ の条件下で提供します。

        • 条件 $${s.re \neq 0}$$ は、仮定 $${1 < s.re}$$ から導かれる `hs_re_ne_zero` によって満たされます。

        • この等式は $${n=0}$$ の場合も、$${Re(s) > 0}$$ であれば $${0=0}$$ となり成立します。

      • `simp_rw [norm_one]` は分子の `norm 1` を `1` にします。

    3. 実数の場合に帰着: 上記の変形により、示すべき命題は `Summable (fun n : ℕ ↦ 1 / (n : ℝ) ^ s.re)` となります。

    4. p級数テストの適用: `rw [Real.summable_one_div_nat_rpow]` を使い、これを `1 < s.re` に書き換えます。これは仮定 `hs_re_gt_one` (または `hs`) そのものです。

    5. 絶対収束から収束へ: `Summable.of_norm h_abs_summable` により、「絶対収束する級数は収束する」という定理を用いて、元の級数の収束を結論付けます。

  • $${n=0}$$ の項について: 実数の場合と同様に、$${n=0}$$ の項 `1 / (0 : ℂ) ^ s` は $${Re(s) > 1}$$ の条件下では `0` と評価され、そのノルムも `0` です。したがって、ここでも実質的に $${\sum_{n=1}^{\infty} \frac{1}{n^s}}$$ の収束性を示しています。

５、全体的な評価とコメント

  • このコードは、mathlibの豊富な定理群を効果的に利用して、リーマンゼータ関数の基本的な収束条件をLEAN4で形式的に証明しています。

  • 証明の各ステップは明確で、標準的な数学の証明戦略（絶対収束、p級数テストへの帰着）に従っています。

  • `#check` や `#print axioms` は、定理の存在確認や公理依存性のチェックに役立つデバッグ手法です。

  • インポートに関しては、`Mathlib.Analysis.NormedSpace.Basic` が `Summable.of_norm` を提供するため、`Mathlib.Analysis.NormedSpace.Real` は必須ではないかもしれません。また、`Mathlib.Analysis.SpecialFunctions.Gamma.Basic` はこの特定の証明では使用されていません。

  • 使用されている `Complex.norm_natCast_cpow_of_re_ne_zero` は `Mathlib.Analysis.SpecialFunctions.Pow.Real` にあります。類似の定理として `Mathlib.Analysis.SpecialFunctions.Pow.Complex` にある `Complex.norm_nat_cpow_eq_of_re_pos` もあり、こちらを使うと $${s.re > 0}$$ という条件で直接適用できます。どちらを使っても証明は可能です。

このコードは、LEAN4を用いて数学的な命題を形式化し、証明する良い例となっています。

2025/06/01 14:08

D.


いいなと思ったら応援しよう！

D. 🐺賢狼👨‍✈️Copilot のご飯代を、私には🍺代を。 または 宇宙式 $N+u^d=(P+u)^d$ を使って新しい発見を！