Lean4: カッコ記号（）の違いだけ

前回の謎仕様よりは、まだ解りやすいですが、難所です。

カッコ外せば同じなのに？

∑ n ∈ Finset.Icc 0 X, ∏ p ∈ (2 * n + 1).primeFactors with p > P₀, Real.exp (t *  ↑((2 * n + 1).factorization p - 2) * Real.log ↑p ) ≤ (Finset.Icc 0 X).card • 1

∑ n ∈ Finset.Icc 0 X, ∏ p ∈ (2 * n + 1).primeFactors with p > P₀, Real.exp (t * (↑((2 * n + 1).factorization p - 2) * Real.log ↑p)) ≤ (Finset.Icc 0 X).card • 1

…っと、note だと比較しづらい記述になってしまいますね。

∑ n ∈ Finset.Icc 0 X, ∏ p ∈ (2 * n + 1).primeFactors with p > P₀, Real.exp (t *  ↑((2 * n + 1).factorization p - 2) * Real.log ↑p ) ≤ (Finset.Icc 0 X).card • 1
∑ n ∈ Finset.Icc 0 X, ∏ p ∈ (2 * n + 1).primeFactors with p > P₀, Real.exp (t * (↑((2 * n + 1).factorization p - 2) * Real.log ↑p)) ≤ (Finset.Icc 0 X).card • 1

これも、横長で…対象となる部分がはみ出てしまう…。

対象部のみ抽出

Real.exp (t *  ↑((2 * n + 1).factorization p - 2) * Real.log ↑p )
Real.exp (t * (↑((2 * n + 1).factorization p - 2) * Real.log ↑p))

これでも、見にくい？
ならば VSCode の色分け表示の画像を

下段の🟪紫のカッコ（）を外せば上段と同じになりますね。
下段の🟦青いカッコ外すわけではないので $${(f(p) - 2)}$$ は維持されます。

これが違う！Error となる → カッコが違うだけで

あと全体的には不等式なので

$$
\Large
a \le b \ = \ a \le b
$$

となります。が、$${a, b}$$ がシンクロ同期している必要がある？

同値性は示せる

等号「＝」では成り立たないと怒られた。じゃあ同値の「$${\iff}$$」ならば？

grind

なんと grind だと等号「＝」でも通るのです！

by rfl

:= by rfl なのか？ try ～ sorry で観測⚠️が付いちゃいましたね。
sorry で Error になってないので sorry は受理されての警告ですね。
→ declaration uses 'sorry'

どうすれば良いのか？

これが正解だそうです。

congr
⊢ (fun n ↦ ∏ p ∈ (2 * n + 1).primeFactors with p > P₀, Real.exp (t * ↑((2 * n + 1).factorization p - 2) * Real.log ↑p))
= fun n ↦ ∏ p ∈ (2 * n + 1).primeFactors with p > P₀, Real.exp (t * (↑((2 * n + 1).factorization p - 2) * Real.log ↑p))

funext n
⊢ ∏ p ∈ (2 * n + 1).primeFactors with p > P₀, Real.exp (t * ↑((2 * n + 1).factorization p - 2) * Real.log ↑p)
= ∏ p ∈ (2 * n + 1).primeFactors with p > P₀, Real.exp (t * (↑((2 * n + 1).factorization p - 2) * Real.log ↑p))

congr
⊢ (fun p ↦ Real.exp (t * ↑((2 * n + 1).factorization p - 2) * Real.log ↑p))
= fun p ↦ Real.exp (t * (↑((2 * n + 1).factorization p - 2) * Real.log ↑p))

funext p
⊢ Real.exp (t * ↑((2 * n + 1).factorization p - 2) * Real.log ↑p)
= Real.exp (t * (↑((2 * n + 1).factorization p - 2) * Real.log ↑p))

mul_assoc
⊢ Real.exp (t * (↑((2 * n + 1).factorization p - 2) * Real.log ↑p))
= Real.exp (t * (↑((2 * n + 1).factorization p - 2) * Real.log ↑p))

これはこれで良しとして…

問題は本題のほうか。
こっちは高度な話になるので Appendix としてしまおう。

初心者の方は、ここまで✍️あ、私も初心者ですね。

2025/10/31 11:26

D.

#Lean #Lean4 #Mathlib #Mathlib4

Appendix

もう一つの例

