級数と不等式 — 実解析を避けて係数比較に落とす

次の三つの級数を考えます。係数の分母が階乗の積で、二つ目・三つ目は一つ目を一回・二回微分したものです。

x ≥ 0 のとき、F₁(x)² − F₀(x)·F₂(x) ≥ 0 か。
（これは log F₀ が凹であること——(log F₀)'' ≤ 0——と同じ内容です。）

F₀ は修正 Bessel 関数 I₁ の変数変換で、この不等式は Turán 型と呼ばれる形（I₂² ≥ I₁I₃）に当たります。既知不等式そのものは既知です（Baricz–Ponnusamy, arXiv:1010.3346。題と要旨を確認しました。係数比較による証明の初出は未確認です）。ここで説明するのはLean への載せ方で、新しい数学の主張はありません。

格子の上の場の理論で、一リンク積分から強結合域の定数を出す途中に現れる部品です。連続極限や質量ギャップ——ミレニアム問題の本体——への主張はありません。

係数を a_k = 1/(k!(k+1)!)・b_k = 1/(k!(k+2)!)・d_k = 1/(k!(k+3)!) と書きます。F₁² − F₀F₂ は二つの級数の積の差なので、Cauchy 積で xⁿ の係数が書けます。

階乗を払うと、この和は二項係数の和になります。

右辺はずらし付きの Vandermonde の恒等式（Σ_k C(n,k) C(m,k+r) = C(n+m, n+r)）で畳めます。

Cat は Catalan 数です。すべての係数が正なので、x ≥ 0 なら和も非負になります。紙では 4 行です。

この道の値打ちは、Bessel 関数の性質を一つも使っていないことです。無限積の表示（零点による積分解）にも、零点が実であることにも頼りません。使うのは二項係数の恒等式と、級数の積の係数の公式だけです。

設計の分かれ目は最初の一つです。Bessel 関数を Lean に持ち込むか、級数を手で定義するか。

mathlib に修正 Bessel 関数の定義はありません。近いものとして超幾何関数の正規化版がありますが、複素関数として組まれているので、実数の不等式に使うには変換が要ります。一方、級数を tsum（無限和）で手で定義するのは十数行です。

級数を手で定義する側を選びました。理由は、紙の証明が Bessel 関数の性質を使っていないからです。証明が使っていないものを型に持ち込むと、持ち込んだぶんの整合性を証明する仕事が増えます。ここでは F₀(κ²/4) = 2I₁(κ)/κ という同定を Lean の外に置き、Lean の中は級数の話で閉じています。

そのぶん、Lean の中では三つの仕事が要ります。

• 可総和性——tsum は和が収束しない場合に 0 を返す約束なので、収束を別に証明しないと式が意味を持ちません。1/k! との比較で出ます。
• 項別微分——F₀ を微分すると F₁ になることは、項ごとに微分してよいという定理（hasDerivAt_tsum_of_isPreconnected）を球の上で当てます。優級数は k Rᵏ⁻¹/k! です。
• Cauchy 積——級数の積を係数の畳み込みに直す定理（tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm）を二回使います。ノルムの可総和性が仮定なので、可総和性の仕事が先に済んでいる必要があります。

三つとも「紙では書かない段」です。紙の 4 行のうち、増えるのはここだけで、二項係数の側は紙と同じ長さで済みます。

二項係数の段は ℤ で述べる

紙の式に C(2n+4, n+2) − C(2n+4, n+1) という引き算が出ます。二項係数は自然数なので、素直に書くと自然数の引き算になります。自然数の引き算は 0 で止まるので（04 と同じ罠です）、引き算が出る側を ℤ で述べます。

/-- ずらし `r` つきの Vandermonde（自然数のまま）。 -/
theorem vdm (n m r : ℕ) :
    ∑ k ∈ range (n + 1), n.choose k * m.choose (k + r) = (n + m).choose (n + r)

/-- 係数の分子（`ℤ` で述べる。引き算が出るため）。 -/
theorem B1 (n : ℕ) :
    ∑ j ∈ range (n + 1),
        (n.choose j : ℤ) * (((n + 4).choose (j + 2) : ℤ) - ((n + 4).choose (j + 1) : ℤ))
      = ((2 * n + 4).choose (n + 2) : ℤ) - ((2 * n + 4).choose (n + 1) : ℤ)

