{
  "replace_all": false,
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-004-sine-moments.py",
  "old_string": "    ev = np.linalg.eigvalsh(H)  # support ~ [-2 sqrt(2n), 2 sqrt(2n)] for this normalization? no:\n    # entries variance 1 (complex): semicircle radius 2*sqrt(n)\n    ev = ev / np.sqrt(N_GUE)    # now support [-2, 2], bulk density (1/pi)... unfold:\n    # semicircle density rho(x) = (1/(2 pi)) sqrt(4 - x^2); unfold via CDF\n    # take middle 60% and rescale by local mean spacing at 0: spacing(0) = 1/rho(0) = pi\n    lo, hi = int(0.2 * N_GUE), int(0.8 * N_GUE)\n    bulk = ev[lo:hi]\n    bulk = bulk * (1.0 / np.pi) * N_GUE / (0.6 * N_GUE) * len(bulk) * (np.pi / len(bulk))\n    # simpler robust unfolding: rescale so mean consecutive spacing is exactly 1\n    bulk = bulk / np.mean(np.diff(bulk))\n    mid = len(bulk) // 2\n    return bulk[mid - W // 2: mid + W // 2]",
  "new_string": "    ev = np.linalg.eigvalsh(H) / np.sqrt(N_GUE)  # semicircle on [-2, 2]\n    # take middle 60% (bulk) and unfold: rescale to mean spacing exactly 1\n    lo, hi = int(0.2 * N_GUE), int(0.8 * N_GUE)\n    bulk = ev[lo:hi]\n    bulk = bulk / np.mean(np.diff(bulk))\n    mid = len(bulk) // 2\n    return bulk[mid - W // 2: mid + W // 2]"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean",
  "oldString": "  -- 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",
  "newString": "  -- h : Summable (fun n : \u2115 \u21a6 (fun x => log x / x\u00b2) \u2191n); shift by 4\n  have h2 := (summable_nat_add_iff (f := fun n : \u2115 =>\n    Real.log (n : \u211d) / (n : \u211d) ^ 2) 4).mpr h\n  refine h2.congr fun n => ?_\n  push_cast\n  ring_nf",
  "originalFile": "/-\nNguyenRH1/LiTightR.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5f (D-069): the tight\nR-bound from the partial-fraction identity (the reference-point method,\nD-056 \u00a72, with the D-069 honest piece-2 two-unit count).\n\n\u00a71: the \u2102 tsum split (variant of LiCircleBound's tsum_split_finset).\n\u00a72: the near-zero subtype finset `nearZerosSub` + membership.\n\u00a73: the seriesFun difference term + identity.\n\u00a74: the six-piece reference-point decomposition `Rexpr_decomp`.\n\u00a75: piece 2 \u2014 the near sum at s\u2080 = 2+it bounded by ZeroCountProp2.\n\u00a76: pieces 4/5 \u2014 the reciprocal differences \u2264 0.045.\n\nRemaining (5f-ii): piece 1 (dirichletC2 \u2264 0.995), piece 6 (the sharp\ndigamma remainder via the level-2 EM), piece 3 (the far-sum interval\nmachine). (5f-iii): the assembly + the pinch lemma + the capstone\n`logDeriv_riemannZeta_sub_nearZeros_le_tight`.\n\nArchive references: D-069 (design + Findings 1/2), D-056 \u00a72, journal-035.\n-/\nimport Mathlib\nimport NguyenRH1.LiSqueeze\n\nopen Zeta23 Complex Filter Topology MeasureTheory\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The \u2102 tsum split -/\n\n/-- Splitting a summable complex tsum over a finset (the \u2102 variant of\nLiCircleBound's `tsum_split_finset`). -/\nlemma tsum_split_finset_complex {\u03b9 : Type*} [DecidableEq \u03b9] {f : \u03b9 \u2192 \u2102} (hf : Summable f)\n    (s : Finset \u03b9) :\n    \u2211' i, f i = \u2211 i \u2208 s, f i + \u2211' i, (if i \u2208 s then 0 else f i) := by\n  classical\n  have h1 : Summable (fun i => if i \u2208 s then f i else 0) := by\n    apply Summable.of_norm_bounded hf.norm\n    intro i\n    by_cases hi : i \u2208 s <;> simp [hi]\n  have h2 : Summable (fun i => if i \u2208 s then 0 else f i) := by\n    apply Summable.of_norm_bounded hf.norm\n    intro i\n    by_cases hi : i \u2208 s <;> simp [hi]\n  have h3 : \u2211' i, f i\n      = \u2211' i, ((if i \u2208 s then f i else 0) + (if i \u2208 s then 0 else f i)) := by\n    apply tsum_congr\n    intro i\n    by_cases hi : i \u2208 s <;> simp [hi]\n  rw [h3, Summable.tsum_add h1 h2]\n  congr 1\n  rw [tsum_eq_sum (s := s) (fun b hb => if_neg hb)]\n  exact Finset.sum_congr rfl (fun b hb => if_pos hb)\n\n/-! ## 2. The near-zero subtype finset -/\n\n/-- The near-zero subtype finset: the nontrivial zeros with |\u03b3 \u2212 t| < 1,\nas a finset of the zero subtype (the `seriesFun` index type). The\ncontaining ball: |\u03b3\u2212t| < 1 and 0 < re < 1 give \u2016\u03c1\u2016 \u2264 |re| + |im| <\n|t| + 3. -/\ndef nearZerosSub (t : \u211d) : Finset {\u03c1 : \u2102 // IsNontrivialZero \u03c1} :=\n  (finite_subtype_norm_lt (|t| + 3)).toFinset.filter fun \u03c1 => |\u03c1.1.im - t| < 1\n\nlemma mem_nearZerosSub {t : \u211d} {\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}} :\n    \u03c1 \u2208 nearZerosSub t \u2194 |\u03c1.1.im - t| < 1 := by\n  rw [nearZerosSub, Finset.mem_filter]\n  refine \u27e8fun h => h.2, fun h => \u27e8?_, h\u27e9\u27e9\n  rw [Set.Finite.mem_toFinset]\n  show \u2016\u03c1.1\u2016 < |t| + 3\n  have hle : \u2016\u03c1.1\u2016 \u2264 |\u03c1.1.re| + |\u03c1.1.im| := Complex.norm_le_abs_re_add_abs_im _\n  have hre : |\u03c1.1.re| \u2264 1 := by\n    have h1 : 0 < \u03c1.1.re := \u03c1.2.2.1\n    have h2 : \u03c1.1.re < 1 := \u03c1.2.2.2\n    rw [abs_le]\n    constructor <;> linarith\n  have him : |\u03c1.1.im| \u2264 |t| + 1 := by\n    calc |\u03c1.1.im| = |\u03c1.1.im - t + t| := by rw [sub_add_cancel]\n      _ \u2264 |\u03c1.1.im - t| + |t| := abs_add_le _ _\n      _ \u2264 1 + |t| := by linarith [h]\n      _ = |t| + 1 := by ring\n  linarith [hle, hre, him]\n\n/-! ## 3. The seriesFun difference identity -/\n\n/-- The seriesFun difference term (a def so the tsum split matches\nsyntactically \u2014 no beta-redexes). -/\ndef seriesDiffTerm (s s\u2080 : \u2102) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2102 :=\n  (zeroMult \u03c1.1 : \u2102) * (1 / (s - \u03c1.1) - 1 / (s\u2080 - \u03c1.1))\n\n/-- The difference series is summable (the two seriesFun summabilities). -/\ntheorem seriesDiffTerm_summable (s s\u2080 : \u2102) :\n    Summable (seriesDiffTerm s s\u2080) := by\n  apply Summable.congr ((seriesSummable s).sub (seriesSummable s\u2080))\n  intro \u03c1\n  show seriesTerm s \u03c1 - seriesTerm s\u2080 \u03c1 = seriesDiffTerm s s\u2080 \u03c1\n  rw [seriesDiffTerm, seriesTerm, seriesTerm]\n  ring\n\n/-- seriesFun s \u2212 seriesFun s\u2080 as the termwise difference series. -/\ntheorem seriesFun_sub_seriesFun (s s\u2080 : \u2102) :\n    seriesFun s - seriesFun s\u2080 = \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n      seriesDiffTerm s s\u2080 \u03c1 := by\n  rw [seriesFun, seriesFun, \u2190 (seriesSummable s).tsum_sub (seriesSummable s\u2080)]\n  refine tsum_congr fun \u03c1 => ?_\n  show seriesTerm s \u03c1 - seriesTerm s\u2080 \u03c1 = seriesDiffTerm s s\u2080 \u03c1\n  rw [seriesDiffTerm, seriesTerm, seriesTerm]\n  ring\n\n/-! ## 4. The reference-point decomposition -/\n\n/-- **The six-piece reference-point decomposition** (D-056 \u00a72, D-069 \u00a73):\nwith both s and s\u2080 good (so `partialFraction_identity` applies at both \u2014\nB cancels), the R-expression at s equals: the reference value, minus the\nnear sum at s\u2080, plus the far difference series, minus the elementary\ndifferences, minus the digamma difference. -/\ntheorem Rexpr_decomp (hZC : ZeroCountProp) {s s\u2080 : \u2102}\n    (hs : riemannZeta s \u2260 0) (hs0 : s \u2260 0) (hs1 : s \u2260 1)\n    (hst : \u2200 n : \u2115, 1 \u2264 n \u2192 s \u2260 -2 * (n : \u2102))\n    (hs\u2080 : riemannZeta s\u2080 \u2260 0) (hs\u20800 : s\u2080 \u2260 0) (hs\u20801 : s\u2080 \u2260 1)\n    (hs\u2080t : \u2200 n : \u2115, 1 \u2264 n \u2192 s\u2080 \u2260 -2 * (n : \u2102)) (t : \u211d) :\n    logDeriv riemannZeta s\n        - \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u2102) / (s - \u03c1.1)\n      = logDeriv riemannZeta s\u2080\n        - \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u2102) / (s\u2080 - \u03c1.1)\n        + (\u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n            if \u03c1 \u2208 nearZerosSub t then (0 : \u2102) else seriesDiffTerm s s\u2080 \u03c1)\n        - (1 / s - 1 / s\u2080) - (1 / (s - 1) - 1 / (s\u2080 - 1))\n        - (Complex.digamma (s / 2) - Complex.digamma (s\u2080 / 2)) / 2 := by\n  obtain \u27e8B, hB\u27e9 := partialFraction_identity hZC\n  have hsid := hB s hs hs0 hs1 hst\n  have hs\u2080id := hB s\u2080 hs\u2080 hs\u20800 hs\u20801 hs\u2080t\n  have hdiff := seriesFun_sub_seriesFun s s\u2080\n  have hsplit := tsum_split_finset_complex (seriesDiffTerm_summable s s\u2080) (nearZerosSub t)\n  have hnear : \u2211 \u03c1 \u2208 nearZerosSub t, seriesDiffTerm s s\u2080 \u03c1\n      = \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u2102) / (s - \u03c1.1)\n        - \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u2102) / (s\u2080 - \u03c1.1) := by\n    rw [\u2190 Finset.sum_sub_distrib]\n    refine Finset.sum_congr rfl fun \u03c1 _ => ?_\n    rw [seriesDiffTerm, div_eq_mul_one_div, div_eq_mul_one_div]\n    ring\n  linear_combination hsid - hs\u2080id + hdiff + hsplit + hnear\n\n/-! ## 5. Piece 2: the near sum at the reference point -/\n\n/-- **Piece 2** (D-069 \u00a73, honest two-unit form): the near sum at\ns\u2080 = 2 + it is bounded by the ZeroCountProp2 count, since\n|s\u2080 \u2212 \u03c1| \u2265 2 \u2212 re \u03c1 \u2265 1 for every nontrivial zero. -/\ntheorem near_sum_refPoint_le (hZC2 : ZeroCountProp2) {t : \u211d} (ht : 10 \u2264 t) :\n    \u2016\u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u2102) / ((2 + t * Complex.I) - \u03c1.1)\u2016\n      \u2264 0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7 := by\n  classical\n  have hterm : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub t \u2192\n      \u2016(zeroMult \u03c1.1 : \u2102) / ((2 + t * Complex.I) - \u03c1.1)\u2016 \u2264 (zeroMult \u03c1.1 : \u211d) := by\n    intro \u03c1 _\n    have h\u03c1re : \u03c1.1.re < 1 := \u03c1.2.2.2\n    have h1 : (1 : \u211d) \u2264 \u2016(2 + t * Complex.I) - \u03c1.1\u2016 := by\n      have hre : ((2 + t * Complex.I) - \u03c1.1).re = 2 - \u03c1.1.re := by simp\n      have h := abs_re_le_norm ((2 + t * Complex.I) - \u03c1.1)\n      rw [hre] at h\n      have h2 : (1 : \u211d) \u2264 |2 - \u03c1.1.re| := by\n        rw [abs_of_nonneg (by linarith)]\n        linarith\n      exact h2.trans h\n    rw [norm_div]\n    have h2 : \u2016(zeroMult \u03c1.1 : \u2102)\u2016 = (zeroMult \u03c1.1 : \u211d) := by\n      rw [show (zeroMult \u03c1.1 : \u2102) = ((zeroMult \u03c1.1 : \u211d) : \u2102) by push_cast; ring,\n        Complex.norm_real]\n      exact abs_of_nonneg (Nat.cast_nonneg _)\n    rw [h2]\n    calc (zeroMult \u03c1.1 : \u211d) / \u2016(2 + t * Complex.I) - \u03c1.1\u2016\n        \u2264 (zeroMult \u03c1.1 : \u211d) / 1 :=\n          div_le_div_of_nonneg_left (Nat.cast_nonneg _)\n            (by norm_num : (0 : \u211d) < 1) h1\n      _ = (zeroMult \u03c1.1 : \u211d) := div_one _\n  have hbridge : \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u211d)\n      = \u2211 \u03c1 \u2208 (nearZerosSub t).image (fun \u03c1 => \u03c1.1), (zeroMult \u03c1 : \u211d) := by\n    rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]\n  have hsub : (nearZerosSub t).image (fun \u03c1 => \u03c1.1)\n      \u2286 (zeroAbsWindow_finite t).toFinset := by\n    intro \u03c1 h\u03c1\n    rw [Finset.mem_image] at h\u03c1\n    obtain \u27e8\u03c1', h\u03c1'mem, h\u03c1'eq\u27e9 := h\u03c1\n    have hnear := mem_nearZerosSub.mp h\u03c1'mem\n    rw [Set.Finite.mem_toFinset]\n    show IsNontrivialZero \u03c1 \u2227 |\u03c1.im - t| \u2264 1\n    rw [\u2190 h\u03c1'eq]\n    exact \u27e8\u03c1'.2, hnear.le\u27e9\n  calc \u2016\u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u2102) / ((2 + t * Complex.I) - \u03c1.1)\u2016\n      \u2264 \u2211 \u03c1 \u2208 nearZerosSub t, \u2016(zeroMult \u03c1.1 : \u2102) / ((2 + t * Complex.I) - \u03c1.1)\u2016 :=\n        norm_sum_le _ _\n    _ \u2264 \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u211d) := Finset.sum_le_sum hterm\n    _ = \u2211 \u03c1 \u2208 (nearZerosSub t).image (fun \u03c1 => \u03c1.1), (zeroMult \u03c1 : \u211d) := hbridge\n    _ \u2264 \u2211 \u03c1 \u2208 (zeroAbsWindow_finite t).toFinset, (zeroMult \u03c1 : \u211d) :=\n        Finset.sum_le_sum_of_subset_of_nonneg hsub (fun \u03c1 _ _ => Nat.cast_nonneg _)\n    _ = (((zeroAbsWindow_finite t).toFinset.sum fun \u03c1 => zeroMult \u03c1) : \u211d) := rfl\n    _ \u2264 0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7 :=\n        hZC2 t ht\n\n/-! ## 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 [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 (2 : \u2102) = ((2 : \u2115) : \u2102) by norm_num, cpow_natCast, norm_pow,\n        Complex.norm_natCast]\n    rw [h1, h2, if_neg hn]\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  rw [show (fun y => -((Real.log y + 1) / y))\n      = -((fun x => Real.log x + 1) / fun x => x) from by\n        ext y; simp only [Pi.neg_apply, Pi.div_apply]]\n  rw [show Real.log x / x ^ 2 = -((x\u207b\u00b9 * x - (Real.log x + 1) * 1) / x ^ 2) from by\n    rw [inv_mul_cancel\u2080 hx0]; ring]\n  exact h2\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 := Real.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) := by\n    simpa only [one_div] using tendsto_inv_atTop_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 [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 2)\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 [interior_Ici] at hx)\n      linarith\n    exact ((Real.differentiableAt_log hx0).div (differentiableAt_pow 2)\n      (pow_ne_zero 2 hx0)).differentiableWithinAt\n  \u00b7 intro x hx\n    have hx3 : (3 : \u211d) < x := Set.mem_Ioi.mp (by rwa [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      have h' : HasDerivAt (fun y => Real.log y / y ^ 2)\n          ((x\u207b\u00b9 * x ^ 2 - Real.log x * (\u21912 * x ^ (2 - 1))) / (x ^ 2) ^ 2) x := by\n        convert h using 1\n        ext y\n        rw [Pi.div_apply]\n      rw [h'.deriv]\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/-- **Pieces 4/5** (D-056 \u00a72): the elementary reciprocal differences,\neach \u2264 4.5/|t|\u00b2 \u2264 0.045 (|s\u2080 \u2212 s| = |2 \u2212 \u03c3| \u2264 4.5; \u2016s\u2016, \u2016s\u2080\u2016 \u2265 t). -/\ntheorem one_div_diff_le {t : \u211d} (ht : 10 \u2264 t) {s : \u2102}\n    (h\u03c3lo : -5 / 2 \u2264 s.re) (h\u03c3hi : s.re \u2264 3) (him : s.im = t) (hs0 : s \u2260 0) :\n    \u20161 / s - 1 / (2 + t * Complex.I)\u2016 \u2264 0.045 \u2227\n      \u20161 / (s - 1) - 1 / ((2 + t * Complex.I) - 1)\u2016 \u2264 0.045 := by\n  have ht0 : (0 : \u211d) < t := by linarith\n  -- the difference s\u2080 \u2212 s is the real (2 \u2212 s.re)\n  have hdiff : (2 + t * Complex.I) - s = ((2 - s.re : \u211d) : \u2102) := by\n    rw [Complex.ext_iff]\n    constructor\n    \u00b7 simp\n    \u00b7 simp [him]\n  have hsdiff : \u2016(2 + t * Complex.I) - s\u2016 = |2 - s.re| := by\n    rw [hdiff]\n    exact Complex.norm_real _\n  have hsdiffle : \u2016(2 + t * Complex.I) - s\u2016 \u2264 4.5 := by\n    rw [hsdiff, abs_le]\n    constructor <;> linarith\n  have hs_norm : (t : \u211d) \u2264 \u2016s\u2016 := by\n    have h := abs_im_le_norm s\n    rw [him, abs_of_nonneg ht0.le] at h\n    exact h\n  have hs0_norm : (t : \u211d) \u2264 \u20162 + t * Complex.I\u2016 := by\n    have h := abs_im_le_norm (2 + t * Complex.I)\n    rw [show (2 + t * Complex.I).im = t by simp, abs_of_nonneg ht0.le] at h\n    exact h\n  have hsm1_norm : (t : \u211d) \u2264 \u2016s - 1\u2016 := by\n    have h := abs_im_le_norm (s - 1)\n    rw [show (s - 1).im = t by simp [him], abs_of_nonneg ht0.le] at h\n    exact h\n  have hs0m1_norm : (t : \u211d) \u2264 \u2016(2 + t * Complex.I) - 1\u2016 := by\n    have h := abs_im_le_norm ((2 + t * Complex.I) - 1)\n    rw [show ((2 + t * Complex.I) - 1).im = t by simp, abs_of_nonneg ht0.le] at h\n    exact h\n  have hprods : (100 : \u211d) \u2264 \u2016s\u2016 * \u20162 + t * Complex.I\u2016 := by\n    have h1 := mul_le_mul hs_norm hs0_norm ht0.le (by positivity : (0 : \u211d) \u2264 \u2016s\u2016)\n    nlinarith [h1, ht]\n  have hprods1 : (100 : \u211d) \u2264 \u2016s - 1\u2016 * \u2016(2 + t * Complex.I) - 1\u2016 := by\n    have h1 := mul_le_mul hsm1_norm hs0m1_norm ht0.le (by positivity : (0 : \u211d) \u2264 \u2016s - 1\u2016)\n    nlinarith [h1, ht]\n  constructor\n  \u00b7 -- 1/s \u2212 1/s\u2080\n    have hs\u20800 : (2 + t * Complex.I) \u2260 0 := by\n      intro h\n      rw [h, norm_zero] at hs0_norm\n      linarith\n    rw [div_sub_div _ _ hs0 hs\u20800]\n    have hnum : 1 * (2 + t * Complex.I) - s * 1 = (2 + t * Complex.I) - s := by ring\n    rw [hnum, norm_div, norm_mul]\n    calc \u2016(2 + t * Complex.I) - s\u2016 / (\u2016s\u2016 * \u20162 + t * Complex.I\u2016)\n        \u2264 4.5 / (\u2016s\u2016 * \u20162 + t * Complex.I\u2016) :=\n          div_le_div_of_nonneg_right hsdiffle (by positivity)\n      _ \u2264 4.5 / 100 := div_le_div_of_nonneg_left (by norm_num) (by norm_num) hprods\n      _ = 0.045 := by norm_num\n  \u00b7 -- 1/(s\u22121) \u2212 1/(s\u2080\u22121)\n    have hs1 : s - 1 \u2260 0 := by\n      intro h\n      rw [h, norm_zero] at hsm1_norm\n      linarith\n    have hs\u20801 : (2 + t * Complex.I) - 1 \u2260 0 := by\n      intro h\n      rw [h, norm_zero] at hs0m1_norm\n      linarith\n    rw [div_sub_div _ _ hs1 hs\u20801]\n    have hnum : 1 * ((2 + t * Complex.I) - 1) - (s - 1) * 1\n        = (2 + t * Complex.I) - s := by ring\n    rw [hnum, norm_div, norm_mul]\n    calc \u2016(2 + t * Complex.I) - s\u2016 / (\u2016s - 1\u2016 * \u2016(2 + t * Complex.I) - 1\u2016)\n        \u2264 4.5 / (\u2016s - 1\u2016 * \u2016(2 + t * Complex.I) - 1\u2016) :=\n          div_le_div_of_nonneg_right hsdiffle (by positivity)\n      _ \u2264 4.5 / 100 := div_le_div_of_nonneg_left (by norm_num) (by norm_num) hprods1\n      _ = 0.045 := by norm_num\n\nend NguyenRH1\n\nend\n",
  "structuredPatch": [
    {
      "oldStart": 314,
      "oldLines": 8,
      "newStart": 314,
      "newLines": 8,
      "lines": [
        "       have hlog : (0 : \u211d) \u2264 Real.log t := Real.log_nonneg (by linarith)",
        "       positivity)",
        "   -- h : Summable (fun n : \u2115 \u21a6 (fun x => log x / x\u00b2) \u2191n); shift by 4",
        "-  have h2 := (summable_nat_add_iff 4).mpr (f := fun n : \u2115 =>",
        "-    Real.log (n : \u211d) / (n : \u211d) ^ 2) h",
        "+  have h2 := (summable_nat_add_iff (f := fun n : \u2115 =>",
        "+    Real.log (n : \u211d) / (n : \u211d) ^ 2) 4).mpr h",
        "   refine h2.congr fun n => ?_",
        "   push_cast",
        "   ring_nf"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}