このカッコの付き方の違いを吸収して同じを言う

section real_exp_factorization_log

-- Real.exp (t *  ↑((2 * n + 1).factorization p - 2) * Real.log ↑p )
-- Real.exp (t * (↑((2 * n + 1).factorization p - 2) * Real.log ↑p))

noncomputable def real_exp (x : ℝ) : ℝ := Real.exp x

noncomputable def n2a1_fact_log (n p : ℕ) : ℝ :=
  (((Chernoff.n2a1 n).factorization p - 2) : ℝ) * Real.log (p : ℝ)

-- Real.exp (t *  ↑((2 * n + 1).factorization p - 2) * Real.log ↑p )
noncomputable def real_exp_factorization_log (n p : ℕ) (t : ℝ) : ℝ :=
  real_exp (t * n2a1_fact_log n p)

lemma real_exp_factorization_log_eq (n p : ℕ) (t : ℝ) :
  real_exp_factorization_log n p t =
    Real.exp (t * (((Chernoff.n2a1 n).factorization p - 2) : ℝ) * Real.log (p : ℝ)) := by
  dsimp [real_exp_factorization_log, real_exp, n2a1_fact_log]
  -- 括弧の位置の違いは乗算の結合法則で一致する
  rw [mul_assoc]
  -- t * (a * b) = (t * a) * b

lemma real_exp_factorization_log_eq' (n p : ℕ) (t : ℝ) :
  real_exp_factorization_log n p t =
    Real.exp (t * (↑((2 * n + 1).factorization p) - ↑2) * Real.log ↑p ) := by
  dsimp [real_exp_factorization_log, real_exp, n2a1_fact_log]
  rw [Chernoff.n2a1]
  -- Chernoff.n2a1 n = 2 * n + 1 なので両辺一致
  rw [mul_assoc]
  -- t * (a * b) = (t * a) * b

real_exp_factorization_log_eq

ここで

real_exp_factorization_log n p t =
    Real.exp (t * (((Chernoff.n2a1 n).factorization p - 2) : ℝ) * Real.log (p : ℝ))

これは通った Chernoff.n2a1 n を展開すれば以下 2 → ↑2 とすれば行ける

real_exp_factorization_log n p t =
    Real.exp (t * (↑((2 * n + 1).factorization p) - ↑2) * Real.log ↑p )

これをｃパターンとする

$$
\text{
-- c: Real.exp (t * (↑((2 * n + 1).factorization p) - ↑2) * Real.log ↑p )
}
$$

ａ，ｂパターンは「違う！」と何度もエラーで怒られた。

$$
\begin{array}{l}
\text{
-- a: Real.exp (t *  ↑((2 * n + 1).factorization p  -  2) * Real.log ↑p )
}\\
\text{
-- b: Real.exp (t * (↑((2 * n + 1).factorization p  -  2) * Real.log ↑p))
}
\end{array}
$$

かっこが余計についている。

見にくいかもしれない。それぞれを比較する例題。

-- c = a
example (n p : ℕ) (t : ℝ) (h : (2 * n + 1).factorization p ≥ 2) :
    Real.exp (t * (↑((2 * n + 1).factorization p) - ↑2) * Real.log ↑p )
  = Real.exp (t *  ↑((2 * n + 1).factorization p  -  2) * Real.log ↑p ) := by
  -- (↑a - ↑b) = ↑(a - b) if a ≥ b
  rw [Nat.cast_sub h]; rfl  -- 型が一致し、等式が証明できるぞ

-- c = b
example (n p : ℕ) (t : ℝ) (h : (2 * n + 1).factorization p ≥ 2) :
    Real.exp (t * (↑((2 * n + 1).factorization p) - ↑2) * Real.log ↑p )
  = Real.exp (t * (↑((2 * n + 1).factorization p  -  2) * Real.log ↑p)) := by
  -- (↑a - ↑b) = ↑(a - b) if a ≥ b
  rw [Nat.cast_sub h, mul_assoc]
  rfl -- 型が一致し、等式が証明できるぞ

-- b = a
example (n p : ℕ) (t : ℝ) (h : (2 * n + 1).factorization p ≥ 2) :
    Real.exp (t *  ↑((2 * n + 1).factorization p  -  2) * Real.log ↑p )
  = Real.exp (t * (↑((2 * n + 1).factorization p  -  2) * Real.log ↑p)) := by
  -- (↑a - ↑b) = ↑(a - b) if a ≥ b
  rw [Nat.cast_sub h, mul_assoc]