/-- その値は Catalan 数。 -/
theorem B1_catalan (n : ℕ) :
    ((2 * n + 4).choose (n + 2) : ℤ) - ((2 * n + 4).choose (n + 1) : ℤ) = (catalan (n + 2) : ℤ)

Vandermonde の側は自然数のままでよく、引き算が現れる B1 だけを ℤ にしています。全部を ℤ にすると、帰納法や Pascal の漸化式のたびに型変換が入ります。型を移すのは、引き算が要る場所だけにします。

係数の恒等式は標数 0 の体で述べる

係数 a_k などは割り算を含むので、体の中で述べる必要があります。ℝ で述べてもよいのですが、標数 0 の体 K のままにしておきました。こうすると同じ補題が ℚ でも ℝ でも使えます。係数が正であることを有理数で確かめ、級数の不等式を実数で述べる——という使い分けができます。

形式的冪級数を経由する

係数の計算は、収束を気にしない形式的冪級数（PowerSeries）の上で済ませました。「係数がこうなる」は収束と無関係な代数の事実です。そこを先に閉じておくと、実解析の側は「係数が分かっている級数の和」を扱うだけになります。

/-- `F` の係数。 -/
noncomputable def a (k : ℕ) : K := 1 / ((k.factorial : K) * ((k + 1).factorial : K))
/-- `F'` の係数。 -/
noncomputable def b (k : ℕ) : K := 1 / ((k.factorial : K) * ((k + 2).factorial : K))
/-- `F''` の係数。 -/
noncomputable def d (k : ℕ) : K := 1 / ((k.factorial : K) * ((k + 3).factorial : K))

/-- 形式的冪級数 `F = ∑ x^k/(k!(k+1)!)`。 -/
noncomputable def Fps : K⟦X⟧ := PowerSeries.mk (a K)

/-- `(F')² − F·F''` の `x^n` の係数は `Cat(n+2)/(n!(n+4)!)`。 -/
theorem coeff_turan (n : ℕ) :
    coeff n ((d⁄dX K (Fps K)) ^ 2 - Fps K * d⁄dX K (d⁄dX K (Fps K)))
      = (catalan (n + 2) : K) / ((n.factorial : K) * ((n + 4).factorial : K))

d⁄dX は mathlib の形式的冪級数の微分の記法で、K⟦X⟧ が K 係数の形式的冪級数の型です。収束の話が一つも出てこないまま、係数の等式が閉じています。

級数の定義と、微分の関係。

/-- `F`。 -/
noncomputable def F0 (x : ℝ) : ℝ := ∑' k, a ℝ k * x ^ k
/-- `F'`。 -/
noncomputable def F1 (x : ℝ) : ℝ := ∑' k, b ℝ k * x ^ k
/-- `F''`。 -/
noncomputable def F2 (x : ℝ) : ℝ := ∑' k, d ℝ k * x ^ k

/-- 係数列が `|c k| ≤ 1/k!` を満たすとき、項別に微分してよい。 -/
theorem hasDerivAt_series (hc : ∀ k, |c k| ≤ 1 / (k.factorial : ℝ)) (x : ℝ) :
    HasDerivAt (fun y => ∑' k, c k * y ^ k) (∑' k : ℕ, ((k : ℝ) + 1) * c (k + 1) * x ^ k) x

theorem hasDerivAt_F0 (x : ℝ) : HasDerivAt F0 (F1 x) x
theorem hasDerivAt_F1 (x : ℝ) : HasDerivAt F1 (F2 x) x

本体の二本。等式の形で先に出し、そこから不等式を出します。

/-- **Turán 型の等式**：すべての実 `x` で成り立つ。 -/
theorem turan_series (x : ℝ) :
    F1 x ^ 2 - F0 x * F2 x
      = ∑' n : ℕ, (catalan (n + 2) : ℝ) / ((n.factorial : ℝ) * ((n + 4).factorial : ℝ)) * x ^ n

/-- **Turán 型の不等式**：`x ≥ 0` で非負。 -/
theorem turan_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ F1 x ^ 2 - F0 x * F2 x

/-- もう一つの不等式：`x ≥ 0` で `2 F1 ≤ F0`。 -/
theorem two_F1_le_F0 {x : ℝ} (hx : 0 ≤ x) : 2 * F1 x ≤ F0 x

LeanOneLinkSeries.vdm・B1・B1_catalan・cauchy_coeff_catalan・hasDerivAt_F0・hasDerivAt_F1・turan_series・turan_nonneg・two_F1_le_F0。

