{
  "replace_all": false,
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1.lean",
  "old_string": "  NguyenRH1.LiContour      \u2014 tier ii\u2032-4: L3 zero-avoiding T (pigeonhole)\n                             + L1 kernel bounds + zeroMult(\u22122) = 1",
  "new_string": "  NguyenRH1.LiContour      \u2014 tier ii\u2032-4: L3 zero-avoiding T (pigeonhole)\n                             + L1 kernel bounds + zeroMult(\u22122) = 1\n  NguyenRH1.LiRBound       \u2014 tier ii\u2032-5b: the level-2 Euler\u2013Maclaurin \u03b6\n                             representation (re > \u22121) + the polynomial\n                             disc bound \u2016\u03b6\u2016 \u2264 (3/4)|t|\u00b2"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean",
  "oldString": "    have hsplit : (\u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9)\n        = \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n          + \u2211' n : \u2115, ((((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9) := by\n      rw [\u2190 hker_summ.sum_add_tsum_nat_add N]",
  "newString": "    have hsplit : (\u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9)\n        = \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n          + \u2211' n : \u2115, ((((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9) := by\n      have h := hker_summ.sum_add_tsum_nat_add N\n      simp only [] at h\n      rw [\u2190 h]",
  "originalFile": "/-\nNguyenRH1/LiDigammaLeft.lean \u2014 tier ii\u2032 sub-stage 5e-ii (D-068 \u00a71 C2):\nthe two digamma bounds feeding the circle estimate of ii\u2032-5e-v.\n\n* \u00a71 `tsum_one_div_sub_telescope`: \u2211'\u2099 (1/(n+N) \u2212 1/(n+N+1)) = 1/N\n  (partial-sum telescope + squeeze).\n* \u00a72 `norm_digamma_le_of_two_le_re`: \u2016\u03c8(w)\u2016 \u2264 20\u00b7log(2+\u2016w\u2016) for\n  re w \u2265 2, |im w| \u2264 5 \u2014 the Weierstrass-series route (Zeta23\n  `DigammaSeries.digamma_series`): \u03a3'_n w/((n+1)(w+n+1)) split at\n  N = \u2308re w\u2309\u208a (head via the harmonic bound `harmonic_le_one_add_log`,\n  tail via \u00a71's telescope); the positive-integer case via `digamma_one`\n  + the recurrence (`digamma_natCast_eq`).\n* \u00a73 (C): `digamma_recip_sum_le` \u2014 the separated reciprocal sum bound\n  \u03a3_{j<m} \u2016w+j\u2016\u207b\u00b9 \u2264 2/c + 2 + 2\u00b7log m for dist(w, \u2212\u2115) \u2265 c (V-split).\n* \u00a74 (A): `norm_digamma_le_of_dist_nat` \u2014 the near-axis left-plane bound\n  for re w \u2264 2, dist(w,\u2212\u2115) \u2265 c (recurrence `digamma_add_natCast` + \u00a73 +\n  the landing-zone bound via \u00a72 or StirlingVert).\n* \u00a75 (G): `logDeriv_Gamma\u211d_eq` \u2014 logDeriv \u0393R s = \u2212(log \u03c0)/2 + \u00bd\u03c8(s/2)\n  for im s \u2260 0 (the m-fold shift: `gamma_mul_prod` + the EventuallyEq\n  machinery of 5d).\n\nArchive references: D-068 \u00a71 (C2) + \u00a77, journal-025/026.\n-/\nimport Mathlib\nimport Zeta23.GammaFacts.Series\nimport Zeta23.GammaFacts.StirlingVert\nimport NguyenRH1.LiReflect\nimport NguyenRH1.LiTrivialZeros\n\nopen Zeta23 Complex Filter Topology MeasureTheory\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The telescoping tail -/\n\n/-- The partial sums of the telescoping series. -/\ntheorem sum_range_one_div_sub (N M : \u2115) :\n    \u2211 n \u2208 Finset.range M, ((1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1))\n      = 1 / (N : \u211d) - 1 / ((M : \u211d) + N) := by\n  have h := Finset.sum_range_sub' (fun n : \u2115 => (1 : \u211d) / ((n : \u211d) + N)) M\n  rw [Nat.cast_zero, zero_add] at h\n  rw [\u2190 h]\n  apply Finset.sum_congr rfl\n  intro n _\n  push_cast\n  ring_nf\n\n/-- **The telescoping tail, HasSum form**. -/\ntheorem hasSum_one_div_sub_telescope (N : \u2115) (hN : 1 \u2264 N) :\n    HasSum (fun n : \u2115 => (1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1))\n      (1 / (N : \u211d)) := by\n  have hNR : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN\n  have hnonneg : \u2200 n : \u2115, (0 : \u211d) \u2264 1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1) := by\n    intro n\n    have h1 : (0 : \u211d) < (n : \u211d) + N := by\n      have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n      linarith [hNR, h2]\n    have h3 : 1 / ((n : \u211d) + N + 1) \u2264 1 / ((n : \u211d) + N) :=\n      one_div_le_one_div_of_le h1 (by linarith)\n    linarith [h3]\n  have hlim0 : Tendsto (fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + N)) atTop (\ud835\udcdd 0) := by\n    have h1 : Tendsto (fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + 1)) atTop (\ud835\udcdd 0) :=\n      tendsto_one_div_add_atTop_nhds_zero_nat\n    refine squeeze_zero (f := fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + N))\n      (g := fun M : \u2115 => (1 : \u211d) / ((M : \u211d) + 1)) ?_ ?_ h1\n    \u00b7 intro M\n      positivity\n    \u00b7 intro M\n      apply one_div_le_one_div_of_le (by positivity)\n      have hN1R : (1 : \u211d) \u2264 (N : \u211d) := by exact_mod_cast hN\n      linarith [hN1R]\n  have hlim : Tendsto (fun M : \u2115 => (1 : \u211d) / (N : \u211d) - 1 / ((M : \u211d) + N)) atTop\n      (\ud835\udcdd (1 / (N : \u211d))) := by\n    have h := hlim0.const_sub (1 / (N : \u211d))\n    rwa [sub_zero] at h\n  rw [hasSum_iff_tendsto_nat_of_nonneg hnonneg]\n  convert hlim using 1\n  ext M\n  exact sum_range_one_div_sub N M\n\n/-- **The telescoping tail**: \u2211'\u2099 (1/(n+N) \u2212 1/(n+N+1)) = 1/N for N \u2265 1. -/\ntheorem tsum_one_div_sub_telescope (N : \u2115) (hN : 1 \u2264 N) :\n    \u2211' n : \u2115, ((1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)) = 1 / (N : \u211d) :=\n  (hasSum_one_div_sub_telescope N hN).tsum_eq\n\n/-! ## 2. The right-half-plane bound (B) -/\n\n/-- \u03c8 at positive integers: \u03c8(n) = \u2212\u03b3 + H_{n\u22121} for n \u2265 1. -/\ntheorem digamma_natCast_eq (n : \u2115) (hn : 1 \u2264 n) :\n    Complex.digamma (n : \u2102)\n      = -(Real.eulerMascheroniConstant : \u2102) + ((harmonic (n - 1) : \u211a) : \u2102) := by\n  induction n with\n  | zero => omega\n  | succ k ih =>\n    rcases eq_or_ne k 0 with hk | hk\n    \u00b7 subst hk\n      simp [Complex.digamma_one, harmonic]\n    \u00b7 have hk1 : 1 \u2264 k := Nat.one_le_iff_ne_zero.mpr hk\n      have h1 := ih hk1\n      have hside : \u2200 m : \u2115, (k : \u2102) \u2260 -(m : \u2102) := by\n        intro m h\n        have hre := congrArg Complex.re h\n        simp [Complex.neg_re, Complex.natCast_re] at hre\n        have hmk : (1 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk1\n        have hm0 : (0 : \u211d) \u2264 (m : \u211d) := by positivity\n        linarith\n      have h2 := Complex.digamma_apply_add_one (k : \u2102) hside\n      rw [show ((k + 1 : \u2115) : \u2102) = (k : \u2102) + 1 by push_cast; ring, h2, h1]\n      have hharm : ((harmonic (k + 1 - 1) : \u211a) : \u2102)\n          = ((harmonic (k - 1) : \u211a) : \u2102) + ((k : \u211d) : \u2102)\u207b\u00b9 := by\n        have h3 : k + 1 - 1 = k := by omega\n        rw [h3]\n        have h4 : harmonic k = harmonic (k - 1) + ((k : \u211a))\u207b\u00b9 := by\n          conv_lhs => rw [show k = (k - 1) + 1 by omega]\n          rw [harmonic, Finset.sum_range_succ]\n          have h5 : k - 1 + 1 = k := by omega\n          rw [h5]\n          rw [harmonic]\n        rw [h4]\n        push_cast\n        ring\n      rw [hharm]\n      push_cast\n      ring\n\n/-- The digamma-series majorant g n = \u2016w\u2016/((n+1)(re w+n+1)) is summable\n(dominated by \u2016w\u2016/(n+1)\u00b2) for re w \u2265 2. -/\ntheorem summable_digamma_majorant {w : \u2102} (hwre : 2 \u2264 w.re) :\n    Summable (fun n : \u2115 => \u2016w\u2016 / (((n : \u211d) + 1) * (w.re + (n : \u211d) + 1))) := by\n  have h1 : Summable (fun n : \u2115 => (((n : \u211d) + 1) ^ 2)\u207b\u00b9) := by\n    have h2 : Summable (fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9) := by\n      have h3 := Real.summable_nat_rpow_inv.mpr (by norm_num : (1 : \u211d) < 2)\n      have heq : (fun n : \u2115 => ((n : \u211d) ^ (2 : \u211d))\u207b\u00b9) = fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9 := by\n        funext n\n        rw [show ((2 : \u211d)) = ((2 : \u2115) : \u211d) by norm_num, Real.rpow_natCast]\n      rwa [heq] at h3\n    have h4 := (summable_nat_add_iff 1).mpr h2\n    simpa [add_comm] using h4\n  refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ (h1.mul_left \u2016w\u2016)\n  intro n\n  have hstep : ((n : \u211d) + 1) ^ 2 \u2264 ((n : \u211d) + 1) * (w.re + (n : \u211d) + 1) := by\n    rw [sq]\n    apply mul_le_mul_of_nonneg_left _ (by positivity)\n    have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n    linarith [hwre, h2]\n  calc \u2016w\u2016 / (((n : \u211d) + 1) * (w.re + (n : \u211d) + 1))\n      \u2264 \u2016w\u2016 / (((n : \u211d) + 1) ^ 2) := by\n        apply div_le_div_of_nonneg_left (norm_nonneg _)\n          (show (0 : \u211d) < ((n : \u211d) + 1) ^ 2 by positivity) hstep\n    _ = \u2016w\u2016 * ((((n : \u211d) + 1) ^ 2)\u207b\u00b9) := by rw [div_eq_mul_inv]\n\n/-- The per-term bound: \u20161/(n+1) \u2212 1/(w+n+1)\u2016 \u2264 \u2016w\u2016/((n+1)(re w+n+1)). -/\ntheorem norm_digamma_term_le {w : \u2102} (hwre : 2 \u2264 w.re) (n : \u2115) :\n    \u20161 / ((n : \u2102) + 1) - 1 / (w + n + 1)\u2016\n      \u2264 \u2016w\u2016 / (((n : \u211d) + 1) * (w.re + (n : \u211d) + 1)) := by\n  have hwn1 : w + (n : \u2102) + 1 \u2260 0 := by\n    intro h\n    have h2 := congrArg Complex.re h\n    simp [Complex.add_re, Complex.natCast_re, Complex.one_re] at h2\n    have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n    linarith [hwre, h3, h2]\n  have hident : 1 / ((n : \u2102) + 1) - 1 / (w + n + 1)\n      = w / (((n : \u2102) + 1) * (w + n + 1)) := by\n    field_simp [Nat.cast_add_one_ne_zero n, hwn1]\n    ring\n  have hrew : (w + (n : \u2102) + 1).re = w.re + (n : \u211d) + 1 := by\n    simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n  have hle : w.re + (n : \u211d) + 1 \u2264 \u2016w + (n : \u2102) + 1\u2016 := by\n    have hpos : (0 : \u211d) \u2264 (w + (n : \u2102) + 1).re := by\n      rw [hrew]\n      have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n      linarith [hwre, h3]\n    have h2 := Complex.abs_re_le_norm (w + (n : \u2102) + 1)\n    rwa [abs_of_nonneg hpos, hrew] at h2\n  rw [hident, norm_div, norm_mul, DigammaSeries.norm_natCast_add_one]\n  apply div_le_div_of_nonneg_left (norm_nonneg _)\n  \u00b7 apply mul_pos (by positivity)\n    have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n    linarith [hwre, h3]\n  \u00b7 apply mul_le_mul_of_nonneg_left hle (by positivity)\n\n/-- The harmonic-sum form used in the head split. -/\ntheorem sum_one_div_le_one_add_log (N : \u2115) :\n    \u2211 n \u2208 Finset.range N, (1 : \u211d) / ((n : \u211d) + 1) \u2264 1 + Real.log N := by\n  have h1 : (\u2211 n \u2208 Finset.range N, (1 : \u211d) / ((n : \u211d) + 1)) = (harmonic N : \u211d) := by\n    rw [harmonic, Rat.cast_sum]\n    apply Finset.sum_congr rfl\n    intro i _\n    rw [Rat.cast_inv, Rat.cast_natCast, Nat.cast_add_one, one_div]\n  rw [h1]\n  exact harmonic_le_one_add_log N\n/-- **The right-half-plane digamma bound (B)**: for re w \u2265 2, |im w| \u2264 5,\n\u2016\u03c8(w)\u2016 \u2264 20\u00b7log(2+\u2016w\u2016). Weierstrass series + split at N = \u2308re w\u2309\u208a;\npositive integers via the harmonic identity. -/\ntheorem norm_digamma_le_of_two_le_re {w : \u2102} (hwre : 2 \u2264 w.re) (hwim : |w.im| \u2264 5) :\n    \u2016Complex.digamma w\u2016 \u2264 20 * Real.log (2 + \u2016w\u2016) := by\n  have hw_norm_ge : 2 \u2264 \u2016w\u2016 := by\n    have h1 := Complex.abs_re_le_norm w\n    rw [abs_of_nonneg (by linarith [hwre])] at h1\n    linarith [hwre, h1]\n  have hlog4 : (5 : \u211d) / 3 \u2264 19 * Real.log (2 + \u2016w\u2016) := by\n    have h1 : Real.log 4 \u2264 Real.log (2 + \u2016w\u2016) :=\n      Real.log_le_log (by norm_num) (by linarith [hw_norm_ge])\n    have h2 : (1 : \u211d) < Real.log 4 := by\n      have h4 := Real.log_two_gt_d9.le\n      have h5 : Real.log 4 = 2 * Real.log 2 := by\n        rw [show (4 : \u211d) = 2 ^ 2 by norm_num, Real.log_pow]\n        push_cast\n        ring\n      linarith [h4, h5]\n    nlinarith [h1, h2]\n  by_cases hwint : \u2203 m : \u2124, (m : \u2102) = w\n  \u00b7 -- the positive-integer case: w = \u2191n, n \u2265 2\n    obtain \u27e8m, hm\u27e9 := hwint\n    have hmre : w.re = (m : \u211d) := by rw [\u2190 hm]; simp\n    have hm2 : 2 \u2264 m := by\n      by_contra h\n      push Not at h\n      have h1 : (m : \u211d) \u2264 1 := by exact_mod_cast (show m \u2264 1 by omega)\n      linarith [hwre, hmre, h1]\n    have hn2 : 2 \u2264 m.toNat := by\n      have h1 : (m : \u2124) = ((m.toNat : \u2115) : \u2124) := (Int.toNat_of_nonneg (by omega)).symm\n      rw [h1] at hm2\n      exact_mod_cast hm2\n    set n := m.toNat with hn_def\n    have hwn : w = (n : \u2102) := by\n      rw [\u2190 hm, hn_def]\n      exact_mod_cast (Int.toNat_of_nonneg (by omega : (0 : \u2124) \u2264 m)).symm\n    rw [hwn, digamma_natCast_eq n (by omega)]\n    have h\u03b30 : (0 : \u211d) \u2264 Real.eulerMascheroniConstant :=\n      (by norm_num : (0 : \u211d) \u2264 1 / 2).trans Real.one_half_lt_eulerMascheroniConstant.le\n    have hreal : |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : \u211a) : \u211d)|\n        \u2264 Real.eulerMascheroniConstant + (1 + Real.log ((n : \u211d) - 1)) := by\n      have hH0 : (0 : \u211d) \u2264 ((harmonic (n - 1) : \u211a) : \u211d) := by positivity\n      have hHbound : ((harmonic (n - 1) : \u211a) : \u211d) \u2264 1 + Real.log (n - 1) :=\n        harmonic_le_one_add_log (n - 1)\n      have hlog0 : (0 : \u211d) \u2264 Real.log ((n : \u211d) - 1) := by\n        apply Real.log_nonneg\n        have h1 : (1 : \u211d) \u2264 ((n - 1 : \u2115) : \u211d) := by exact_mod_cast (by omega : 1 \u2264 n - 1)\n        have h2 : ((n - 1 : \u2115) : \u211d) = (n : \u211d) - 1 := by\n          rw [Nat.cast_sub (by omega : 1 \u2264 n)]\n          push_cast\n          ring\n        linarith [h1, h2]\n      have hHlog : ((harmonic (n - 1) : \u211a) : \u211d) \u2264 1 + Real.log ((n : \u211d) - 1) := by\n        refine hHbound.trans ?_\n        have h2 : ((n - 1 : \u2115) : \u211d) = (n : \u211d) - 1 := by\n          rw [Nat.cast_sub (by omega : 1 \u2264 n)]\n          push_cast\n          ring\n        rw [h2]\n      apply abs_le.mpr\n      constructor <;> linarith [h\u03b30, hH0, hHlog, hlog0]\n    have hnrm : \u2016-(Real.eulerMascheroniConstant : \u2102) + ((harmonic (n - 1) : \u211a) : \u2102)\u2016\n        = |(-Real.eulerMascheroniConstant + (harmonic (n - 1) : \u211a) : \u211d)| := by\n      rw [\u2190 Complex.ofReal_ratCast, \u2190 Complex.ofReal_neg, \u2190 Complex.ofReal_add,\n        Complex.norm_real, Real.norm_eq_abs]\n    rw [hnrm]\n    have hlogn1 : Real.log ((n : \u211d) - 1) \u2264 Real.log (2 + \u2016w\u2016) := by\n      have h2 : ((n - 1 : \u2115) : \u211d) = (n : \u211d) - 1 := by\n        rw [Nat.cast_sub (by omega : 1 \u2264 n)]\n        push_cast\n        ring\n      have hpos : (0 : \u211d) < (n : \u211d) - 1 := by\n        have h1 : (1 : \u211d) \u2264 ((n - 1 : \u2115) : \u211d) := by exact_mod_cast (by omega : 1 \u2264 n - 1)\n        linarith [h1, h2]\n      apply Real.log_le_log hpos\n      have hwnorm : \u2016w\u2016 = (n : \u211d) := by rw [hwn, RCLike.norm_natCast]\n      rw [hwnorm]\n      linarith [h2]\n    have h\u03b31 : Real.eulerMascheroniConstant \u2264 1 :=\n      Real.eulerMascheroniConstant_lt_two_thirds.le.trans (by norm_num)\n    linarith [hreal, h\u03b31, hlogn1, hlog4]\n  \u00b7 -- the series case: w off the integers\n    have hcomp : w \u2208 Complex.integerComplement := hwint\n    rw [DigammaSeries.digamma_series hcomp]\n    set A := w.re with hA_def\n    set N := \u2308w.re\u2309\u208a with hN_def\n    have hA0 : (0 : \u211d) < A := by linarith [hwre]\n    have hNA : A \u2264 (N : \u211d) := by rw [hN_def]; exact Nat.le_ceil _\n    have hNA1 : (N : \u211d) \u2264 A + 1 := by\n      have h := Nat.ceil_lt_add_one (show (0 : \u211d) \u2264 w.re by linarith [hwre])\n      have h2 : ((\u2308w.re\u2309\u208a : \u2115) : \u211d) < w.re + 1 := by exact_mod_cast h\n      rw [hN_def]\n      linarith [h2]\n    have hN1 : 1 \u2264 N := by\n      have h1 : (2 : \u2115) \u2264 N := by\n        rw [hN_def]\n        have h2 := Nat.ceil_mono hwre\n        rwa [Nat.ceil_ofNat] at h2\n      omega\n    have hterm_summ : Summable (fun n : \u2115 => \u20161 / ((n : \u2102) + 1) - 1 / (w + n + 1)\u2016) :=\n      Summable.of_nonneg_of_le (fun n => norm_nonneg _) (fun n => norm_digamma_term_le hwre n)\n        (summable_digamma_majorant hwre)\n    -- the kernel: summable + the split bound\n    have hker_summ : Summable (fun n : \u2115 => (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9) := by\n      have h1 : Summable (fun n : \u2115 => (((n : \u211d) + 1) ^ 2)\u207b\u00b9) := by\n        have h2 : Summable (fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9) := by\n          have h3 := Real.summable_nat_rpow_inv.mpr (by norm_num : (1 : \u211d) < 2)\n          have heq : (fun n : \u2115 => ((n : \u211d) ^ (2 : \u211d))\u207b\u00b9)\n              = fun n : \u2115 => (((n : \u211d)) ^ 2)\u207b\u00b9 := by\n            funext n\n            rw [show ((2 : \u211d)) = ((2 : \u2115) : \u211d) by norm_num, Real.rpow_natCast]\n          rwa [heq] at h3\n        have h4 := (summable_nat_add_iff 1).mpr h2\n        simpa [add_comm] using h4\n      refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ h1\n      intro n\n      apply (inv_le_inv\u2080 (by positivity) (by positivity)).mpr\n      rw [sq]\n      apply mul_le_mul_of_nonneg_left _ (by positivity)\n      have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n      linarith [hA0, h2]\n    have hsplit : (\u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9)\n        = \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n          + \u2211' n : \u2115, ((((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9) := by\n      rw [\u2190 hker_summ.sum_add_tsum_nat_add N]\n    -- the head bound\n    have hhead : \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n        \u2264 (1 + Real.log (N : \u211d)) / A := by\n      have hper : \u2200 n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n          \u2264 ((n : \u211d) + 1)\u207b\u00b9 * A\u207b\u00b9 := by\n        intro n\n        have h1 : (0 : \u211d) < ((n : \u211d) + 1) * A := mul_pos (by positivity) hA0\n        have h2 : (0 : \u211d) < ((n : \u211d) + 1) * (A + (n : \u211d) + 1) := by\n          apply mul_pos (by positivity)\n          have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n          linarith [hA0, h3]\n        rw [\u2190 mul_inv]\n        apply (inv_le_inv\u2080 h2 h1).mpr\n        apply mul_le_mul_of_nonneg_left _ (by positivity)\n        have h3 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n        linarith [hA0, h3]\n      have hS' : (\u2211 n \u2208 Finset.range N, ((n : \u211d) + 1)\u207b\u00b9) \u2264 1 + Real.log (N : \u211d) := by\n        have h := sum_one_div_le_one_add_log N\n        simpa [one_div] using h\n      calc \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9\n          \u2264 \u2211 n \u2208 Finset.range N, ((n : \u211d) + 1)\u207b\u00b9 * A\u207b\u00b9 :=\n            Finset.sum_le_sum fun n _ => hper n\n        _ = (\u2211 n \u2208 Finset.range N, ((n : \u211d) + 1)\u207b\u00b9) * A\u207b\u00b9 := by rw [\u2190 Finset.sum_mul]\n        _ \u2264 (1 + Real.log (N : \u211d)) * A\u207b\u00b9 :=\n            mul_le_mul_of_nonneg_right hS' (inv_nonneg.mpr hA0.le)\n        _ = (1 + Real.log (N : \u211d)) / A := by rw [div_eq_mul_inv]\n    -- the tail bound\n    have htail : (\u2211' n : \u2115, ((((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9)\n        \u2264 1 / (N : \u211d) := by\n      have h1 : Summable (fun n : \u2115 => ((((n + N : \u2115) : \u211d) + 1)\n          * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9) :=\n        (summable_nat_add_iff N).mpr hker_summ\n      have hterm : \u2200 n : \u2115, ((((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9\n          \u2264 1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1) := by\n        intro n\n        have hN0 : (0 : \u211d) < (n : \u211d) + N := by\n          have h2 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n          have h3 : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n          linarith [h2, h3]\n        have htele : (1 : \u211d) / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)\n            = (((n : \u211d) + N) * ((n : \u211d) + N + 1))\u207b\u00b9 := by\n          rw [div_sub_div _ _ hN0.ne' (by positivity)]\n          rw [div_eq_iff (by positivity : (0 : \u211d) < ((n : \u211d) + N) * ((n : \u211d) + N + 1))]\n          rw [inv_mul_cancel\u2080 (by positivity : ((n : \u211d) + N) * ((n : \u211d) + N + 1) \u2260 0)]\n          ring\n        rw [htele]\n        have h2 : (0 : \u211d) < ((n : \u211d) + N) * ((n : \u211d) + N + 1) := by positivity\n        have h3 : (0 : \u211d) < (((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1) := by\n          apply mul_pos\n          \u00b7 push_cast\n            have h4 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n            have h5 : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n            positivity\n          \u00b7 push_cast\n            have h4 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n            have h5 : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n            linarith [hA0, h4, h5]\n        apply (inv_le_inv\u2080 h3 h2).mpr\n        push_cast\n        have h4 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg n\n        nlinarith [hA0, h4, hN0]\n      calc (\u2211' n : \u2115, ((((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9)\n          \u2264 \u2211' n : \u2115, (1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)) :=\n            tsum_le_tsum hterm h1 (hasSum_one_div_sub_telescope N hN1).summable\n        _ = 1 / (N : \u211d) := (hasSum_one_div_sub_telescope N hN1).tsum_eq\n    -- the kernel bound\n    have hN0R : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1\n    have hkernel_bound : (\u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9)\n        \u2264 (2 + Real.log (A + 1)) / A := by\n      rw [hsplit]\n      have h1 : (1 + Real.log (N : \u211d)) / A \u2264 (1 + Real.log (A + 1)) / A := by\n        apply div_le_div_of_nonneg_left _ hA0\n        have h2 : Real.log (N : \u211d) \u2264 Real.log (A + 1) := Real.log_le_log hN0R hNA1\n        linarith [h2]\n      have h2 : (1 : \u211d) / (N : \u211d) \u2264 1 / A := one_div_le_one_div_of_le hA0 hNA\n      linarith [h1, h2, hhead, htail]\n    -- the norm of the series\n    have hser : \u2016\u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016\n        \u2264 (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) := by\n      calc \u2016\u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016\n          \u2264 \u2211' n : \u2115, \u20161 / ((n : \u2102) + 1) - 1 / (w + n + 1)\u2016 :=\n            norm_tsum_le_tsum_norm hterm_summ\n        _ \u2264 \u2211' n : \u2115, \u2016w\u2016 / (((n : \u211d) + 1) * (A + (n : \u211d) + 1)) :=\n            tsum_le_tsum (fun n => norm_digamma_term_le hwre n) hterm_summ\n              (summable_digamma_majorant hwre)\n        _ = \u2016w\u2016 * \u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9 := by\n            rw [tsum_mul_left]\n            apply tsum_congr\n            intro n\n            rw [div_eq_mul_inv]\n        _ \u2264 \u2016w\u2016 * ((2 + Real.log (A + 1)) / A) :=\n            mul_le_mul_of_nonneg_left hkernel_bound (norm_nonneg _)\n        _ = (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) := by ring\n    -- the ratio \u2016w\u2016/A \u2264 3\n    have hratio : \u2016w\u2016 / A \u2264 3 := by\n      have h1 : \u2016w\u2016 \u2264 3 * A := by\n        have hnormsq : \u2016w\u2016 ^ 2 = w.re ^ 2 + w.im ^ 2 := by\n          rw [\u2190 Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n          ring\n        have him5 : w.im ^ 2 \u2264 25 := by\n          calc w.im ^ 2 = |w.im| ^ 2 := by rw [sq_abs]\n            _ \u2264 5 ^ 2 := pow_le_pow_left\u2080 (abs_nonneg _) hwim _\n            _ = 25 := by norm_num\n        have h2 : \u2016w\u2016 ^ 2 \u2264 (3 * A) ^ 2 := by\n          rw [hnormsq]\n          have hA2 : 2 \u2264 A := hwre\n          nlinarith [him5, hA2]\n        exact le_of_pow_le_pow_left\u2080 (two_ne_zero) (by positivity) h2\n      rw [div_le_iff\u2080 hA0]\n      linarith [h1]\n    have hlogA : Real.log (A + 1) \u2264 Real.log (\u2016w\u2016 + 1) := by\n      apply Real.log_le_log (by linarith [hA0])\n      have h1 : w.re \u2264 \u2016w\u2016 := by\n        have h2 := Complex.abs_re_le_norm w\n        rwa [abs_of_nonneg (by linarith [hwre])] at h2\n      linarith [h1]\n    -- the final assembly\n    have h\u03b31 : Real.eulerMascheroniConstant \u2264 1 :=\n      Real.eulerMascheroniConstant_lt_two_thirds.le.trans (by norm_num)\n    have h1w : \u2016(1 : \u2102) / w\u2016 \u2264 1 := by\n      rw [norm_div, norm_one]\n      rw [div_le_one (by linarith [hw_norm_ge] : (0 : \u211d) < \u2016w\u2016)]\n      exact hw_norm_ge\n    calc \u2016-(Real.eulerMascheroniConstant : \u2102) - 1 / w\n          + \u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016\n        \u2264 Real.eulerMascheroniConstant + \u2016(1 : \u2102) / w\u2016\n          + \u2016\u2211' n : \u2115, (1 / ((n : \u2102) + 1) - 1 / (w + n + 1))\u2016 := by\n          refine (norm_add_le _ _).trans ?_\n          refine add_le_add_right ?_ _\n          refine (norm_sub_le _ _).trans ?_\n          rw [norm_neg]\n          refine add_le_add_right ?_ _\n          rw [show (Real.eulerMascheroniConstant : \u2102)\n            = ((Real.eulerMascheroniConstant : \u211d) : \u2102) from rfl, Complex.norm_real,\n            Real.norm_eq_abs,\n            abs_of_nonneg (Real.one_half_lt_eulerMascheroniConstant.le.trans (by norm_num))]\n      _ \u2264 1 + 1 + (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) := by\n          gcongr\n          \u00b7 exact h\u03b31\n          \u00b7 exact h1w\n          \u00b7 exact hser\n      _ \u2264 20 * Real.log (2 + \u2016w\u2016) := by\n          have h2 : (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) \u2264 3 * (2 + Real.log (\u2016w\u2016 + 1)) := by\n            apply mul_le_mul hratio (by linarith [hlogA]) (by positivity) (by positivity)\n          have h3 : Real.log (\u2016w\u2016 + 1) \u2264 Real.log (2 + \u2016w\u2016) :=\n            Real.log_le_log (by positivity) (by linarith)\n          have hlognonneg : (0 : \u211d) \u2264 Real.log (2 + \u2016w\u2016) :=\n            Real.log_nonneg (by linarith [hw_norm_ge])\n          nlinarith [h2, h3, hlog4, hlognonneg]\n\n\nend NguyenRH1\n\nend\n",
  "structuredPatch": [
    {
      "oldStart": 317,
      "oldLines": 7,
      "newStart": 317,
      "newLines": 9,
      "lines": [
        "     have hsplit : (\u2211' n : \u2115, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9)",
        "         = \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9",
        "           + \u2211' n : \u2115, ((((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9) := by",
        "-      rw [\u2190 hker_summ.sum_add_tsum_nat_add N]",
        "+      have h := hker_summ.sum_add_tsum_nat_add N",
        "+      simp only [] at h",
        "+      rw [\u2190 h]",
        "     -- the head bound",
        "     have hhead : \u2211 n \u2208 Finset.range N, (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9",
        "         \u2264 (1 + Real.log (N : \u211d)) / A := by"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}