{
  "replace_all": false,
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean",
  "old_string": "end NguyenRH1\n\nend",
  "new_string": "/-! ## 4. The Jensen count -/\n\n/-- A nonzero constant factor does not change the analytic order. -/\ntheorem analyticOrderNatAt_const_mul {C : \u2102} (hC : C \u2260 0) {X : \u2102 \u2192 \u2102} {w\u2080 : \u2102}\n    (hX : AnalyticAt \u2102 X w\u2080) :\n    analyticOrderNatAt (fun w => C * X w) w\u2080 = analyticOrderNatAt X w\u2080 := by\n  have hord : analyticOrderAt (fun w => C * X w) w\u2080 = analyticOrderAt X w\u2080 := by\n    have h1 : analyticOrderAt ((fun _ : \u2102 => C) \u2022 X) w\u2080\n        = analyticOrderAt (fun _ : \u2102 => C) w\u2080 + analyticOrderAt X w\u2080 :=\n      analyticOrderAt_smul analyticAt_const hX\n    have h2 : analyticOrderAt (fun _ : \u2102 => C) w\u2080 = 0 :=\n      (analyticAt_const (\ud835\udd5c := \u2102) (v := C)).analyticOrderAt_eq_zero.mpr hC\n    have h3 : (fun w : \u2102 => C * X w) = (fun _ : \u2102 => C) \u2022 X :=\n      funext fun w => by simp [smul_eq_mul]\n    rw [h3, h1, h2]\n    simp\n  by_cases htop : analyticOrderAt X w\u2080 = \u22a4\n  \u00b7 rw [htop] at hord\n    have h4 : analyticOrderAt (fun w => C * X w) w\u2080 = \u22a4 := hord\n    rw [analyticOrderAt_eq_top] at htop h4  -- both sides junk 0: toNat \u22a4 = 0\n    rw [h4, htop]\n  \u00b7 have h1c := Nat.cast_analyticOrderNatAt (f := fun w => C * X w) (z\u2080 := w\u2080)\n      (by rw [hord]; exact htop)\n    have h2c := Nat.cast_analyticOrderNatAt (f := X) (z\u2080 := w\u2080) htop\n    have hcast : ((analyticOrderNatAt (fun w => C * X w) w\u2080 : \u2115) : \u2115\u221e)\n        = ((analyticOrderNatAt X w\u2080 : \u2115) : \u2115\u221e) := by\n      rw [h1c, h2c, hord]\n    exact Nat.cast_inj.mp hcast\n\n/-- The order of the scaled function at w\u2080 equals the order of \u03b6 at the\naffine image (for \u2016w\u2080\u2016 \u2264 1, |t| \u2265 10). -/\ntheorem analyticOrderNatAt_scaledZeta {t : \u211d} (ht : 10 \u2264 |t|) {w\u2080 : \u2102} (hw\u2080 : \u2016w\u2080\u2016 \u2264 1) :\n    analyticOrderNatAt (scaledZeta t) w\u2080\n      = analyticOrderNatAt riemannZeta (discCenter t + (5 / 2 : \u2102) * w\u2080) := by\n  have h\u03b60 : riemannZeta (discCenter t) \u2260 0 := by\n    have h := RvM.zeta_lower_bound_two t\n    intro h0\n    rw [\u2190 show discCenter t = 2 + t * Complex.I from rfl, h0, norm_zero] at h\n    norm_num at h\n  have haffine := analyticOrderNatAt_riemannZeta_affine ht hw\u2080\n  have haff_an : AnalyticAt \u2102 (fun w => riemannZeta (discCenter t + (5 / 2 : \u2102) * w)) w\u2080 := by\n    have hne : discCenter t + (5 / 2 : \u2102) * w\u2080 \u2260 1 := by\n      intro h\n      have hwim : |w\u2080.im| \u2264 1 := (abs_im_le_norm _).trans hw\u2080\n      have him : (discCenter t + (5 / 2 : \u2102) * w\u2080).im = t + (5 / 2) * w\u2080.im := by\n        simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]\n      have hbig : 15 / 2 \u2264 |t + (5 / 2) * w\u2080.im| := by\n        have h3 := abs_add_le (t + (5 / 2) * w\u2080.im) (-((5 / 2) * w\u2080.im))\n        rw [abs_neg, add_neg_cancel_right] at h3\n        have h4 : |(5 / 2) * w\u2080.im| \u2264 5 / 2 := by\n          rw [abs_mul, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5 / 2)]\n          calc (5 / 2) * |w\u2080.im| \u2264 (5 / 2) * 1 :=\n                mul_le_mul_of_nonneg_left hwim (by norm_num)\n            _ = 5 / 2 := by norm_num\n        linarith [h3, h4, ht]\n      rw [h] at him\n      rw [Complex.one_im] at him\n      rw [\u2190 him] at hbig\n      norm_num at hbig\n    have haff : AnalyticAt \u2102 (fun w : \u2102 => discCenter t + (5 / 2 : \u2102) * w) w\u2080 :=\n      analyticAt_const.add (analyticAt_const.mul analyticAt_id)\n    exact (analyticAt_riemannZeta_of_ne_one hne).comp_of_eq haff rfl\n  have hconst := analyticOrderNatAt_const_mul (inv_ne_zero h\u03b60) haff_an\n  -- scaledZeta t = fun w => (\u03b6(s\u2080))\u207b\u00b9 * \u03b6(aff w) pointwise\n  have hpoint : scaledZeta t = fun w => (riemannZeta (discCenter t))\u207b\u00b9 *\n      riemannZeta (discCenter t + (5 / 2 : \u2102) * w) :=\n    funext fun w => by unfold scaledZeta; rw [div_eq_mul_inv]\n  rw [hpoint, hconst]\n  exact haffine\n\n/-- **The Jensen count**: the mult-weighted count of zeros of the scaled\nfunction F in the closed ball of radius 24/25, via Zeta23's `ZerosBound`\napplied with B = (9/4)\u00b7|t|\u00b2. -/\ntheorem scaledZeta_jensen_count {t : \u211d} (ht : 10 \u2264 |t|) :\n    \u2211 \u03c1 \u2208 (finiteSetOfZeros_mono (f := scaledZeta t) (r := 24 / 25) (R := 99 / 100)\n      (by norm_num) (scaledZeta_zeros_finite)).toFinset,\n        analyticOrderNatAt (scaledZeta t) \u03c1\n      \u2264 Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32) := by\n  have hB : \u2200 z : \u2102, \u2016z\u2016 \u2264 99 / 100 \u2192 \u2016scaledZeta t z\u2016 \u2264 (9 / 4) * |t| ^ 2 := by\n    intro z hz\n    have hcenter : (1 / 3 : \u211d) \u2264 \u2016riemannZeta (discCenter t)\u2016 := by\n      have h := RvM.zeta_lower_bound_two t\n      rwa [\u2190 show discCenter t = 2 + t * Complex.I from rfl] at h\n    have htop : \u2016riemannZeta (discCenter t + (5 / 2 : \u2102) * z)\u2016 \u2264 (3 / 4) * |t| ^ 2 := by\n      apply norm_riemannZeta_le_disc ht\n      rw [Metric.mem_closedBall, Complex.dist_eq, add_sub_cancel_left]\n      calc \u2016(5 / 2 : \u2102) * z\u2016 \u2264 (5 / 2) * \u2016z\u2016 := by\n            rw [norm_mul]\n            have hn : \u2016(5 / 2 : \u2102)\u2016 = 5 / 2 := by\n              rw [show (5 / 2 : \u2102) = ((5 / 2 : \u211d) : \u2102) by norm_num, Complex.norm_real,\n                Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5 / 2)]\n            rw [hn]\n        _ \u2264 (5 / 2) * (99 / 100) := mul_le_mul_of_nonneg_left hz (by norm_num)\n        _ \u2264 5 / 2 := by norm_num\n    unfold scaledZeta\n    rw [norm_div]\n    calc \u2016riemannZeta (discCenter t + (5 / 2 : \u2102) * z)\u2016 / \u2016riemannZeta (discCenter t)\u2016\n        \u2264 ((3 / 4) * |t| ^ 2) / (1 / 3) := by\n          apply div_le_div htop _ (by norm_num) hcenter\n          \u00b7 norm_num\n      _ = (9 / 4) * |t| ^ 2 := by ring\n  have h := ZerosBound (f := scaledZeta t) (r := 24 / 25) (R := 99 / 100)\n    (by norm_num) (by norm_num) (by norm_num) (by norm_num)\n    (scaledZeta_analytic ht) (scaledZeta_zero t) scaledZeta_zeros_finite hB\n  refine h.trans ?_\n  rw [one_div, inv_mul_eq_div]\n  apply div_le_div_of_nonneg_right _ ... \n  sorry\n\nend NguyenRH1\n\nend"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean",
  "oldString": "            tsum_le_tsum hterm h1 (hasSum_one_div_sub_telescope N hN1).summable",
  "newString": "            Summable.tsum_le_tsum hterm h1 (hasSum_one_div_sub_telescope N hN1).summable",
  "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 h1log4 : Real.log 4 \u2264 Real.log (2 + \u2016w\u2016) :=\n    Real.log_le_log (by norm_num) (by linarith [hw_norm_ge])\n  have hlog4gt : (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  have hlog4 : (5 : \u211d) / 3 \u2264 19 * Real.log (2 + \u2016w\u2016) := by nlinarith [h1log4, hlog4gt]\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\u211a : (0 : \u211a) \u2264 harmonic (n - 1) :=\n        Finset.sum_nonneg (fun i _ => by positivity)\n      have hH0 : (0 : \u211d) \u2264 ((harmonic (n - 1) : \u211a) : \u211d) := by exact_mod_cast hH0\u211a\n      have hcast2 : ((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 hHbound : ((harmonic (n - 1) : \u211a) : \u211d) \u2264 1 + Real.log ((n : \u211d) - 1) := by\n        have h := harmonic_le_one_add_log (n - 1)\n        rw [hcast2] at h\n        exact h\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        linarith [h1, hcast2]\n      apply abs_le.mpr\n      constructor <;> linarith [h\u03b30, hH0, hHbound, 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    rw [hwn] at hlogn1 h1log4\n    have hlogbig : (2 : \u211d) \u2264 19 * Real.log (2 + \u2016(n : \u2102)\u2016) := by nlinarith [h1log4, hlog4gt]\n    linarith [hreal, h\u03b31, hlogn1, hlogbig]\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, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N) := by\n      exact (hker_summ.sum_add_tsum_nat_add N).symm\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, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N))\n        \u2264 1 / (N : \u211d) := by\n      have h1 : Summable (fun n : \u2115 => (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9)\n          (n + N)) :=\n        (summable_nat_add_iff N).mpr hker_summ\n      have hterm : \u2200 n : \u2115, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N)\n          \u2264 1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1) := by\n        intro n\n        show ((((n + N : \u2115) : \u211d) + 1) * (A + ((n + N : \u2115) : \u211d) + 1))\u207b\u00b9\n          \u2264 1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)\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 : ((n : \u211d) + N) * ((n : \u211d) + N + 1) \u2260 0)]\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, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N))\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": 381,
      "oldLines": 7,
      "newStart": 381,
      "newLines": 7,
      "lines": [
        "         nlinarith [hA0, h4, hN0]",
        "       calc (\u2211' n : \u2115, (fun m : \u2115 => (((m : \u211d) + 1) * (A + (m : \u211d) + 1))\u207b\u00b9) (n + N))",
        "           \u2264 \u2211' n : \u2115, (1 / ((n : \u211d) + N) - 1 / ((n : \u211d) + N + 1)) :=",
        "-            tsum_le_tsum hterm h1 (hasSum_one_div_sub_telescope N hN1).summable",
        "+            Summable.tsum_le_tsum hterm h1 (hasSum_one_div_sub_telescope N hN1).summable",
        "         _ = 1 / (N : \u211d) := (hasSum_one_div_sub_telescope N hN1).tsum_eq",
        "     -- the kernel bound",
        "     have hN0R : (0 : \u211d) < (N : \u211d) := by exact_mod_cast hN1"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}