turan_series が等式で、x に条件が付いていないことが設計の成果です。非負性は「係数が非負な級数を x ≥ 0 で足す」という一行に落ちます。もし不等式を直接証明しようとすると、x の場合分けが証明の中に入り込みます。等式で出しておくと、条件は最後の一行にだけ現れます。

Vandermonde の側

vdm は n についての帰納法で閉じます。効いたのは三点です。

• r を一般化してから帰納する。r を固定すると帰納の仮定が使えません。r を ∀ のまま回すと、Pascal の漸化式で出る二つの項がどちらも仮定の形になります。
• Pascal は Nat.choose_succ_succ' を使う。向きが二つあり、和の添字のずらしと合う側を選びます。
• 和の端を落とすのは Finset.sum_range_succ'。後ろの端を落とす Finset.sum_range_succ と、前の端を落とす ' つきがあり、ここでは前を落とします。

mathlib には Nat.add_choose_eq（反対角の形の Vandermonde）もありますが、端の項を落として対称性で移す手数より、帰納法のほうが短くなりました。「在る補題を探して当てる」と「自分で帰納する」のどちらが短いかは、当ててみないと分かりません。

階乗を払う段

紙で「階乗を払う」と一言で書いた段が、Lean ではいちばん手が掛かります。やってはいけないのは、階乗の式に field_simp を直接掛けることです。分母が k! のような再帰的な項なので、展開が止まりません。

そこで、階乗を「体の元」に一般化した補助補題を先に立てました。P · f_i · f_j = N と Q · f_i' · f_j' = M から N · M · (1/(f_i f_i')) · (1/(f_j f_j')) = P · Q を出す、という形です。階乗であることを忘れさせてから field_simp を掛けます。具体的な階乗の等式（Nat.add_choose_mul_factorial_mul_factorial）は、この補助補題に三回流し込みます。

Cauchy 積と非負性

theorem turan_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ F1 x ^ 2 - F0 x * F2 x := by
  rw [turan_series]
  exact tsum_nonneg fun n => mul_nonneg (by positivity) (pow_nonneg hx n)

二行です。rw [turan_series] で等式に書き換え、tsum_nonneg（項がすべて非負なら和も非負）を当て、項ごとの非負性は「係数が非負」と「xⁿ が非負」の積に分けます。x ≥ 0 を使うのは pow_nonneg hx n の一箇所だけです。仮定がどこで効いているかが、この一語で見えます。

turan_series の側では、Cauchy 積の定理を二回（F₁·F₁ と F₀·F₂）使い、Summable.tsum_sub で差を取り、係数の等式（cauchy_coeff_catalan）で畳みます。Cauchy 積の定理はノルムの可総和性を仮定するので、可総和性の補題が先に要ります。

紙の 4 行のうち、二項係数の段は小さな数で確かめられます。n = 3・m = 7・r = 2 で Vandermonde を見ます。

import Mathlib

open Finset Nat

/-- ずらし `r` つきの Vandermonde を `n = 3`・`m = 7`・`r = 2` で見たもの。 -/
example : ∑ k ∈ range 4, Nat.choose 3 k * Nat.choose 7 (k + 2) = Nat.choose 10 5 := by decide

/-- 係数の分子が Catalan 数になること（`n = 0` と `n = 1`）。 -/
example : (Nat.choose 4 2 : ℤ) - Nat.choose 4 1 = catalan 2 := by
  rw [catalan_two]; decide
example : (Nat.choose 6 3 : ℤ) - Nat.choose 6 2 = catalan 3 := by
  rw [catalan_three]; decide

Lean手元で検査して通ったもの。21 + 105 + 105 + 21 = 252 = C(10,5) です。catalan をそのまま decide に渡すと止まります——mathlib の catalan は整礎再帰で定義されているので kernel が展開しません。値を与える補題（catalan_two・catalan_three）で先に置き換えます。「有限の値だから decide で出る」は、定義の書き方によっては成り立ちません。

もう一つの不等式（2 F₁ ≤ F₀）の芯も、係数の恒等式です。これは k について一般に成り立つので、ℚ で確かめられます。

