← Session 17 — Lean tier (i): elementary proofs (after crash)
thinking (114 chars)
`sInf_series_summable` compiles. Now piece 2: harmonic bounds + oddHarm identity. Add after the summability lemma.
Summability compiles. Piece 2: harmonic bounds (from Mathlib's Euler–Mascheroni lemmas) + the odd-harmonic identity.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"old_string": "/-- [SKELETON] Archimedean lower bound (draft \u00a73.1 Step 1):",
"new_string": "/-- [PROVED session 011] H1: `log M + \u03b3 \u2264 H_M` (from Mathlib's strictly\ndecreasing `eulerMascheroniSeq'`). -/\ntheorem harmonic_lower (M : \u2115) (hM : 1 \u2264 M) :\n Real.log M + Real.eulerMascheroniConstant \u2264 (harmonic M : \u211d) := by\n have h := Real.eulerMascheroniConstant_lt_eulerMascheroniSeq' M\n rw [Real.eulerMascheroniSeq', if_neg (by omega : M \u2260 0)] at h\n linarith\n\n/-- [PROVED session 011] H2: `H_M \u2264 log (M+1) + \u03b3` (from Mathlib's strictly\nincreasing `eulerMascheroniSeq`). -/\ntheorem harmonic_upper (M : \u2115) :\n (harmonic M : \u211d) \u2264 Real.log ((M : \u211d) + 1) + Real.eulerMascheroniConstant := by\n have h := Real.eulerMascheroniSeq_lt_eulerMascheroniConstant M\n rw [Real.eulerMascheroniSeq] at h\n linarith\n\n/-- The odd reciprocals sum `\u03a3_{k=1}^{K} 1/(2k+1)`. -/\nprivate def oddHarm (K : \u2115) : \u211d := \u2211 k \u2208 Finset.Icc 1 K, (1 : \u211d) / (2 * k + 1)\n\n/-- [PROVED session 011] Odd-harmonic identity (D-037 \u00a73):\n`\u03a3_{k=1}^{K} 1/(2k+1) = H_{2K+1} \u2212 \u00bdH_K \u2212 1`, by induction. -/\ntheorem oddHarm_eq (K : \u2115) :\n oddHarm K = (harmonic (2 * K + 1) : \u211d) - (harmonic K : \u211d) / 2 - 1 := by\n induction K with\n | zero => simp [oddHarm, harmonic_succ]\n | succ K ih =>\n have h1 : (harmonic (2 * (K + 1) + 1) : \u211d) =\n (harmonic (2 * K + 1) : \u211d) + 1 / (2 * (K : \u211d) + 2) + 1 / (2 * (K : \u211d) + 3) := by\n have hs : 2 * (K + 1) + 1 = (2 * K + 1) + 1 + 1 := by ring\n rw [hs, harmonic_succ, harmonic_succ]\n push_cast\n ring\n have h2 : (harmonic (K + 1) : \u211d) = (harmonic K : \u211d) + 1 / ((K : \u211d) + 1) := by\n rw [harmonic_succ]\n push_cast\n ring\n have e3 : (1 : \u211d) / (2 * (K : \u211d) + 2) = (1 / ((K : \u211d) + 1)) / 2 := by\n have hne : (K : \u211d) + 1 \u2260 0 := by positivity\n field_simp\n ring\n show (\u2211 k \u2208 Finset.Icc 1 (K + 1), (1 : \u211d) / (2 * k + 1)) = _\n rw [Finset.sum_Icc_succ_top (by omega : 1 \u2264 K + 1) (fun k => (1 : \u211d) / (2 * k + 1))]\n show (\u2211 k \u2208 Finset.Icc 1 K, (1 : \u211d) / (2 * k + 1)) + 1 / (2 * ((K : \u211d) + 1) + 1) = _\n rw [show (\u2211 k \u2208 Finset.Icc 1 K, (1 : \u211d) / (2 * k + 1)) = oddHarm K from rfl, ih, h1, h2]\n push_cast\n rw [e3]\n ring\n\n/-- [SKELETON] Archimedean lower bound (draft \u00a73.1 Step 1):"
}
raw content_json (database row)
[{"type":"thinking","thinking":"`sInf_series_summable` compiles. Now piece 2: harmonic bounds + oddHarm identity. Add after the summability lemma.","signature":""},{"type":"text","text":"Summability compiles. Piece 2: harmonic bounds (from Mathlib's Euler–Mascheroni lemmas) + the odd-harmonic identity."},{"type":"tool_use","id":"Edit_56","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":"/-- [SKELETON] Archimedean lower bound (draft §3.1 Step 1):","new_string":"/-- [PROVED session 011] H1: `log M + γ ≤ H_M` (from Mathlib's strictly\ndecreasing `eulerMascheroniSeq'`). -/\ntheorem harmonic_lower (M : ℕ) (hM : 1 ≤ M) :\n Real.log M + Real.eulerMascheroniConstant ≤ (harmonic M : ℝ) := by\n have h := Real.eulerMascheroniConstant_lt_eulerMascheroniSeq' M\n rw [Real.eulerMascheroniSeq', if_neg (by omega : M ≠ 0)] at h\n linarith\n\n/-- [PROVED session 011] H2: `H_M ≤ log (M+1) + γ` (from Mathlib's strictly\nincreasing `eulerMascheroniSeq`). -/\ntheorem harmonic_upper (M : ℕ) :\n (harmonic M : ℝ) ≤ Real.log ((M : ℝ) + 1) + Real.eulerMascheroniConstant := by\n have h := Real.eulerMascheroniSeq_lt_eulerMascheroniConstant M\n rw [Real.eulerMascheroniSeq] at h\n linarith\n\n/-- The odd reciprocals sum `Σ_{k=1}^{K} 1/(2k+1)`. -/\nprivate def oddHarm (K : ℕ) : ℝ := ∑ k ∈ Finset.Icc 1 K, (1 : ℝ) / (2 * k + 1)\n\n/-- [PROVED session 011] Odd-harmonic identity (D-037 §3):\n`Σ_{k=1}^{K} 1/(2k+1) = H_{2K+1} − ½H_K − 1`, by induction. -/\ntheorem oddHarm_eq (K : ℕ) :\n oddHarm K = (harmonic (2 * K + 1) : ℝ) - (harmonic K : ℝ) / 2 - 1 := by\n induction K with\n | zero => simp [oddHarm, harmonic_succ]\n | succ K ih =>\n have h1 : (harmonic (2 * (K + 1) + 1) : ℝ) =\n (harmonic (2 * K + 1) : ℝ) + 1 / (2 * (K : ℝ) + 2) + 1 / (2 * (K : ℝ) + 3) := by\n have hs : 2 * (K + 1) + 1 = (2 * K + 1) + 1 + 1 := by ring\n rw [hs, harmonic_succ, harmonic_succ]\n push_cast\n ring\n have h2 : (harmonic (K + 1) : ℝ) = (harmonic K : ℝ) + 1 / ((K : ℝ) + 1) := by\n rw [harmonic_succ]\n push_cast\n ring\n have e3 : (1 : ℝ) / (2 * (K : ℝ) + 2) = (1 / ((K : ℝ) + 1)) / 2 := by\n have hne : (K : ℝ) + 1 ≠ 0 := by positivity\n field_simp\n ring\n show (∑ k ∈ Finset.Icc 1 (K + 1), (1 : ℝ) / (2 * k + 1)) = _\n rw [Finset.sum_Icc_succ_top (by omega : 1 ≤ K + 1) (fun k => (1 : ℝ) / (2 * k + 1))]\n show (∑ k ∈ Finset.Icc 1 K, (1 : ℝ) / (2 * k + 1)) + 1 / (2 * ((K : ℝ) + 1) + 1) = _\n rw [show (∑ k ∈ Finset.Icc 1 K, (1 : ℝ) / (2 * k + 1)) = oddHarm K from rfl, ih, h1, h2]\n push_cast\n rw [e3]\n ring\n\n/-- [SKELETON] Archimedean lower bound (draft §3.1 Step 1):"},"extra_content":null}]