結果はこの通り成り立つ！

記号で書けば

$$
c=a\ \land\ c=b \quad \implies \quad b=a
$$

$$
\LARGE
a=b
$$

しかし…

んー？この example は通ったのに、
本題の方で解決できなかったのはどうしてだろう？🤔

P₀ の条件か？ここでは単なる$${\N}$$としての変数

本来の P₀

∀ p : ℕ, p.Prime → p ≤ P₀ → p ≠ 2

というもの。

これは、自然数に関する命題を数式で表現したものです。言葉で言い換えると、以下のようになります。

「任意の自然数 p について、もし p が素数であり、かつ p がある固定された自然数 P₀ 以下であるならば、p は 2 ではない。」

より自然な日本語にすると、

「P₀ 以下の任意の素数 p は、2 ではない。」

あるいは、

「P₀ 以下の素数の中に、2 は存在しない。」

となります。

補足:

• `∀ p : ℕ` は、「任意の自然数 p について」という意味です。

• `p.Prime` は、「p は素数である」という意味です。

• `p ≤ P₀` は、「p は P₀ 以下である」という意味です。

• `p ≠ 2` は、「p は 2 と等しくない」という意味です。

• `→` は、「ならば」という意味です。

この命題が真であるためには、P₀ が 2 より小さい自然数である必要があります。例えば、P₀ が 1 や 0 であれば、この命題は真となります。

AI に解説お願いしてもらった。

じゃあ本来の素数ですら無い？（笑）

ご指摘の通りです。この命題は、P₀ が 2 より小さい自然数である場合にのみ真となるため、通常、素数について議論する文脈では意味をなしません。

なぜなら、素数とは 1 より大きい自然数で、1 と自分自身以外に約数を持たない数のことだからです。つまり、素数は少なくとも 2 から始まります。

この命題が意味を持つとすれば、以下のような特殊な状況が考えられます。

1. P₀ が 1 または 0 の場合: この場合、P₀ 以下の自然数の中に素数は存在しないため、命題は自明的に真となります。しかし、これは素数の性質を議論する上で有用ではありません。

2. 形式的な演習問題: 数学の論理や記号の練習問題として、このような命題が提示されることがあります。この場合、命題の内容よりも、記号の読み方や論理的な推論の練習が目的となります。

したがって、この命題は、通常の素数の性質を表現するものではなく、特殊な状況下でのみ真となる、あるいは形式的な練習問題として扱われるべきものです。

まとめると、この命題は、素数という概念を理解している人にとっては、
ほとんど意味のない命題と言えます。

それを参照している命題、これはどういう事か？

なるほど、Lean での証明の一部として使われているのですね。文脈が分かると、この命題の役割が見えてきます。

この命題は、証明全体の戦略の一部として、小さい素数 (2 を除く) がある種の評価式に与える影響を限定するために使われていると考えられます。具体的には、

• `p.Prime → p ≤ P₀ → p ≠ 2` の部分は、「P₀ 以下の 2 以外の素数 p について」という条件を表しています。

• `∃ C_p > 0, ∀ X ≥ 3, ...` の部分は、「そのような p に対して、ある正の定数 C_p が存在し、任意の X ≥ 3 に対して、... が成り立つ」ということを表しています。

• `Finset.sum ...` の部分は、具体的な評価式を表しており、p がこの評価式に与える影響を評価しています。

つまり、この命題は、 「P₀ 以下の 2 以外の素数 p は、ある評価式に対して、X が十分に大きいとき、その影響を C_p という定数で抑えることができる」ということを主張しています。

なぜ 2 を除くのか？

2 を除く理由は、2 が他の素数とは異なる性質を持っている可能性があるからです。例えば、2 は唯一の偶数の素数であり、他の素数とは異なる振る舞いをする場合があります。そのため、2 を特別扱いすることで、証明をより簡単にする、あるいはより正確な評価を得ることができる可能性があります。

全体の戦略

この命題が証明全体の中でどのような役割を果たしているかは、全体のコードを読まないと正確には分かりませんが、おそらく以下のような戦略の一部であると考えられます。