/-- 係数の引き算が「同じ係数の `k/(k+2)` 倍」になること（`ℚ` で・全ての `k`）。 -/
example (k : ℕ) : (1 : ℚ) / (k ! * (k + 1)!) - 2 / (k ! * (k + 2)!)
    = (1 / (k ! * (k + 1)!)) * (k / (k + 2)) := by
  have h2 : (((k + 2)! : ℕ) : ℚ) = (k + 2) * ((k + 1)! : ℕ) := by
    rw [Nat.factorial_succ]; push_cast; ring
  have hk : ((k ! : ℕ) : ℚ) ≠ 0 := Nat.cast_ne_zero.2 (Nat.factorial_ne_zero k)
  have hk1 : (((k + 1)! : ℕ) : ℚ) ≠ 0 := Nat.cast_ne_zero.2 (Nat.factorial_ne_zero _)
  have hk2 : ((k : ℚ) + 2) ≠ 0 := by positivity
  rw [h2]
  field_simp
  ring

右辺が非負なので、a_k − 2 b_k ≥ 0 がすべての k で成り立ちます。field_simp を掛ける前に (k+2)! = (k+2)·(k+1)! を手で入れているのが、上で書いた「階乗のまま field_simp を掛けない」の実物です。分母が k! と (k+1)! だけになってから掛けます。

可総和性のほうも短く確かめられます。

/-- 係数列の可総和性は `1/k!` との比較で出る（`(k+1)! ≥ 1` を捨てるだけ）。 -/
example (x : ℝ) : Summable (fun k : ℕ => x ^ k / ((k ! : ℝ) * ((k + 1)! : ℝ))) := by
  refine Summable.of_norm_bounded (Real.summable_pow_div_factorial |x|) ?_
  intro k
  have hk : (0:ℝ) < (k ! : ℕ) := by exact_mod_cast k.factorial_pos
  have hk1 : (1:ℝ) ≤ ((k + 1)! : ℕ) := by exact_mod_cast (k + 1).factorial_pos
  rw [Real.norm_eq_abs, abs_div, abs_pow, abs_mul, abs_of_pos hk,
    abs_of_pos (by exact_mod_cast (k + 1).factorial_pos : (0:ℝ) < ((k + 1)! : ℕ))]
  gcongr
  nlinarith [hk, hk1]

Lean手元で検査して通ったもの。Real.summable_pow_div_factorial（Σ |x|ᵏ/k! は収束する）に、項ごとの比較を添えるだけです。比較する相手を 1/k! に選ぶと、落とすのは (k+1)! ≥ 1 の一つだけになります。

lake env lean LatticeGaugeOneLink.lean

3,979 行・エラー 0・警告 0・約 58 秒。公理の出力から数本を抜きます。

'OneLinkSeries.vdm' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.B1' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.B1_catalan' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.cauchy_coeff_catalan' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.hasDerivAt_F0' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.turan_series' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.turan_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]

すべて標準三公理の内側で、sorryAx と Lean.ofReduceBool はありません。実数の解析を扱う証明では Classical.choice がほぼ必ず出ます——実数そのものの構成や、tsum の定義（収束しない場合に 0 を返す約束）が選択公理を経由するためです。05 の組合せの補題では出ていなかったのと対比になります。

turan_nonneg が言っているのは次のことです。

実数 x ≥ 0 について、F1 x ^ 2 - F0 x * F2 x は 0 以上である。ここで F0・F1・F2 は、この Lean ファイルの中で tsum によって定義された関数である。

言っていないことを三つ。

• x < 0 については何も言っていません。仮定 0 ≤ x は落とせません。もう一方の不等式（2 F₁ ≤ F₀）は x = −30 で実際に破れます（F₀ − 2F₁ = −0.041…）。計算この端末で数値的に確かめた値です。
• 「これは Bessel 関数の不等式である」とは言っていません。F₀ は級数として定義された関数で、F₀(κ²/4) = 2I₁(κ)/κ という同定は Lean の中にありません。この対応を疑うなら、疑うべき場所は Lean の外です。手元では数値で 15 桁一致することを確かめてありますが、それは証明ではありません。計算
• この不等式が何の役に立つかは、言明の外です。log F₀ の凹性から先——強結合域の定数の見積り——は別の定理の連なりで、そちらには Lean に入っていない段（格子の幾何の側）が残っています。

二つめが、級数で定義を書いたときに必ず出る借りです。手で定義した関数が、呼びたかった名前の関数と同じものかどうかは、定義の外にあります。続きは 通っても、言いたいことが言えているかへ。

出典と再現

次は 07 証明書を Lean に検査させる——探索と検査を分ける組み方です。用語は 12 用語集。