← Session 17 — Lean tier (i): elementary proofs (after crash)
thinking (300 chars)
I was mid-planning. Time to write the code. Let me write the helper lemmas first in a small edit, build, then the main theorem in pieces. Keep pieces small.
Step 1: add private defs + basic term lemmas (one_sub_div_pow_ge, sInfTerm, sInfTerm_nonneg, sInfTerm_lower, sInfTerm_factor, sInfTerm_upper).
Writing the proof now, in small pieces. Piece 1: term definition + Bernoulli bounds.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"old_string": "/-- C\u2081 = (\u03b3 \u2212 1 \u2212 log 2\u03c0)/2 (D-037). -/\ndef lagariasC1 : \u211d :=\n (Real.eulerMascheroniConstant - 1 - Real.log (2 * Real.pi)) / 2",
"new_string": "/-- C\u2081 = (\u03b3 \u2212 1 \u2212 log 2\u03c0)/2 (D-037). -/\ndef lagariasC1 : \u211d :=\n (Real.eulerMascheroniConstant - 1 - Real.log (2 * Real.pi)) / 2\n\n/-! ### Helpers for the `sInfty_lower_bound` proof (D-037 \u00a73) -/\n\n/-- The summand of the odd-m series in `SInfty`, as a function on \u2115. -/\nprivate def sInfTerm (n m : \u2115) : \u211d := (1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / (m : \u211d)\n\n/-- Bernoulli: `1 \u2212 n/m \u2264 (1 \u2212 1/m)\u207f` for `m \u2265 1`. -/\nprivate lemma one_sub_div_pow_ge (n m : \u2115) (hm : 1 \u2264 m) :\n 1 - (n : \u211d) / m \u2264 (1 - 1 / (m : \u211d)) ^ n := by\n have hm1 : (1 : \u211d) \u2264 m := by exact_mod_cast hm\n have h2 : (-2 : \u211d) \u2264 -(1 / (m : \u211d)) := by\n have h : (1 : \u211d) / m \u2264 2 := le_trans (div_le_one (by positivity) |>.mpr hm1) (by norm_num)\n linarith\n have h := one_add_mul_le_pow h2 n\n have e1 : (1 : \u211d) + (n : \u211d) * -(1 / (m : \u211d)) = 1 - (n : \u211d) / m := by ring\n have e2 : (1 : \u211d) + -(1 / (m : \u211d)) = 1 - 1 / (m : \u211d) := by ring\n rwa [e1, e2] at h\n\nprivate lemma sInfTerm_nonneg (n m : \u2115) (hm : 1 \u2264 m) : 0 \u2264 sInfTerm n m := by\n have h := one_sub_div_pow_ge n m hm\n unfold sInfTerm\n linarith\n\nprivate lemma sInfTerm_lower (n m : \u2115) (hm : 1 \u2264 m) :\n (n : \u211d) / m - 1 \u2264 sInfTerm n m := by\n have h := one_sub_div_pow_ge n m hm\n unfold sInfTerm\n linarith\n\n/-- Geometric-sum factorization: `sInfTerm n m = (1/m)\u00b7\u03a3_{j<n} (1 \u2212 (1\u22121/m)\u02b2)`. -/\nprivate lemma sInfTerm_factor (n m : \u2115) (hm : 1 \u2264 m) :\n sInfTerm n m = (1 / (m : \u211d)) * \u2211 j \u2208 Finset.range n, (1 - (1 - 1 / (m : \u211d)) ^ j) := by\n have hgeom := geom_sum_mul (1 - 1 / (m : \u211d)) n\n have h2 : (1 - 1 / (m : \u211d)) - 1 = -(1 / (m : \u211d)) := by ring\n rw [h2] at hgeom\n have e2 : (1 / (m : \u211d)) * \u2211 j \u2208 Finset.range n, (1 - (1 - 1 / (m : \u211d)) ^ j) =\n (1 / (m : \u211d)) * ((n : \u211d) - \u2211 j \u2208 Finset.range n, (1 - 1 / (m : \u211d)) ^ j) := by\n congr 1\n rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one]\n rw [e2]\n unfold sInfTerm\n linear_combination -hgeom\n\n/-- Termwise quadratic upper bound: `sInfTerm n m \u2264 (n(n\u22121)/2)\u00b7(1/m\u00b2)`. -/\nprivate lemma sInfTerm_upper (n m : \u2115) (hn : 1 \u2264 n) (hm : 1 \u2264 m) :\n sInfTerm n m \u2264 ((n : \u211d) * ((n : \u211d) - 1) / 2) * (1 / (m : \u211d) ^ 2) := by\n have hm1 : (1 : \u211d) \u2264 m := by exact_mod_cast hm\n have key := sInfTerm_factor n m hm\n rw [key]\n have hterm : \u2200 j \u2208 Finset.range n, (1 : \u211d) - (1 - 1 / (m : \u211d)) ^ j \u2264 (j : \u211d) / m := by\n intro j _\n have h := one_sub_div_pow_ge j m hm\n linarith\n have hsum := Finset.sum_le_sum hterm\n have hsum2 : \u2211 j \u2208 Finset.range n, ((j : \u211d) / m) = ((n : \u211d) * ((n : \u211d) - 1) / 2) / m := by\n rw [\u2190 Finset.sum_div]\n congr 1\n have h2 := Finset.sum_range_id_mul_two n\n have h4 : (((\u2211 i \u2208 Finset.range n, i) * 2 : \u2115) : \u211d) = ((n * (n - 1) : \u2115) : \u211d) := by\n exact_mod_cast h2\n have h5 : ((n - 1 : \u2115) : \u211d) = (n : \u211d) - 1 := by\n rw [Nat.cast_sub hn, Nat.cast_one]\n push_cast at h4\n rw [h5] at h4\n linarith\n rw [hsum2] at hsum\n have hm0' : (0 : \u211d) \u2264 1 / (m : \u211d) := by positivity\n calc (1 / (m : \u211d)) * \u2211 j \u2208 Finset.range n, (1 - (1 - 1 / (m : \u211d)) ^ j)\n \u2264 (1 / (m : \u211d)) * (((n : \u211d) * ((n : \u211d) - 1) / 2) / m) :=\n mul_le_mul_of_nonneg_left hsum hm0'\n _ = ((n : \u211d) * ((n : \u211d) - 1) / 2) * (1 / (m : \u211d) ^ 2) := by field_simp; ring"
}
raw content_json (database row)
[{"type":"thinking","thinking":"I was mid-planning. Time to write the code. Let me write the helper lemmas first in a small edit, build, then the main theorem in pieces. Keep pieces small.\n\nStep 1: add private defs + basic term lemmas (one_sub_div_pow_ge, sInfTerm, sInfTerm_nonneg, sInfTerm_lower, sInfTerm_factor, sInfTerm_upper).","signature":""},{"type":"text","text":"Writing the proof now, in small pieces. Piece 1: term definition + Bernoulli bounds."},{"type":"tool_use","id":"Edit_42","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":"/-- C₁ = (γ − 1 − log 2π)/2 (D-037). -/\ndef lagariasC1 : ℝ :=\n (Real.eulerMascheroniConstant - 1 - Real.log (2 * Real.pi)) / 2","new_string":"/-- C₁ = (γ − 1 − log 2π)/2 (D-037). -/\ndef lagariasC1 : ℝ :=\n (Real.eulerMascheroniConstant - 1 - Real.log (2 * Real.pi)) / 2\n\n/-! ### Helpers for the `sInfty_lower_bound` proof (D-037 §3) -/\n\n/-- The summand of the odd-m series in `SInfty`, as a function on ℕ. -/\nprivate def sInfTerm (n m : ℕ) : ℝ := (1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ)\n\n/-- Bernoulli: `1 − n/m ≤ (1 − 1/m)ⁿ` for `m ≥ 1`. -/\nprivate lemma one_sub_div_pow_ge (n m : ℕ) (hm : 1 ≤ m) :\n 1 - (n : ℝ) / m ≤ (1 - 1 / (m : ℝ)) ^ n := by\n have hm1 : (1 : ℝ) ≤ m := by exact_mod_cast hm\n have h2 : (-2 : ℝ) ≤ -(1 / (m : ℝ)) := by\n have h : (1 : ℝ) / m ≤ 2 := le_trans (div_le_one (by positivity) |>.mpr hm1) (by norm_num)\n linarith\n have h := one_add_mul_le_pow h2 n\n have e1 : (1 : ℝ) + (n : ℝ) * -(1 / (m : ℝ)) = 1 - (n : ℝ) / m := by ring\n have e2 : (1 : ℝ) + -(1 / (m : ℝ)) = 1 - 1 / (m : ℝ) := by ring\n rwa [e1, e2] at h\n\nprivate lemma sInfTerm_nonneg (n m : ℕ) (hm : 1 ≤ m) : 0 ≤ sInfTerm n m := by\n have h := one_sub_div_pow_ge n m hm\n unfold sInfTerm\n linarith\n\nprivate lemma sInfTerm_lower (n m : ℕ) (hm : 1 ≤ m) :\n (n : ℝ) / m - 1 ≤ sInfTerm n m := by\n have h := one_sub_div_pow_ge n m hm\n unfold sInfTerm\n linarith\n\n/-- Geometric-sum factorization: `sInfTerm n m = (1/m)·Σ_{j<n} (1 − (1−1/m)ʲ)`. -/\nprivate lemma sInfTerm_factor (n m : ℕ) (hm : 1 ≤ m) :\n sInfTerm n m = (1 / (m : ℝ)) * ∑ j ∈ Finset.range n, (1 - (1 - 1 / (m : ℝ)) ^ j) := by\n have hgeom := geom_sum_mul (1 - 1 / (m : ℝ)) n\n have h2 : (1 - 1 / (m : ℝ)) - 1 = -(1 / (m : ℝ)) := by ring\n rw [h2] at hgeom\n have e2 : (1 / (m : ℝ)) * ∑ j ∈ Finset.range n, (1 - (1 - 1 / (m : ℝ)) ^ j) =\n (1 / (m : ℝ)) * ((n : ℝ) - ∑ j ∈ Finset.range n, (1 - 1 / (m : ℝ)) ^ j) := by\n congr 1\n rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one]\n rw [e2]\n unfold sInfTerm\n linear_combination -hgeom\n\n/-- Termwise quadratic upper bound: `sInfTerm n m ≤ (n(n−1)/2)·(1/m²)`. -/\nprivate lemma sInfTerm_upper (n m : ℕ) (hn : 1 ≤ n) (hm : 1 ≤ m) :\n sInfTerm n m ≤ ((n : ℝ) * ((n : ℝ) - 1) / 2) * (1 / (m : ℝ) ^ 2) := by\n have hm1 : (1 : ℝ) ≤ m := by exact_mod_cast hm\n have key := sInfTerm_factor n m hm\n rw [key]\n have hterm : ∀ j ∈ Finset.range n, (1 : ℝ) - (1 - 1 / (m : ℝ)) ^ j ≤ (j : ℝ) / m := by\n intro j _\n have h := one_sub_div_pow_ge j m hm\n linarith\n have hsum := Finset.sum_le_sum hterm\n have hsum2 : ∑ j ∈ Finset.range n, ((j : ℝ) / m) = ((n : ℝ) * ((n : ℝ) - 1) / 2) / m := by\n rw [← Finset.sum_div]\n congr 1\n have h2 := Finset.sum_range_id_mul_two n\n have h4 : (((∑ i ∈ Finset.range n, i) * 2 : ℕ) : ℝ) = ((n * (n - 1) : ℕ) : ℝ) := by\n exact_mod_cast h2\n have h5 : ((n - 1 : ℕ) : ℝ) = (n : ℝ) - 1 := by\n rw [Nat.cast_sub hn, Nat.cast_one]\n push_cast at h4\n rw [h5] at h4\n linarith\n rw [hsum2] at hsum\n have hm0' : (0 : ℝ) ≤ 1 / (m : ℝ) := by positivity\n calc (1 / (m : ℝ)) * ∑ j ∈ Finset.range n, (1 - (1 - 1 / (m : ℝ)) ^ j)\n ≤ (1 / (m : ℝ)) * (((n : ℝ) * ((n : ℝ) - 1) / 2) / m) :=\n mul_le_mul_of_nonneg_left hsum hm0'\n _ = ((n : ℝ) * ((n : ℝ) - 1) / 2) * (1 / (m : ℝ) ^ 2) := by field_simp; ring"},"extra_content":null}]