← Session 30 — ii′-5e squeeze capstone + 5f perimeter repair
thinking (623 chars)
Good: head = lines 1–198 (through §5's near_sum_refPoint_le end), tail = lines 432–508 (pieces 4/5 through `end NguyenRH1 / end`). Now write the new §6 (piece 1) to a temp file, then splice: head + §6-header-and-piece1 + section-header-for-pieces45 + tail.
Wait — the tail starts with the `/-- **Pieces 4/5**` docstring but is missing the `/-! ## 6. Pieces 4/5: ... -/` section header (which my bad edit replaced). I'll add a section header in the middle part.
Let me write the middle (§6 complete with the factored helpers + dirichletC2_le_one + the §7 header) to /tmp/litightr_mid.txt via Write, then cat them together.
Writing the corrected §6 (piece 1) to a temp file, then splicing.
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\litightr_mid.tmp",
"content": "/-! ## 6. Piece 1: the Dirichlet bound at the reference point -/\n\n/-- The Dirichlet term norm at 2: \u2016LSeries.term \u039b 2 n\u2016 = (if n = 0 then\n0 else) \u039b(n)/n\u00b2. -/\nlemma dirichletTerm_norm_eq (n : \u2115) :\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n = if n = 0 then (0 : \u211d)\n else (ArithmeticFunction.vonMangoldt n) / (n : \u211d) ^ 2 := by\n rcases eq_or_ne n 0 with rfl | hn\n \u00b7 simp [LSeries.term]\n \u00b7 rw [LSeries.term_def, if_neg hn, norm_div]\n have h1 : \u2016(ArithmeticFunction.vonMangoldt n : \u2102)\u2016\n = ArithmeticFunction.vonMangoldt n := by\n rw [show (ArithmeticFunction.vonMangoldt n : \u2102)\n = ((ArithmeticFunction.vonMangoldt n : \u211d) : \u2102) by push_cast; ring,\n Complex.norm_real]\n exact abs_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n have h2 : \u2016((n : \u2102)) ^ (2 : \u2102)\u2016 = (n : \u211d) ^ 2 := by\n rw [show ((n : \u2102)) ^ (2 : \u2102) = ((n : \u2102)) ^ (2 : \u2115) by\n exact_mod_cast rfl, norm_pow]\n rw [show ((n : \u2102)) = ((n : \u211d) : \u2102) by push_cast; ring, Complex.norm_real]\n exact abs_of_nonneg (by positivity)\n rw [h1, h2]\n\n/-- The antiderivative derivative fact: d/dx [\u2212(log x + 1)/x] = log x/x\u00b2. -/\nlemma hasDerivAt_neg_log_add_one_div {x : \u211d} (hx0 : x \u2260 0) :\n HasDerivAt (fun y => -(Real.log y + 1) / y) (Real.log x / x ^ 2) x := by\n have h1 := ((Real.hasDerivAt_log hx0).add_const 1).div (hasDerivAt_id' x) hx0\n have h2 := h1.neg\n convert h2 using 1\n \u00b7 ext y\n simp [neg_div]\n \u00b7 simp only [id_eq]\n field_simp\n ring\n\n/-- \u2212(log x + 1)/x \u2192 0 as x \u2192 \u221e. -/\nlemma tendsto_neg_log_add_one_div :\n Tendsto (fun y => -(Real.log y + 1) / y) atTop (\ud835\udcdd 0) := by\n have hA : Tendsto (fun x => Real.log x / x) atTop (\ud835\udcdd 0) := by\n have h := tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero\n simpa using h\n have hB : Tendsto (fun x => (1 : \u211d) / x) atTop (\ud835\udcdd 0) :=\n tendsto_one_div_atTop_nhds_zero\n have hC : Tendsto (fun x => Real.log x / x + 1 / x) atTop (\ud835\udcdd (0 + 0)) :=\n hA.add hB\n have heq : (fun y => -(Real.log y + 1) / y) = (fun x => -(Real.log x / x + 1 / x)) := by\n ext x\n rw [neg_div, add_div]\n rw [heq]\n simpa using hC.neg\n\n/-- log x/x\u00b2 is integrable on Ioi 3. -/\nlemma integrableOn_log_div_sq :\n IntegrableOn (fun x => Real.log x / x ^ 2) (Set.Ioi (3 : \u211d)) volume := by\n apply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>\n hasDerivAt_neg_log_add_one_div (by\n have h := (Set.mem_Ici.mp hx); linarith))\n \u00b7 intro x hx\n have hx3 : (3 : \u211d) < x := hx\n have hlog : (0 : \u211d) \u2264 Real.log x := Real.log_nonneg (by linarith)\n positivity\n \u00b7 exact tendsto_neg_log_add_one_div\n\n/-- The integral of log x/x\u00b2 over Ioi 3 is (log 3 + 1)/3. -/\nlemma integral_log_div_sq_Ioi_three :\n \u222b x in Set.Ioi (3 : \u211d), Real.log x / x ^ 2 = (Real.log 3 + 1) / 3 := by\n have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n (fun x hx => hasDerivAt_neg_log_add_one_div (by\n have h := (Set.mem_Ici.mp hx); linarith))\n integrableOn_log_div_sq tendsto_neg_log_add_one_div\n rw [h]\n show (0 : \u211d) - (-(Real.log 3 + 1) / 3) = (Real.log 3 + 1) / 3\n ring\n\n/-- log x/x\u00b2 is antitone on Ici 3 (its derivative (1 \u2212 2 log x)/x\u00b3 is\n\u2264 0 for x \u2265 3 since log x \u2265 log 3 \u2265 1). -/\nlemma antitoneOn_log_div_sq :\n AntitoneOn (fun x => Real.log x / x ^ 2) (Set.Ici (3 : \u211d)) := by\n apply antitoneOn_of_deriv_nonpos (convex_Ici 3)\n \u00b7 intro x hx\n have hx0 : x \u2260 0 := by have h := (Set.mem_Ici.mp hx); linarith\n exact ((Real.differentiableAt_log hx0).div (differentiableAt_pow _ _)\n (pow_ne_zero 2 hx0)).continuousAt.continuousWithinAt\n \u00b7 intro x hx\n have hx0 : x \u2260 0 := by\n have h : (3 : \u211d) < x := Set.mem_Ioi.mp (by rwa [Set.interior_Ici] at hx)\n linarith\n exact ((Real.differentiableAt_log hx0).div (differentiableAt_pow _ _)\n (pow_ne_zero 2 hx0)).differentiableWithinAt\n \u00b7 intro x hx\n have hx3 : (3 : \u211d) < x := Set.mem_Ioi.mp (by rwa [Set.interior_Ici] at hx)\n have hx0 : x \u2260 0 := by linarith\n have hlog3 : (1 : \u211d) \u2264 Real.log 3 := by\n have h := Real.log_le_log (Real.exp_pos 1)\n (by linarith [Real.exp_one_lt_d9.le] : Real.exp 1 \u2264 3)\n rwa [Real.log_exp] at h\n have hlogx : (1 : \u211d) \u2264 Real.log x :=\n hlog3.trans (Real.log_le_log (by positivity : (0 : \u211d) < 3) hx3.le)\n have hderiv : deriv (fun y => Real.log y / y ^ 2) x\n = (1 - 2 * Real.log x) / x ^ 3 := by\n have h := (Real.hasDerivAt_log hx0).div (hasDerivAt_pow 2 x) (pow_ne_zero 2 hx0)\n rw [h.deriv]\n congr 1\n field_simp\n ring\n rw [hderiv]\n exact div_nonpos_of_nonpos_of_nonneg (by linarith [hlogx]) (by positivity)\n\n/-- Summability of the log-tail (integral test). -/\nlemma summable_log_div_sq_tail :\n Summable (fun n : \u2115 => Real.log ((n : \u211d) + 4) / ((n : \u211d) + 4) ^ 2) := by\n have h := AntitoneOn.summable_of_integrableOn_Ioi antitoneOn_log_div_sq\n integrableOn_log_div_sq (fun t ht => by\n have ht3 : (3 : \u211d) < t := ht\n have hlog : (0 : \u211d) \u2264 Real.log t := Real.log_nonneg (by linarith)\n positivity)\n -- h : Summable (fun n : \u2115 \u21a6 (fun x => log x / x\u00b2) \u2191n); shift by 4\n have h2 := (summable_nat_add_iff 4).mpr (f := fun n : \u2115 =>\n Real.log (n : \u211d) / (n : \u211d) ^ 2) h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n\n/-- The tail bound: \u03a3_{n\u22654} log n/n\u00b2 \u2264 (log 3 + 1)/3 (integral test). -/\nlemma tsum_log_div_sq_tail_le :\n \u2211' n : \u2115, Real.log ((n : \u211d) + 4) / ((n : \u211d) + 4) ^ 2 \u2264 (Real.log 3 + 1) / 3 := by\n have hle := antitoneOn_log_div_sq.tsum_comp_add_le_integral 3\n integrableOn_log_div_sq (fun t ht => by\n have ht3 : (3 : \u211d) < t := ht\n have hlog : (0 : \u211d) \u2264 Real.log t := Real.log_nonneg (by linarith)\n positivity)\n -- hle : \u2211' n, (fun x => log x/x\u00b2) \u2191(n + 3 + 1) \u2264 \u222b Ioi 3\n rw [integral_log_div_sq_Ioi_three] at hle\n refine hle.trans_eq' ?_\n refine tsum_congr fun n => ?_\n push_cast\n ring_nf\n\n/-- **Piece 1** (D-069 \u00a73): dirichletC2 \u2264 1. The honest value is\n\u2212\u03b6\u2032/\u03b6(2) \u2248 0.56997; the bound here uses \u039b(n) \u2264 log n, the exact head\nn = 2, 3, and the integral-test tail (log 3 + 1)/3 \u2264 0.7. -/\ntheorem dirichletC2_le_one : dirichletC2 \u2264 1 := by\n rw [dirichletC2]\n have hsumm_g : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n -- the log majorant h n = if n = 0 then 0 else log n/n\u00b2, and its tsum split\n set h : \u2115 \u2192 \u211d := fun n => if n = 0 then (0 : \u211d)\n else Real.log n / (n : \u211d) ^ 2 with hh\n have hle_pointwise : \u2200 n : \u2115,\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n \u2264 h n := by\n intro n\n rw [dirichletTerm_norm_eq n, hh]\n rcases eq_or_ne n 0 with rfl | hn\n \u00b7 simp\n \u00b7 rw [if_neg hn, if_neg hn]\n exact div_le_div_of_nonneg_right ArithmeticFunction.vonMangoldt_le_log\n (by positivity : (0 : \u211d) \u2264 (n : \u211d) ^ 2)\n -- summability of h: the tail n + 4 is summable, and the head is finite\n have hsumh : Summable h := by\n have h1 : Summable (fun n : \u2115 => h (n + 4)) := by\n apply summable_log_div_sq_tail.congr\n intro n\n rw [hh]\n show (if (n + 4 : \u2115) = 0 then (0 : \u211d) else Real.log (n + 4) / ((n + 4 : \u2115) : \u211d) ^ 2)\n = Real.log ((n : \u211d) + 4) / ((n : \u211d) + 4) ^ 2\n rw [if_neg (by omega : (n + 4 : \u2115) \u2260 0)]\n push_cast\n ring_nf\n exact (summable_nat_add_iff 4).mp h1\n -- the head/tail split of the h-tsum\n have hsplit : \u2211' n : \u2115, h n = (\u2211 n \u2208 Finset.range 4, h n) + \u2211' n : \u2115, h (n + 4) := by\n exact (sum_add_tsum_nat_add 4 hsumh).symm\n have hhead : \u2211 n \u2208 Finset.range 4, h n = Real.log 2 / 4 + Real.log 3 / 9 := by\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_zero]\n rw [hh]\n simp only [Nat.zero_eq, if_pos, Nat.one_ne_zero, Nat.add_eq_zero_iff,\n OfNat.ofNat_ne_zero, and_self, not_false_eq_true]\n rw [show h 1 = (0 : \u211d) from by rw [hh]; simp]\n rw [show h 2 = Real.log 2 / 4 from by\n rw [hh]; rw [if_neg (by norm_num : (2 : \u2115) \u2260 0)]; push_cast; ring_nf]\n rw [show h 3 = Real.log 3 / 9 from by\n rw [hh]; rw [if_neg (by norm_num : (3 : \u2115) \u2260 0)]; push_cast; ring_nf]\n ring\n have htail : \u2211' n : \u2115, h (n + 4) \u2264 (Real.log 3 + 1) / 3 := by\n have h1 : (\u2211' n : \u2115, h (n + 4))\n = \u2211' n : \u2115, Real.log ((n : \u211d) + 4) / ((n : \u211d) + 4) ^ 2 := by\n refine tsum_congr fun n => ?_\n rw [hh]\n show (if (n + 4 : \u2115) = 0 then (0 : \u211d) else Real.log (n + 4) / ((n + 4 : \u2115) : \u211d) ^ 2)\n = Real.log ((n : \u211d) + 4) / ((n : \u211d) + 4) ^ 2\n rw [if_neg (by omega : (n + 4 : \u2115) \u2260 0)]\n push_cast\n ring_nf\n rw [h1]\n exact tsum_log_div_sq_tail_le\n -- assemble\n have hmain : \u2211' n : \u2115,\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n \u2264 Real.log 2 / 4 + Real.log 3 / 9 + (Real.log 3 + 1) / 3 := by\n calc \u2211' n : \u2115,\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n \u2264 \u2211' n : \u2115, h n := Summable.tsum_le_tsum hle_pointwise hsumm_g hsumh\n _ = (\u2211 n \u2208 Finset.range 4, h n) + \u2211' n : \u2115, h (n + 4) := hsplit\n _ \u2264 (Real.log 2 / 4 + Real.log 3 / 9) + (Real.log 3 + 1) / 3 := by\n linarith [hhead, htail]\n -- the numeric fold: log 2 \u2264 0.6932, log 3 \u2264 1.1\n have hlog2 : Real.log 2 \u2264 0.6932 := Real.log_two_lt_d9.le.trans (by norm_num)\n have hlog3 : Real.log 3 \u2264 1.1 := by\n have h3le : (3 : \u211d) \u2264 Real.exp 1.1 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : \u211d) \u2264 1.1 by norm_num) 6\n -- \u03a3_{k<6} 1.1^k/k! = 3.00126\u2026 \u2265 3\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_zero] at h\n norm_num at h\n linarith [h]\n have h2 : Real.log 3 \u2264 Real.log (Real.exp 1.1) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 3) h3le\n rwa [Real.log_exp] at h2\n have hlog2nn : (0 : \u211d) \u2264 Real.log 2 := Real.log_nonneg (by norm_num)\n have hlog3nn : (0 : \u211d) \u2264 Real.log 3 := Real.log_nonneg (by norm_num)\n linarith [hmain, hlog2, hlog3, hlog2nn, hlog3nn]\n\n/-! ## 7. Pieces 4/5: the reciprocal differences -/\n\n"
}
result 2026-08-24 09:45:08Z → 2026-08-24 09:45:08Z
{
"type": "create",
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\litightr_mid.tmp",
"content": "/-! ## 6. Piece 1: the Dirichlet bound at the reference point -/\n\n/-- The Dirichlet term norm at 2: \u2016LSeries.term \u039b 2 n\u2016 = (if n = 0 then\n0 else) \u039b(n)/n\u00b2. -/\nlemma dirichletTerm_norm_eq (n : \u2115) :\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n = if n = 0 then (0 : \u211d)\n else (ArithmeticFunction.vonMangoldt n) / (n : \u211d) ^ 2 := by\n rcases eq_or_ne n 0 with rfl | hn\n \u00b7 simp [LSeries.term]\n \u00b7 rw [LSeries.term_def, if_neg hn, norm_div]\n have h1 : \u2016(ArithmeticFunction.vonMangoldt n : \u2102)\u2016\n = ArithmeticFunction.vonMangoldt n := by\n rw [show (ArithmeticFunction.vonMangoldt n : \u2102)\n = ((ArithmeticFunction.vonMangoldt n : \u211d) : \u2102) by push_cast; ring,\n Complex.norm_real]\n exact abs_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n have h2 : \u2016((n : \u2102)) ^ (2 : \u2102)\u2016 = (n : \u211d) ^ 2 := by\n rw [show ((n : \u2102)) ^ (2 : \u2102) = ((n : \u2102)) ^ (2 : \u2115) by\n exact_mod_cast rfl, norm_pow]\n rw [show ((n : \u2102)) = ((n : \u211d) : \u2102) by push_cast; ring, Complex.norm_real]\n exact abs_of_nonneg (by positivity)\n rw [h1, h2]\n\n/-- The antiderivative derivative fact: d/dx [\u2212(log x + 1)/x] = log x/x\u00b2. -/\nlemma hasDerivAt_neg_log_add_one_div {x : \u211d} (hx0 : x \u2260 0) :\n HasDerivAt (fun y => -(Real.log y + 1) / y) (Real.log x / x ^ 2) x := by\n have h1 := ((Real.hasDerivAt_log hx0).add_const 1).div (hasDerivAt_id' x) hx0\n have h2 := h1.neg\n convert h2 using 1\n \u00b7 ext y\n simp [neg_div]\n \u00b7 simp only [id_eq]\n field_simp\n ring\n\n/-- \u2212(log x + 1)/x \u2192 0 as x \u2192 \u221e. -/\nlemma tendsto_neg_log_add_one_div :\n Tendsto (fun y => -(Real.log y + 1) / y) atTop (\ud835\udcdd 0) := by\n have hA : Tendsto (fun x => Real.log x / x) atTop (\ud835\udcdd 0) := by\n have h := tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero\n simpa using h\n have hB : Tendsto (fun x => (1 : \u211d) / x) atTop (\ud835\udcdd 0) :=\n tendsto_one_div_atTop_nhds_zero\n have hC : Tendsto (fun x => Real.log x / x + 1 / x) atTop (\ud835\udcdd (0 + 0)) :=\n hA.add hB\n have heq : (fun y => -(Real.log y + 1) / y) = (fun x => -(Real.log x / x + 1 / x)) := by\n ext x\n rw [neg_div, add_div]\n rw [heq]\n simpa using hC.neg\n\n/-- log x/x\u00b2 is integrable on Ioi 3. -/\nlemma integrableOn_log_div_sq :\n IntegrableOn (fun x => Real.log x / x ^ 2) (Set.Ioi (3 : \u211d)) volume := by\n apply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>\n hasDerivAt_neg_log_add_one_div (by\n have h := (Set.mem_Ici.mp hx); linarith))\n \u00b7 intro x hx\n have hx3 : (3 : \u211d) < x := hx\n have hlog : (0 : \u211d) \u2264 Real.log x := Real.log_nonneg (by linarith)\n positivity\n \u00b7 exact tendsto_neg_log_add_one_div\n\n/-- The integral of log x/x\u00b2 over Ioi 3 is (log 3 + 1)/3. -/\nlemma integral_log_div_sq_Ioi_three :\n \u222b x in Set.Ioi (3 : \u211d), Real.log x / x ^ 2 = (Real.log 3 + 1) / 3 := by\n have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n (fun x hx => hasDerivAt_neg_log_add_one_div (by\n have h := (Set.mem_Ici.mp hx); linarith))\n integrableOn_log_div_sq tendsto_neg_log_add_one_div\n rw [h]\n show (0 : \u211d) - (-(Real.log 3 + 1) / 3) = (Real.log 3 + 1) / 3\n ring\n\n/-- log x/x\u00b2 is antitone on Ici 3 (its derivative (1 \u2212 2 log x)/x\u00b3 is\n\u2264 0 for x \u2265 3 since log x \u2265 log 3 \u2265 1). -/\nlemma antitoneOn_log_div_sq :\n AntitoneOn (fun x => Real.log x / x ^ 2) (Set.Ici (3 : \u211d)) := by\n apply antitoneOn_of_deriv_nonpos (convex_Ici 3)\n \u00b7 intro x hx\n have hx0 : x \u2260 0 := by have h := (Set.mem_Ici.mp hx); linarith\n exact ((Real.differentiableAt_log hx0).div (differentiableAt_pow _ _)\n (pow_ne_zero 2 hx0)).continuousAt.continuousWithinAt\n \u00b7 intro x hx\n have hx0 : x \u2260 0 := by\n have h : (3 : \u211d) < x := Set.mem_Ioi.mp (by rwa [Set.interior_Ici] at hx)\n linarith\n exact ((Real.differentiableAt_log hx0).div (differentiableAt_pow _ _)\n (pow_ne_zero 2 hx0)).differentiableWithinAt\n \u00b7 intro x hx\n have hx3 : (3 : \u211d) < x := Set.mem_Ioi.mp (by rwa [Set.interior_Ici] at hx)\n have hx0 : x \u2260 0 := by linarith\n have hlog3 : (1 : \u211d) \u2264 Real.log 3 := by\n have h := Real.log_le_log (Real.exp_pos 1)\n (by linarith [Real.exp_one_lt_d9.le] : Real.exp 1 \u2264 3)\n rwa [Real.log_exp] at h\n have hlogx : (1 : \u211d) \u2264 Real.log x :=\n hlog3.trans (Real.log_le_log (by positivity : (0 : \u211d) < 3) hx3.le)\n have hderiv : deriv (fun y => Real.log y / y ^ 2) x\n = (1 - 2 * Real.log x) / x ^ 3 := by\n have h := (Real.hasDerivAt_log hx0).div (hasDerivAt_pow 2 x) (pow_ne_zero 2 hx0)\n rw [h.deriv]\n congr 1\n field_simp\n ring\n rw [hderiv]\n exact div_nonpos_of_nonpos_of_nonneg (by linarith [hlogx]) (by positivity)\n\n/-- Summability of the log-tail (integral test). -/\nlemma summable_log_div_sq_tail :\n Summable (fun n : \u2115 => Real.log ((n : \u211d) + 4) / ((n : \u211d) + 4) ^ 2) := by\n have h := AntitoneOn.summable_of_integrableOn_Ioi antitoneOn_log_div_sq\n integrableOn_log_div_sq (fun t ht => by\n have ht3 : (3 : \u211d) < t := ht\n have hlog : (0 : \u211d) \u2264 Real.log t := Real.log_nonneg (by linarith)\n positivity)\n -- h : Summable (fun n : \u2115 \u21a6 (fun x => log x / x\u00b2) \u2191n); shift by 4\n have h2 := (summable_nat_add_iff 4).mpr (f := fun n : \u2115 =>\n Real.log (n : \u211d) / (n : \u211d) ^ 2) h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n\n/-- The tail bound: \u03a3_{n\u22654} log n/n\u00b2 \u2264 (log 3 + 1)/3 (integral test). -/\nlemma tsum_log_div_sq_tail_le :\n \u2211' n : \u2115, Real.log ((n : \u211d) + 4) / ((n : \u211d) + 4) ^ 2 \u2264 (Real.log 3 + 1) / 3 := by\n have hle := antitoneOn_log_div_sq.tsum_comp_add_le_integral 3\n integrableOn_log_div_sq (fun t ht => by\n have ht3 : (3 : \u211d) < t := ht\n have hlog : (0 : \u211d) \u2264 Real.log t := Real.log_nonneg (by linarith)\n positivity)\n -- hle : \u2211' n, (fun x => log x/x\u00b2) \u2191(n + 3 + 1) \u2264 \u222b Ioi 3\n rw [integral_log_div_sq_Ioi_three] at hle\n refine hle.trans_eq' ?_\n refine tsum_congr fun n => ?_\n push_cast\n ring_nf\n\n/-- **Piece 1** (D-069 \u00a73): dirichletC2 \u2264 1. The honest value is\n\u2212\u03b6\u2032/\u03b6(2) \u2248 0.56997; the bound here uses \u039b(n) \u2264 log n, the exact head\nn = 2, 3, and the integral-test tail (log 3 + 1)/3 \u2264 0.7. -/\ntheorem dirichletC2_le_one : dirichletC2 \u2264 1 := by\n rw [dirichletC2]\n have hsumm_g : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n -- the log majorant h n = if n = 0 then 0 else log n/n\u00b2, and its tsum split\n set h : \u2115 \u2192 \u211d := fun n => if n = 0 then (0 : \u211d)\n else Real.log n / (n : \u211d) ^ 2 with hh\n have hle_pointwise : \u2200 n : \u2115,\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n \u2264 h n := by\n intro n\n rw [dirichletTerm_norm_eq n, hh]\n rcases eq_or_ne n 0 with rfl | hn\n \u00b7 simp\n \u00b7 rw [if_neg hn, if_neg hn]\n exact div_le_div_of_nonneg_right ArithmeticFunction.vonMangoldt_le_log\n (by positivity : (0 : \u211d) \u2264 (n : \u211d) ^ 2)\n -- summability of h: the tail n + 4 is summable, and the head is finite\n have hsumh : Summable h := by\n have h1 : Summable (fun n : \u2115 => h (n + 4)) := by\n apply summable_log_div_sq_tail.congr\n intro n\n rw [hh]\n show (if (n + 4 : \u2115) = 0 then (0 : \u211d) else Real.log (n + 4) / ((n + 4 : \u2115) : \u211d) ^ 2)\n = Real.log ((n : \u211d) + 4) / ((n : \u211d) + 4) ^ 2\n rw [if_neg (by omega : (n + 4 : \u2115) \u2260 0)]\n push_cast\n ring_nf\n exact (summable_nat_add_iff 4).mp h1\n -- the head/tail split of the h-tsum\n have hsplit : \u2211' n : \u2115, h n = (\u2211 n \u2208 Finset.range 4, h n) + \u2211' n : \u2115, h (n + 4) := by\n exact (sum_add_tsum_nat_add 4 hsumh).symm\n have hhead : \u2211 n \u2208 Finset.range 4, h n = Real.log 2 / 4 + Real.log 3 / 9 := by\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_zero]\n rw [hh]\n simp only [Nat.zero_eq, if_pos, Nat.one_ne_zero, Nat.add_eq_zero_iff,\n OfNat.ofNat_ne_zero, and_self, not_false_eq_true]\n rw [show h 1 = (0 : \u211d) from by rw [hh]; simp]\n rw [show h 2 = Real.log 2 / 4 from by\n rw [hh]; rw [if_neg (by norm_num : (2 : \u2115) \u2260 0)]; push_cast; ring_nf]\n rw [show h 3 = Real.log 3 / 9 from by\n rw [hh]; rw [if_neg (by norm_num : (3 : \u2115) \u2260 0)]; push_cast; ring_nf]\n ring\n have htail : \u2211' n : \u2115, h (n + 4) \u2264 (Real.log 3 + 1) / 3 := by\n have h1 : (\u2211' n : \u2115, h (n + 4))\n = \u2211' n : \u2115, Real.log ((n : \u211d) + 4) / ((n : \u211d) + 4) ^ 2 := by\n refine tsum_congr fun n => ?_\n rw [hh]\n show (if (n + 4 : \u2115) = 0 then (0 : \u211d) else Real.log (n + 4) / ((n + 4 : \u2115) : \u211d) ^ 2)\n = Real.log ((n : \u211d) + 4) / ((n : \u211d) + 4) ^ 2\n rw [if_neg (by omega : (n + 4 : \u2115) \u2260 0)]\n push_cast\n ring_nf\n rw [h1]\n exact tsum_log_div_sq_tail_le\n -- assemble\n have hmain : \u2211' n : \u2115,\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n \u2264 Real.log 2 / 4 + Real.log 3 / 9 + (Real.log 3 + 1) / 3 := by\n calc \u2211' n : \u2115,\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n \u2264 \u2211' n : \u2115, h n := Summable.tsum_le_tsum hle_pointwise hsumm_g hsumh\n _ = (\u2211 n \u2208 Finset.range 4, h n) + \u2211' n : \u2115, h (n + 4) := hsplit\n _ \u2264 (Real.log 2 / 4 + Real.log 3 / 9) + (Real.log 3 + 1) / 3 := by\n linarith [hhead, htail]\n -- the numeric fold: log 2 \u2264 0.6932, log 3 \u2264 1.1\n have hlog2 : Real.log 2 \u2264 0.6932 := Real.log_two_lt_d9.le.trans (by norm_num)\n have hlog3 : Real.log 3 \u2264 1.1 := by\n have h3le : (3 : \u211d) \u2264 Real.exp 1.1 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : \u211d) \u2264 1.1 by norm_num) 6\n -- \u03a3_{k<6} 1.1^k/k! = 3.00126\u2026 \u2265 3\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_zero] at h\n norm_num at h\n linarith [h]\n have h2 : Real.log 3 \u2264 Real.log (Real.exp 1.1) :=\n Real.log_le_log (by norm_num : (0 : \u211d) < 3) h3le\n rwa [Real.log_exp] at h2\n have hlog2nn : (0 : \u211d) \u2264 Real.log 2 := Real.log_nonneg (by norm_num)\n have hlog3nn : (0 : \u211d) \u2264 Real.log 3 := Real.log_nonneg (by norm_num)\n linarith [hmain, hlog2, hlog3, hlog2nn, hlog3nn]\n\n/-! ## 7. Pieces 4/5: the reciprocal differences -/\n\n",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"Good: head = lines 1–198 (through §5's near_sum_refPoint_le end), tail = lines 432–508 (pieces 4/5 through `end NguyenRH1 / end`). Now write the new §6 (piece 1) to a temp file, then splice: head + §6-header-and-piece1 + section-header-for-pieces45 + tail.\n\nWait — the tail starts with the `/-- **Pieces 4/5**` docstring but is missing the `/-! ## 6. Pieces 4/5: ... -/` section header (which my bad edit replaced). I'll add a section header in the middle part.\n\nLet me write the middle (§6 complete with the factored helpers + dirichletC2_le_one + the §7 header) to /tmp/litightr_mid.txt via Write, then cat them together.","signature":""},{"type":"text","text":"Writing the corrected §6 (piece 1) to a temp file, then splicing."},{"type":"tool_use","id":"Write_169","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\litightr_mid.tmp","content":"/-! ## 6. Piece 1: the Dirichlet bound at the reference point -/\n\n/-- The Dirichlet term norm at 2: ‖LSeries.term Λ 2 n‖ = (if n = 0 then\n0 else) Λ(n)/n². -/\nlemma dirichletTerm_norm_eq (n : ℕ) :\n ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖\n = if n = 0 then (0 : ℝ)\n else (ArithmeticFunction.vonMangoldt n) / (n : ℝ) ^ 2 := by\n rcases eq_or_ne n 0 with rfl | hn\n · simp [LSeries.term]\n · rw [LSeries.term_def, if_neg hn, norm_div]\n have h1 : ‖(ArithmeticFunction.vonMangoldt n : ℂ)‖\n = ArithmeticFunction.vonMangoldt n := by\n rw [show (ArithmeticFunction.vonMangoldt n : ℂ)\n = ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ) by push_cast; ring,\n Complex.norm_real]\n exact abs_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n have h2 : ‖((n : ℂ)) ^ (2 : ℂ)‖ = (n : ℝ) ^ 2 := by\n rw [show ((n : ℂ)) ^ (2 : ℂ) = ((n : ℂ)) ^ (2 : ℕ) by\n exact_mod_cast rfl, norm_pow]\n rw [show ((n : ℂ)) = ((n : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n exact abs_of_nonneg (by positivity)\n rw [h1, h2]\n\n/-- The antiderivative derivative fact: d/dx [−(log x + 1)/x] = log x/x². -/\nlemma hasDerivAt_neg_log_add_one_div {x : ℝ} (hx0 : x ≠ 0) :\n HasDerivAt (fun y => -(Real.log y + 1) / y) (Real.log x / x ^ 2) x := by\n have h1 := ((Real.hasDerivAt_log hx0).add_const 1).div (hasDerivAt_id' x) hx0\n have h2 := h1.neg\n convert h2 using 1\n · ext y\n simp [neg_div]\n · simp only [id_eq]\n field_simp\n ring\n\n/-- −(log x + 1)/x → 0 as x → ∞. -/\nlemma tendsto_neg_log_add_one_div :\n Tendsto (fun y => -(Real.log y + 1) / y) atTop (𝓝 0) := by\n have hA : Tendsto (fun x => Real.log x / x) atTop (𝓝 0) := by\n have h := tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero\n simpa using h\n have hB : Tendsto (fun x => (1 : ℝ) / x) atTop (𝓝 0) :=\n tendsto_one_div_atTop_nhds_zero\n have hC : Tendsto (fun x => Real.log x / x + 1 / x) atTop (𝓝 (0 + 0)) :=\n hA.add hB\n have heq : (fun y => -(Real.log y + 1) / y) = (fun x => -(Real.log x / x + 1 / x)) := by\n ext x\n rw [neg_div, add_div]\n rw [heq]\n simpa using hC.neg\n\n/-- log x/x² is integrable on Ioi 3. -/\nlemma integrableOn_log_div_sq :\n IntegrableOn (fun x => Real.log x / x ^ 2) (Set.Ioi (3 : ℝ)) volume := by\n apply integrableOn_Ioi_deriv_of_nonneg' (fun x hx =>\n hasDerivAt_neg_log_add_one_div (by\n have h := (Set.mem_Ici.mp hx); linarith))\n · intro x hx\n have hx3 : (3 : ℝ) < x := hx\n have hlog : (0 : ℝ) ≤ Real.log x := Real.log_nonneg (by linarith)\n positivity\n · exact tendsto_neg_log_add_one_div\n\n/-- The integral of log x/x² over Ioi 3 is (log 3 + 1)/3. -/\nlemma integral_log_div_sq_Ioi_three :\n ∫ x in Set.Ioi (3 : ℝ), Real.log x / x ^ 2 = (Real.log 3 + 1) / 3 := by\n have h := integral_Ioi_of_hasDerivAt_of_tendsto'\n (fun x hx => hasDerivAt_neg_log_add_one_div (by\n have h := (Set.mem_Ici.mp hx); linarith))\n integrableOn_log_div_sq tendsto_neg_log_add_one_div\n rw [h]\n show (0 : ℝ) - (-(Real.log 3 + 1) / 3) = (Real.log 3 + 1) / 3\n ring\n\n/-- log x/x² is antitone on Ici 3 (its derivative (1 − 2 log x)/x³ is\n≤ 0 for x ≥ 3 since log x ≥ log 3 ≥ 1). -/\nlemma antitoneOn_log_div_sq :\n AntitoneOn (fun x => Real.log x / x ^ 2) (Set.Ici (3 : ℝ)) := by\n apply antitoneOn_of_deriv_nonpos (convex_Ici 3)\n · intro x hx\n have hx0 : x ≠ 0 := by have h := (Set.mem_Ici.mp hx); linarith\n exact ((Real.differentiableAt_log hx0).div (differentiableAt_pow _ _)\n (pow_ne_zero 2 hx0)).continuousAt.continuousWithinAt\n · intro x hx\n have hx0 : x ≠ 0 := by\n have h : (3 : ℝ) < x := Set.mem_Ioi.mp (by rwa [Set.interior_Ici] at hx)\n linarith\n exact ((Real.differentiableAt_log hx0).div (differentiableAt_pow _ _)\n (pow_ne_zero 2 hx0)).differentiableWithinAt\n · intro x hx\n have hx3 : (3 : ℝ) < x := Set.mem_Ioi.mp (by rwa [Set.interior_Ici] at hx)\n have hx0 : x ≠ 0 := by linarith\n have hlog3 : (1 : ℝ) ≤ Real.log 3 := by\n have h := Real.log_le_log (Real.exp_pos 1)\n (by linarith [Real.exp_one_lt_d9.le] : Real.exp 1 ≤ 3)\n rwa [Real.log_exp] at h\n have hlogx : (1 : ℝ) ≤ Real.log x :=\n hlog3.trans (Real.log_le_log (by positivity : (0 : ℝ) < 3) hx3.le)\n have hderiv : deriv (fun y => Real.log y / y ^ 2) x\n = (1 - 2 * Real.log x) / x ^ 3 := by\n have h := (Real.hasDerivAt_log hx0).div (hasDerivAt_pow 2 x) (pow_ne_zero 2 hx0)\n rw [h.deriv]\n congr 1\n field_simp\n ring\n rw [hderiv]\n exact div_nonpos_of_nonpos_of_nonneg (by linarith [hlogx]) (by positivity)\n\n/-- Summability of the log-tail (integral test). -/\nlemma summable_log_div_sq_tail :\n Summable (fun n : ℕ => Real.log ((n : ℝ) + 4) / ((n : ℝ) + 4) ^ 2) := by\n have h := AntitoneOn.summable_of_integrableOn_Ioi antitoneOn_log_div_sq\n integrableOn_log_div_sq (fun t ht => by\n have ht3 : (3 : ℝ) < t := ht\n have hlog : (0 : ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)\n positivity)\n -- h : Summable (fun n : ℕ ↦ (fun x => log x / x²) ↑n); shift by 4\n have h2 := (summable_nat_add_iff 4).mpr (f := fun n : ℕ =>\n Real.log (n : ℝ) / (n : ℝ) ^ 2) h\n refine h2.congr fun n => ?_\n push_cast\n ring_nf\n\n/-- The tail bound: Σ_{n≥4} log n/n² ≤ (log 3 + 1)/3 (integral test). -/\nlemma tsum_log_div_sq_tail_le :\n ∑' n : ℕ, Real.log ((n : ℝ) + 4) / ((n : ℝ) + 4) ^ 2 ≤ (Real.log 3 + 1) / 3 := by\n have hle := antitoneOn_log_div_sq.tsum_comp_add_le_integral 3\n integrableOn_log_div_sq (fun t ht => by\n have ht3 : (3 : ℝ) < t := ht\n have hlog : (0 : ℝ) ≤ Real.log t := Real.log_nonneg (by linarith)\n positivity)\n -- hle : ∑' n, (fun x => log x/x²) ↑(n + 3 + 1) ≤ ∫ Ioi 3\n rw [integral_log_div_sq_Ioi_three] at hle\n refine hle.trans_eq' ?_\n refine tsum_congr fun n => ?_\n push_cast\n ring_nf\n\n/-- **Piece 1** (D-069 §3): dirichletC2 ≤ 1. The honest value is\n−ζ′/ζ(2) ≈ 0.56997; the bound here uses Λ(n) ≤ log n, the exact head\nn = 2, 3, and the integral-test tail (log 3 + 1)/3 ≤ 0.7. -/\ntheorem dirichletC2_le_one : dirichletC2 ≤ 1 := by\n rw [dirichletC2]\n have hsumm_g : Summable (fun n : ℕ =>\n ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n -- the log majorant h n = if n = 0 then 0 else log n/n², and its tsum split\n set h : ℕ → ℝ := fun n => if n = 0 then (0 : ℝ)\n else Real.log n / (n : ℝ) ^ 2 with hh\n have hle_pointwise : ∀ n : ℕ,\n ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖\n ≤ h n := by\n intro n\n rw [dirichletTerm_norm_eq n, hh]\n rcases eq_or_ne n 0 with rfl | hn\n · simp\n · rw [if_neg hn, if_neg hn]\n exact div_le_div_of_nonneg_right ArithmeticFunction.vonMangoldt_le_log\n (by positivity : (0 : ℝ) ≤ (n : ℝ) ^ 2)\n -- summability of h: the tail n + 4 is summable, and the head is finite\n have hsumh : Summable h := by\n have h1 : Summable (fun n : ℕ => h (n + 4)) := by\n apply summable_log_div_sq_tail.congr\n intro n\n rw [hh]\n show (if (n + 4 : ℕ) = 0 then (0 : ℝ) else Real.log (n + 4) / ((n + 4 : ℕ) : ℝ) ^ 2)\n = Real.log ((n : ℝ) + 4) / ((n : ℝ) + 4) ^ 2\n rw [if_neg (by omega : (n + 4 : ℕ) ≠ 0)]\n push_cast\n ring_nf\n exact (summable_nat_add_iff 4).mp h1\n -- the head/tail split of the h-tsum\n have hsplit : ∑' n : ℕ, h n = (∑ n ∈ Finset.range 4, h n) + ∑' n : ℕ, h (n + 4) := by\n exact (sum_add_tsum_nat_add 4 hsumh).symm\n have hhead : ∑ n ∈ Finset.range 4, h n = Real.log 2 / 4 + Real.log 3 / 9 := by\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_zero]\n rw [hh]\n simp only [Nat.zero_eq, if_pos, Nat.one_ne_zero, Nat.add_eq_zero_iff,\n OfNat.ofNat_ne_zero, and_self, not_false_eq_true]\n rw [show h 1 = (0 : ℝ) from by rw [hh]; simp]\n rw [show h 2 = Real.log 2 / 4 from by\n rw [hh]; rw [if_neg (by norm_num : (2 : ℕ) ≠ 0)]; push_cast; ring_nf]\n rw [show h 3 = Real.log 3 / 9 from by\n rw [hh]; rw [if_neg (by norm_num : (3 : ℕ) ≠ 0)]; push_cast; ring_nf]\n ring\n have htail : ∑' n : ℕ, h (n + 4) ≤ (Real.log 3 + 1) / 3 := by\n have h1 : (∑' n : ℕ, h (n + 4))\n = ∑' n : ℕ, Real.log ((n : ℝ) + 4) / ((n : ℝ) + 4) ^ 2 := by\n refine tsum_congr fun n => ?_\n rw [hh]\n show (if (n + 4 : ℕ) = 0 then (0 : ℝ) else Real.log (n + 4) / ((n + 4 : ℕ) : ℝ) ^ 2)\n = Real.log ((n : ℝ) + 4) / ((n : ℝ) + 4) ^ 2\n rw [if_neg (by omega : (n + 4 : ℕ) ≠ 0)]\n push_cast\n ring_nf\n rw [h1]\n exact tsum_log_div_sq_tail_le\n -- assemble\n have hmain : ∑' n : ℕ,\n ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖\n ≤ Real.log 2 / 4 + Real.log 3 / 9 + (Real.log 3 + 1) / 3 := by\n calc ∑' n : ℕ,\n ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖\n ≤ ∑' n : ℕ, h n := Summable.tsum_le_tsum hle_pointwise hsumm_g hsumh\n _ = (∑ n ∈ Finset.range 4, h n) + ∑' n : ℕ, h (n + 4) := hsplit\n _ ≤ (Real.log 2 / 4 + Real.log 3 / 9) + (Real.log 3 + 1) / 3 := by\n linarith [hhead, htail]\n -- the numeric fold: log 2 ≤ 0.6932, log 3 ≤ 1.1\n have hlog2 : Real.log 2 ≤ 0.6932 := Real.log_two_lt_d9.le.trans (by norm_num)\n have hlog3 : Real.log 3 ≤ 1.1 := by\n have h3le : (3 : ℝ) ≤ Real.exp 1.1 := by\n have h := Real.sum_le_exp_of_nonneg (show (0 : ℝ) ≤ 1.1 by norm_num) 6\n -- Σ_{k<6} 1.1^k/k! = 3.00126… ≥ 3\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_succ,\n Finset.sum_range_zero] at h\n norm_num at h\n linarith [h]\n have h2 : Real.log 3 ≤ Real.log (Real.exp 1.1) :=\n Real.log_le_log (by norm_num : (0 : ℝ) < 3) h3le\n rwa [Real.log_exp] at h2\n have hlog2nn : (0 : ℝ) ≤ Real.log 2 := Real.log_nonneg (by norm_num)\n have hlog3nn : (0 : ℝ) ≤ Real.log 3 := Real.log_nonneg (by norm_num)\n linarith [hmain, hlog2, hlog3, hlog2nn, hlog3nn]\n\n/-! ## 7. Pieces 4/5: the reciprocal differences -/\n\n"},"extra_content":null}]