1. 小さい素数と大きい素数を分けて考える: 素数全体の評価を直接行うのではなく、小さい素数と大きい素数に分けて、それぞれ別々に評価する。

2. 小さい素数の影響を限定する: 小さい素数は数が限られているため、個別に評価することで、その影響を定数で抑えることができる。

3. 大きい素数の影響を別の方法で評価する: 大きい素数は数が多いため、個別に評価するのではなく、別の方法 (例えば、統計的な手法) でその影響を評価する。

このように、小さい素数と大きい素数を分けて考えることで、証明をより簡単にする、あるいはより正確な評価を得ることができる場合があります。

まとめ

この命題は、単独で見ると奇妙に見えますが、Lean での証明の一部として見ると、小さい素数の影響を限定するという明確な目的を持っていることが分かります。特に、2 を除く理由は、2 が他の素数とは異なる性質を持っている可能性があるためと考えられます。

ごく一部だけなのに、想定が当たっている AI 賢いなあ。
$${p > 2 \Rightarrow p \ge 3}$$ という条件で証明が語られている場面です。

have h3_le : 3 ≤ P₀ := by rfl

この命題により、上記の $${\text{h3\_le} := 3\le P_0}$$ これは「真」です。
P₀ が取る値は 0, 1 でなく 2 でもない 3 以上になるからですね。

ありがとうございます。`h_large` の命題と関連する定義を共有していただいたことで、全体像がより明確になりました。

`h_large` の命題は、P₀ より大きい素数からの寄与を評価するためのもので、`h_small_primes` と対をなす役割を果たしていることが分かります。

以下に、`h_large` の命題をより詳しく見ていきましょう。

• `∃ C₂ > 0, ...`：ある正の定数 C₂ が存在し、... が成り立つ。

• `Finset.sum (Finset.Icc 0 X) fun n => ...`：0 から X までの n について、... の総和を取る。

• `Finset.prod ((2 * n + 1).primeFactors.filter (fun p => p > P₀)) fun p => ...`：2n+1 の素因数のうち、P₀ より大きい素数 p について、... の総積を取る。

• `real_exp_factorization_log n p t`：定義から、`real_exp (t * (((Chernoff.n2a1 n).factorization p - 2) : ℝ) * Real.log (p : ℝ))` であり、これは素因数 p が 2n+1 に現れる回数 (factorization p) に依存する項です。

つまり、`h_large` の命題は、「P₀ より大きい素数 p が 2n+1 の素因数として現れる回数に基づいて計算されるある評価式について、その総和は、ある定数 C₂ で抑えられる」ということを主張しています。

全体の戦略の再確認

これらの情報から、全体の証明戦略は以下のようになっていると考えられます。

1. 評価対象の式を、小さい素数と大きい素数の寄与に分解する。

2. 小さい素数 (p ≤ P₀ かつ p ≠ 2) については、`h_small_primes` を用いて、その寄与を定数 C_p で抑える。 `h_small_primes` は、個々の小さい素数の寄与を評価し、それらの総和を定数で抑えることを可能にする。

3. 大きい素数 (p > P₀) については、`h_large` を用いて、その寄与を定数 C₂ で抑える。 `h_large` は、個々の大きい素数の寄与を直接評価するのではなく、素因数分解に基づいて計算される評価式を用いて、その総和を定数で抑えることを可能にする。

4. 小さい素数と大きい素数の寄与を合わせることで、全体の評価を完了する。

P₀ の役割

P₀ は、小さい素数と大きい素数を区別するための閾値として機能しています。P₀ を適切に設定することで、`h_small_primes` と `h_large` の両方が成り立つようにする必要があります。

まとめ

`h_large` の命題は、P₀ より大きい素数からの寄与を評価するためのものであり、`h_small_primes` と組み合わせて、全体の評価を完了するために使用されます。P₀ は、小さい素数と大きい素数を区別するための閾値として機能し、証明全体の戦略において重要な役割を果たしています。

この分析が、Lean のコードの理解に役立つことを願っています。

ふむ。なるほど！わからん（笑）
でも、🐺賢狼がいつもそう言っていたので流れは合っている。

ああ！…

もしかして。

$$
p \ge 2
$$

$${p = 2}$$ を含めてしまっているから？

$$
p \gt 2\ または\ p \ge 3\ だと…
$$

Error になる…これか？😅汗