{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
  "old_string": "/-- The cast bridge: DinfC(\u2191x) = \u2191(DinfR x) for 0 < x. -/\nlemma DinfC_ofReal {x : \u211d} (hx : 0 < x) : DinfC (\u2191x) = \u2191(DinfR x) := by",
  "new_string": "/-- The cast bridge: DinfC(\u2191x) = \u2191(DinfR x) for 0 < x. -/\nlemma DinfC_ofReal {x : \u211d} (_hx : 0 < x) : DinfC (\u2191x) = \u2191(DinfR x) := by"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
  "oldString": "    unfold HIntegral\n    rw [\u2190 intervalIntegral_conj]\n    apply intervalIntegral.integral_congr",
  "newString": "    unfold HIntegral\n    rw [\u2190 RCLike.intervalIntegral_conj]\n    apply intervalIntegral.integral_congr",
  "originalFile": "/-\nNguyenRH1/LiDogLeg.lean \u2014 ii\u2032-6-DL-1 (D-074, session 040): the zero-free\ndog-leg deformation of the Lagarias horizontal right tail.\n\nTHE CONTENT (D-074 \u00a73.1\u20133.2): on the dog-leg rectangle [3, X_R]\u00d7[T, U]\n(T > 0), the Lagarias integrand Jlag n s = (s/(s\u22121))\u207f\u22121 \u00b7 (\u2212\u03b6\u2032/\u03b6(s)) is\nholomorphic UNCONDITIONALLY (s \u2260 1 since im > 0; \u03b6 s \u2260 0 for re s \u2265 3 > 1\nby Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`\n\u2014 NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem\n(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation\nidentity\n  H(3\u2192X_R, T) = H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U)\n(the upper right tail = the high horizontal \u2212 the right drop + the left\nlift), plus the Jlag conjugation identity for the lower-side transfer.\n\nThis is the repair of Finding F-D (D-072): the broken low-path envelope\nis ABANDONED (not bounded) \u2014 the magnitude bound comes later from the\nthree dog-leg pieces, all in the unconditionally zero-free region.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiBasePoints\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Dog-leg analyticity (D-074 \u00a73.1; no perimeter) -/\n\n/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/\ndef dogZ (T : \u211d) : \u2102 := ((3 : \u211d) : \u2102) + (T : \u211d) * Complex.I\ndef dogW (XR U : \u211d) : \u2102 := ((XR : \u211d) : \u2102) + (U : \u211d) * Complex.I\n\nlemma dogZ_re (T : \u211d) : (dogZ T).re = 3 := by simp [dogZ]\nlemma dogZ_im (T : \u211d) : (dogZ T).im = T := by simp [dogZ]\nlemma dogW_re (XR U : \u211d) : (dogW XR U).re = XR := by simp [dogW]\nlemma dogW_im (XR U : \u211d) : (dogW XR U).im = U := by simp [dogW]\n\n/-- Jlag is differentiable at every point with 3 \u2264 re, 0 < im:\n\u03b6 is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,\nUNCONDITIONAL \u2014 the Euler-product region) and s \u2260 1 (im \u2260 0).\nNO perimeter hypothesis. -/\ntheorem Jlag_differentiableAt_dogleg {n : \u2115} {s : \u2102}\n    (hre : 3 \u2264 s.re) (him : 0 < s.im) :\n    DifferentiableAt \u2102 (Jlag n) s := by\n  apply Jlag_differentiableAt\n  \u00b7 rintro rfl\n    simp at him\n  \u00b7 exact riemannZeta_ne_zero_of_one_lt_re (by linarith)\n\n/-- Jlag is holomorphic on the whole dog-leg rectangle\n[3, X_R]\u00d7[T, U] (T > 0). -/\ntheorem holomorphicOn_Jlag_dogleg {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by\n  intro s hs\n  rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs\n  rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs\n  exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt\n\n/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is\nunconditionally zero-free \u2014 the residue sum is EMPTY, no perimeter). -/\ntheorem rectangleIntegral_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=\n  (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl\n\n/-- The (2\u03c0i)\u207b\u00b9-normalized form (API symmetry with rectInt'_Jlag). -/\ntheorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by\n  rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,\n    smul_zero]\n\n/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 \u00a73.2 (\u2605), the\ncapstone for ii\u2032-6-c): the low right-horizontal equals the high\nhorizontal minus the right drop plus the left lift. Orientations: all\nH-integrals left-to-right, all V-integrals upward (the main contour's\ntop side is their reversal, handled at the fold site). -/\ntheorem upper_right_horizontal_eq_dogleg {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    HIntegral (Jlag n) 3 XR T =\n      HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +\n        VIntegral (Jlag n) 3 T U := by\n  have h0 := rectangleIntegral_Jlag_dogleg_eq_zero (n := n) hT hTU hXR\n  unfold RectangleIntegral at h0\n  rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0\n  linear_combination h0\n\n/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/\n\n/-- kFun is conjugation-symmetric (real-coefficient rational function). -/\ntheorem kFun_conj (n : \u2115) (s : \u2102) :\n    kFun n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (kFun n s) := by\n  unfold kFun\n  simp [map_sub, map_pow, map_one]\n\n/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +\n`iteratedDeriv_riemannZeta_conj`): Jlag n (s\u0304) = conj (Jlag n s).\nNeeded for the lower-horizontal transfer (DL-5). -/\ntheorem Jlag_conj (n : \u2115) {s : \u2102} (hs : s \u2260 1) :\n    Jlag n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (Jlag n s) := by\n  have h1 : deriv riemannZeta ((starRingEnd \u2102) s) =\n      (starRingEnd \u2102) (deriv riemannZeta s) := by\n    have h := iteratedDeriv_riemannZeta_conj 1 hs\n    rwa [iteratedDeriv_one] at h\n  unfold Jlag\n  rw [kFun_conj, _root_.riemannZeta_conj, h1]\n  simp only [map_mul, map_neg, map_div\u2080]\n\n/-! ## 3. The left-lift bound (DL-2, D-074 \u00a73.3 V_left) -/\n\n/-- **Kernel on the lift**: \u2016kFun n (3+it)\u2016 \u2264 e^{5/2}+1 for n \u2264 t\u00b2\n(D-074 \u00a76: |(3+it)/(2+it)|\u00b2 = (9+t\u00b2)/(4+t\u00b2) = 1 + 5/(4+t\u00b2), whose n-th\npower is \u2264 e^{5n/(2(4+t\u00b2))} \u2264 e^{5/2}). -/\ntheorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : \u2115} {t : \u211d}\n    (hT : (n : \u211d) \u2264 t ^ 2) :\n    \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp (5 / 2) + 1 := by\n  rcases Nat.eq_zero_or_pos n with hn | hn\n  \u00b7 subst hn\n    simp only [kFun, pow_zero, sub_self, norm_zero]\n    positivity\n  \u00b7 have hnR : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n    have ht2 : (0 : \u211d) < 4 + t ^ 2 := by positivity\n    have hn4t2 : (n : \u211d) \u2264 4 + t ^ 2 := by linarith [hT]\n    have hQpos : (0 : \u211d) \u2264 (9 + t ^ 2) / (4 + t ^ 2) := by positivity\n    have hQle : (9 + t ^ 2) / (4 + t ^ 2) \u2264 Real.exp (5 / (n : \u211d)) := by\n      have h1 : (9 + t ^ 2) / (4 + t ^ 2) = 1 + 5 / (4 + t ^ 2) := by\n        field_simp [ht2.ne']\n        ring\n      rw [h1]\n      have h2 : 5 / (4 + t ^ 2) \u2264 5 / (n : \u211d) :=\n        (div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)).mpr hn4t2\n      have h3 := Real.add_one_le_exp (5 / (n : \u211d))\n      linarith\n    have hQn : ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 Real.exp 5 := by\n      calc ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 (Real.exp (5 / (n : \u211d))) ^ n :=\n            pow_le_pow_left\u2080 hQpos hQle n\n        _ = Real.exp 5 := by\n            rw [\u2190 Real.exp_nat_mul]\n            congr 1\n            have hn0 : (n : \u211d) \u2260 0 := by exact_mod_cast hn.ne'\n            field_simp [hn0]\n    have hns3 : Complex.normSq ((3 : \u211d) + t * Complex.I) = 9 + t ^ 2 := by\n      simp [Complex.normSq_apply]\n      ring\n    have hns2 : Complex.normSq ((2 : \u211d) + t * Complex.I) = 4 + t ^ 2 := by\n      simp [Complex.normSq_apply]\n      ring\n    have hnormA : \u2016((3 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (9 + t ^ 2) := by\n      have h1 : \u2016((3 : \u211d) + t * Complex.I)\u2016 =\n          Real.sqrt (Complex.normSq ((3 : \u211d) + t * Complex.I)) := by\n        rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n      rw [h1, hns3]\n    have hnormB : \u2016((2 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (4 + t ^ 2) := by\n      have h1 : \u2016((2 : \u211d) + t * Complex.I)\u2016 =\n          Real.sqrt (Complex.normSq ((2 : \u211d) + t * Complex.I)) := by\n        rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n      rw [h1, hns2]\n    have hnorm : \u2016((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)\u2016 =\n        Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by\n      rw [norm_div, hnormA, hnormB,\n        \u2190 Real.sqrt_div (by positivity : (0 : \u211d) \u2264 9 + t ^ 2)]\n    have hs1 : ((3 : \u211d) + t * Complex.I) - 1 = (2 : \u211d) + t * Complex.I := by\n      push_cast\n      ring\n    unfold kFun\n    rw [hs1]\n    calc \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n - 1\u2016\n        \u2264 \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n          norm_sub_le _ _\n      _ = (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n + 1 := by\n          rw [norm_pow, hnorm, norm_one]\n      _ \u2264 Real.exp (5 / 2) + 1 := by\n          have h4 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n \u2264 Real.exp (5 / 2) := by\n            have hx0 : (0 : \u211d) \u2264 Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) :=\n              Real.sqrt_nonneg _\n            have hx : (0 : \u211d) \u2264 (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n :=\n              pow_nonneg hx0 n\n            have h5 : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 \u2264 Real.exp 5 := by\n              have e : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 =\n                  ((9 + t ^ 2) / (4 + t ^ 2)) ^ n := by\n                rw [\u2190 pow_mul, mul_comm n 2, pow_mul, Real.sq_sqrt hQpos]\n              rw [e]\n              exact hQn\n            have h8 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n =\n                Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2) := by\n              rw [Real.sqrt_sq hx]\n            rw [h8]\n            calc Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2)\n                \u2264 Real.sqrt (Real.exp 5) := Real.sqrt_le_sqrt h5\n              _ = Real.exp (5 / 2) := (Real.exp_half 5).symm\n          linarith [h4]\n\n/-- The Dirichlet majorant at s = 3 (summable since 3 > 1). -/\ndef dirichletC3 : \u211d :=\n  \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016\n\n/-- Termwise 3-vs-2 comparison for the \u039b L-series: \u039b(n)/n\u00b3 \u2264 (1/2)\u00b7\u039b(n)/n\u00b2. -/\nlemma norm_term_vonMangoldt_three_le_half (n : \u2115) :\n    \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 \u2264\n      (1 / 2) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 := by\n  have h3re : ((3 : \u2102).re) = 3 := rfl\n  have h2re : ((2 : \u2102).re) = 2 := rfl\n  simp only [LSeries.norm_term_eq, h3re, h2re]\n  split\n  \u00b7 norm_num\n  \u00b7 next hn =>\n    rcases eq_or_ne n 1 with rfl | hn1\n    \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n    \u00b7 have hn2 : 2 \u2264 n := by omega\n      have h\u039b : \u2016(ArithmeticFunction.vonMangoldt n : \u2102)\u2016 =\n          ArithmeticFunction.vonMangoldt n :=\n        Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n      rw [h\u039b]\n      have e : ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d) =\n          (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := by\n        rw [show (3 : \u211d) = 2 + 1 by norm_num,\n          Real.rpow_add (by positivity : (0 : \u211d) < (n : \u211d)), Real.rpow_one]\n        field_simp [show (n : \u211d) \u2260 0 by positivity]\n      have h12 : (1 : \u211d) / (n : \u211d) \u2264 1 / 2 :=\n        one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 2)\n          (by exact_mod_cast hn2 : (2 : \u211d) \u2264 (n : \u211d))\n      have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d) :=\n        div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n          (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (n : \u211d)) _)\n      calc ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d)\n          = (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := e\n        _ \u2264 (1 / 2) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) :=\n            mul_le_mul_of_nonneg_right h12 hpos\n\n/-- dirichletC3 \u2264 1/2 (the termwise comparison + dirichletC2 \u2264 1) \u2014\nthe certified C_zeta3 = 0.5 of D-074 \u00a74. (A tighter 0.17 build is\npossible via a 6-prime partial sum + antitone-integral tail; the fold\nis indifferent to the constant, so the cheap certified 0.5 is charged.) -/\nlemma dirichletC3_le_half : dirichletC3 \u2264 1 / 2 := by\n  have hsum3 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsum2 : 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  calc dirichletC3\n      = \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 := rfl\n    _ \u2264 \u2211' n : \u2115, (1 / 2) *\n          \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n        Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3\n          (hsum2.mul_left (1 / 2))\n    _ = (1 / 2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n    _ \u2264 1 / 2 := by linarith [dirichletC2_le_one]\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 dirichletC3 for re s \u2265 3 (the s = 3 clone of the\nDirichlet-series majorant). -/\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : \u2102} (hs : 3 \u2264 s.re) :\n    \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC3 := by\n  have hs1 : (1 : \u211d) < s.re := by linarith\n  have h1 : -logDeriv riemannZeta s\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsum3 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsumS : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n      \u2264 dirichletC3 := by\n    show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n    calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n        \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n          norm_tsum_le_tsum_norm hsumS\n      _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 :=\n          Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n            simp\n            exact hs) n) hsumS hsum3\n      _ = dirichletC3 := rfl\n  calc \u2016logDeriv riemannZeta s\u2016\n      = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n        rw [\u2190 h1, norm_neg]\n    _ \u2264 dirichletC3 := hle\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 1/2 for re s \u2265 3 (the charged C_zeta3 = 0.5). -/\nlemma norm_logDeriv_zeta_le_half {s : \u2102} (hs : 3 \u2264 s.re) :\n    \u2016logDeriv riemannZeta s\u2016 \u2264 1 / 2 :=\n  (norm_logDeriv_zeta_le_dirichletC3 hs).trans dirichletC3_le_half\n\n/-- **The left-lift bound** (D-074 \u00a73.3 V_left): for 0 < T \u2264 U and\nn \u2264 T\u00b2, \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U \u2212 T)\u00b7(e^{5/2}+1)/2. The kernel\n\u2264 e^{5/2}+1 (the 1+5/(4+t\u00b2) computation), the zeta factor \u2264 1/2\n(certified, no perimeter). -/\ntheorem vIntegral_Jlag_three_norm_le {n : \u2115} {T U : \u211d}\n    (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n    \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n  have hnorm : \u2016VIntegral (Jlag n) 3 T U\u2016 =\n      \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 := by\n    unfold VIntegral\n    rw [norm_smul, Complex.norm_I, one_mul]\n  rw [hnorm]\n  have hbound : \u2200 t \u2208 Set.Ioc T U,\n      \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 (Real.exp (5 / 2) + 1) * (1 / 2) := by\n    intro t ht\n    have htT : T < t := ht.1\n    have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n    have hre : (3 : \u211d) \u2264 ((3 : \u211d) + t * Complex.I).re := by simp\n    have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2\n    have h2 := norm_logDeriv_zeta_le_half (s := (3 : \u211d) + t * Complex.I) hre\n    have hnorm3 : \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 =\n        \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 *\n          \u2016logDeriv riemannZeta ((3 : \u211d) + t * Complex.I)\u2016 := by\n      show \u2016kFun n ((3 : \u211d) + t * Complex.I) *\n          (-logDeriv riemannZeta ((3 : \u211d) + t * Complex.I))\u2016 = _\n      rw [norm_mul, norm_neg]\n    rw [hnorm3]\n    exact mul_le_mul h1 h2 (norm_nonneg _) (by positivity)\n  have hint : \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264\n      ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by\n    apply intervalIntegral.norm_integral_le_of_norm_le_const\n    intro t ht\n    rw [Set.uIoc_of_le hTU] at ht\n    exact hbound t ht\n  have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n  rw [habs] at hint\n  calc \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016\n      \u2264 ((Real.exp (5 / 2) + 1) * (1 / 2)) * (U - T) := hint\n    _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring\n\n/-! ## 4. The high-horizontal stepping (DL-3, D-074 \u00a77 + D-073 \u00a74) -/\n\n/-- Termwise \u03c3-vs-2 comparison for the \u039b L-series (the (6.10) halving):\n\u039b(m)/m^\u03c3 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7\u039b(m)/m\u00b2 for \u03c3 \u2265 2. -/\nlemma norm_term_vonMangoldt_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) (m : \u2115) :\n    \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n        ((\u03c3 : \u211d) + t * Complex.I) m\u2016 \u2264\n      (2 : \u211d) ^ (-(\u03c3 - 2)) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by\n  have h\u03c3re : ((\u03c3 : \u211d) + t * Complex.I).re = \u03c3 := by simp\n  have h2re : ((2 : \u2102).re) = 2 := rfl\n  simp only [LSeries.norm_term_eq, h\u03c3re, h2re]\n  split\n  \u00b7 norm_num\n  \u00b7 next hm =>\n    have h\u039b : \u2016(ArithmeticFunction.vonMangoldt m : \u2102)\u2016 =\n        ArithmeticFunction.vonMangoldt m :=\n      Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n    rw [h\u039b]\n    rcases eq_or_ne m 1 with rfl | hm1\n    \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n    \u00b7 have hm2 : 2 \u2264 m := by omega\n      have e : ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ \u03c3 =\n          (1 / (m : \u211d) ^ (\u03c3 - 2)) * (ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d)) := by\n        rw [show (\u03c3 : \u211d) = (\u03c3 - 2) + 2 by ring,\n          Real.rpow_add (by positivity : (0 : \u211d) < (m : \u211d))]\n        field_simp [show (m : \u211d) \u2260 0 by positivity]\n        ring_nf\n      rw [e]\n      have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n        rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2), \u2190 one_div]\n        apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n        exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n          (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)\n      have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d) :=\n        div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n          (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (m : \u211d)) _)\n      exact mul_le_mul_of_nonneg_right hle hpos\n\n/-- \u2016\u03b6\u2032/\u03b6(\u03c3+it)\u2016 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7dirichletC2 for \u03c3 \u2265 2 (the (6.10)\nhalving in LSeries form; dirichletC2 \u2264 1 makes the tail free). -/\nlemma norm_logDeriv_zeta_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) :\n    \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n      (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n  have hs1 : (1 : \u211d) < ((\u03c3 : \u211d) + t * Complex.I).re := by simp; linarith\n  have h1 : -logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) ((\u03c3 : \u211d) + t * Complex.I) := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsum2 : 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  have hsumS : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n        ((\u03c3 : \u211d) + t * Complex.I) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n      ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n    show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n      ((\u03c3 : \u211d) + t * Complex.I) n\u2016 \u2264 _\n    calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n          ((\u03c3 : \u211d) + t * Complex.I) n\u2016\n        \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n            ((\u03c3 : \u211d) + t * Complex.I) n\u2016 :=\n          norm_tsum_le_tsum_norm hsumS\n      _ \u2264 \u2211' n : \u2115, (2 : \u211d) ^ (-(\u03c3 - 2)) *\n            \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n          Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_le_two_pow h\u03c3 n) hsumS\n            (hsum2.mul_left _)\n      _ = (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n  calc \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016\n      = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n          ((\u03c3 : \u211d) + t * Complex.I)\u2016 := by\n        rw [\u2190 h1, norm_neg]\n    _ \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := hle\n\n/-- **Kernel envelope** (D-074 \u00a77, the single-exponential form that\nreplaces the unit-step geometric series): \u2016(1+1/((\u03c3\u22121)+iU))\u207f\u2016 \u2264\ne^{(4/9)\u03c3} for \u03c3 \u2265 3 and n \u2264 (4/9)U\u00b2. From the (6.11) core\n\u20161+1/s\u2016 \u2264 1+(re s+1)/normSq s \u2264 1+\u03c3/U\u00b2. -/\ntheorem one_add_div_pow_norm_le_exp_four_ninths {n : \u2115} {\u03c3 U : \u211d}\n    (h\u03c3 : 3 \u2264 \u03c3) (hU : 0 < U) (hnU : (n : \u211d) \u2264 (4 / 9) * U ^ 2) :\n    \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 Real.exp ((4 / 9) * \u03c3) := by\n  have hs0 : (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2260 0 := by\n    intro h\n    have him : (((\u03c3 : \u211d) - 1) + U * Complex.I).im = 0 := by rw [h]; simp\n    simp at him\n    linarith\n  have hle := norm_one_add_one_div_le hs0\n  have hre : (((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1 = \u03c3 := by\n    simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n      Complex.sub_re, Complex.one_re]\n  have hns : Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) = (\u03c3 - 1) ^ 2 + U ^ 2 := by\n    simp [Complex.normSq_apply]\n    ring\n  have hstep : ((((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1) /\n      Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2264 \u03c3 / U ^ 2 := by\n    rw [hre, hns]\n    have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n    have h1 : (0 : \u211d) \u2264 (\u03c3 - 1) ^ 2 := sq_nonneg _\n    exact (div_le_div_iff_of_pos_left (by linarith : (0 : \u211d) < \u03c3)\n      (by positivity) hU2).mpr (by linarith [h1])\n  have hstep1 : 1 + ((((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1) /\n      Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2264 1 + \u03c3 / U ^ 2 := by\n    linarith [hstep]\n  have hpow1 : \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 (1 + \u03c3 / U ^ 2) ^ n :=\n    pow_le_pow_left\u2080 (norm_nonneg _) (hle.trans hstep1) n\n  have hpow2 : (1 + \u03c3 / U ^ 2) ^ n \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := by\n    calc (1 + \u03c3 / U ^ 2) ^ n \u2264 (Real.exp (\u03c3 / U ^ 2)) ^ n := by\n          have h := Real.add_one_le_exp (\u03c3 / U ^ 2)\n          exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n      _ = Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := (Real.exp_nat_mul (\u03c3 / U ^ 2) n).symm\n  have hexp : (n : \u211d) * (\u03c3 / U ^ 2) \u2264 (4 / 9) * \u03c3 := by\n    have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n    have h\u03c30 : (0 : \u211d) < \u03c3 := by linarith\n    have h1 : (n : \u211d) / U ^ 2 \u2264 4 / 9 := by\n      have h2 := div_le_div_of_nonneg_right hnU hU2.le\n      rwa [mul_div_cancel_right\u2080 _ hU2.ne'] at h2\n    rw [show (n : \u211d) * (\u03c3 / U ^ 2) = ((n : \u211d) / U ^ 2) * \u03c3 by ring]\n    exact mul_le_mul_of_nonneg_right h1 h\u03c30.le\n  calc \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n\n      \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := hpow1.trans hpow2\n    _ \u2264 Real.exp ((4 / 9) * \u03c3) := Real.exp_le_exp.mpr hexp\n\n/-! ## 5. The product envelope and the integral assembly (DL-3c/d) -/\n\n/-- **The product envelope** (D-074 \u00a77): for \u03c3 \u2265 3, 0 < t, n \u2264 (4/9)t\u00b2,\n\u2016Jlag n (\u03c3+it)\u2016 \u2264 (4\u00b7e^{\u2212c\u03c3} + 4\u00b72^{\u2212\u03c3})\u00b7dirichletC2, c = log 2 \u2212 4/9.\nThe kernel envelope (e^{(4/9)\u03c3}) times the zeta halving (2^{\u2212(\u03c3\u22122)})\ncollapses to the single exponential 4\u00b7e^{\u2212c\u03c3}: no geometric series. -/\ntheorem Jlag_dogleg_norm_le_envelope {n : \u2115} {\u03c3 t : \u211d}\n    (h\u03c3 : 3 \u2264 \u03c3) (ht : 0 < t) (hnU : (n : \u211d) \u2264 (4 / 9) * t ^ 2) :\n    \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n      dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := by\n  have hw1 : ((\u03c3 : \u211d) + t * Complex.I) - 1 = ((\u03c3 : \u211d) - 1) + t * Complex.I := by\n    ring\n  have hs1ne : (((\u03c3 : \u211d) - 1) + t * Complex.I) \u2260 0 := by\n    intro h\n    have him : (((\u03c3 : \u211d) - 1) + t * Complex.I).im = 0 := by rw [h]; simp\n    simp at him\n    linarith\n  have hwid : ((\u03c3 : \u211d) + t * Complex.I) / (((\u03c3 : \u211d) + t * Complex.I) - 1) =\n      1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I) := by\n    rw [hw1]\n    field_simp [hs1ne]\n    ring\n  have hker := one_add_div_pow_norm_le_exp_four_ninths h\u03c3 ht hnU\n  have hzeta := norm_logDeriv_zeta_le_two_pow (show (2 : \u211d) \u2264 \u03c3 by linarith) (t := t)\n  have hk : \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp ((4 / 9) * \u03c3) + 1 := by\n    unfold kFun\n    rw [hwid]\n    calc \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I)) ^ n - 1\u2016\n        \u2264 \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 := norm_sub_le _ _\n      _ = \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I))\u2016 ^ n + 1 := by rw [norm_pow, norm_one]\n      _ \u2264 Real.exp ((4 / 9) * \u03c3) + 1 := by linarith [hker]\n  have hprod : \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n      (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2) := by\n    have hn3 : \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 =\n        \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I)\u2016 *\n          \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016 := by\n      show \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I) *\n          (-logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I))\u2016 = _\n      rw [norm_mul, norm_neg]\n    rw [hn3]\n    exact mul_le_mul hk hzeta (norm_nonneg _)\n      (add_nonneg (Real.exp_nonneg _) (by norm_num))\n  have h2b : (2 : \u211d) ^ (-\u03c3) = Real.exp (-(Real.log 2) * \u03c3) := by\n    rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n    congr 1\n    ring\n  have h22 : (2 : \u211d) ^ (2 : \u211d) = 4 := by\n    rw [Real.rpow_two]\n    norm_num\n  have h2a : (2 : \u211d) ^ (-(\u03c3 - 2)) = 4 * (2 : \u211d) ^ (-\u03c3) := by\n    rw [show (-(\u03c3 - 2)) = -\u03c3 + 2 by ring, Real.rpow_add (by norm_num : (0 : \u211d) < 2), h2b, h22]\n    ring\n  have hexp_alg : Real.exp ((4 / 9) * \u03c3) * Real.exp (-(Real.log 2) * \u03c3) =\n      Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) := by\n    rw [\u2190 Real.exp_add]\n    congr 1\n    ring\n  have halg : (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2))) =\n      4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3) := by\n    rw [h2a, h2b]\n    calc (Real.exp ((4 / 9) * \u03c3) + 1) * (4 * Real.exp (-(Real.log 2) * \u03c3))\n        = 4 * (Real.exp ((4 / 9) * \u03c3) * Real.exp (-(Real.log 2) * \u03c3)) +\n          4 * Real.exp (-(Real.log 2) * \u03c3) := by ring\n      _ = 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * Real.exp (-(Real.log 2) * \u03c3) := by\n        rw [hexp_alg]\n  calc \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016\n      \u2264 (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2) := hprod\n    _ = dirichletC2 * ((Real.exp ((4 / 9) * \u03c3) + 1) * (2 : \u211d) ^ (-(\u03c3 - 2))) := by ring\n    _ = dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := by\n        rw [halg]\n\n/-- The FTC-bound \u222b\u2083^XR e^{\u2212c\u03c3}d\u03c3 \u2264 e^{\u22123c}/c for c > 0. -/\nlemma integral_exp_neg_le {c XR : \u211d} (hc : 0 < c) (_hXR : 3 \u2264 XR) :\n    \u222b \u03c3 in (3 : \u211d)..XR, Real.exp (-c * \u03c3) \u2264 Real.exp (-3 * c) / c := by\n  have hF : \u2200 x \u2208 Set.uIcc (3 : \u211d) XR,\n      HasDerivAt (fun \u03c3 => -Real.exp (-c * \u03c3) / c) (Real.exp (-c * x)) x := by\n    intro x hx\n    have h2 : HasDerivAt (fun \u03c3 => Real.exp (-c * \u03c3)) (Real.exp (-c * x) * (-c)) x := by\n      have h := ((hasDerivAt_id' x).const_mul (-c)).exp\n      rwa [mul_one] at h\n    have h3 := h2.const_mul (-1 / c)\n    rw [show (-1 / c) * (Real.exp (-c * x) * (-c)) = Real.exp (-c * x) by\n      field_simp [hc.ne']] at h3\n    have h5 : (fun \u03c3 => (-1 / c) * Real.exp (-c * \u03c3)) =\n        (fun \u03c3 => -Real.exp (-c * \u03c3) / c) := by\n      funext \u03c3\n      field_simp [hc.ne']\n    rw [h5] at h3\n    exact h3\n  have hint : IntervalIntegrable (fun \u03c3 => Real.exp (-c * \u03c3)) MeasureTheory.volume 3 XR := by\n    apply ContinuousOn.intervalIntegrable\n    exact (Real.continuous_exp.comp (continuous_const.mul continuous_id)).continuousOn\n  have e : Real.exp (-c * 3) = Real.exp (-3 * c) := by\n    congr 1\n    ring\n  rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF hint, e]\n  have h1 : (0 : \u211d) \u2264 Real.exp (-c * XR) := (Real.exp_pos _).le\n  have h2 : (0 : \u211d) < c := hc\n  rw [show -Real.exp (-c * XR) / c - -Real.exp (-3 * c) / c =\n      (Real.exp (-3 * c) - Real.exp (-c * XR)) / c by\n    field_simp [h2.ne']\n    ring]\n  rw [show Real.exp (-3 * c) / c = (Real.exp (-3 * c) - (0 : \u211d)) / c by ring]\n  exact div_le_div_of_nonneg_right (by linarith [h1]) h2.le\n\n/-- The certified exponent-decay constant c = log 2 \u2212 4/9 \u2265 0.2487. -/\nlemma cdog_gt : (0.2487 : \u211d) \u2264 Real.log 2 - 4 / 9 := by\n  have h := Real.log_two_gt_d9\n  norm_num at h\n  linarith\n\n/-- The certified e^{4/3} \u2264 3.8073 (the (1\u2212x/16)\u207b\u00b9\u2076 route + d9 e). -/\nlemma exp_four_thirds_le : Real.exp (4 / 3) \u2264 (3.8073 : \u211d) := by\n  have he13 : Real.exp (1 / 3) \u2264 (1.4006 : \u211d) :=\n    le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n  rw [show (4 / 3 : \u211d) = 1 + 1 / 3 by norm_num, Real.exp_add]\n  calc Real.exp 1 * Real.exp (1 / 3) \u2264 2.7182818286 * 1.4006 :=\n        mul_le_mul Real.exp_one_lt_d9.le he13 (Real.exp_pos _).le (by norm_num)\n    _ \u2264 3.8073 := by norm_num\n\n/-- **THE HIGH-HORIZONTAL BOUND** (D-074 \u00a77 capstone; D-073 Cor 4.2's\nR(1.5) in single-exponential-envelope form): for 0 < U, n \u2264 (4/9)U\u00b2\n(i.e. U \u2265 (3/2)\u221an) and 3 \u2264 XR, \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264 8.38\n(charged; the true value \u2264 1.2 at n = 10\u2075, E-034 V5). Charged with\ndirichletC2 \u2264 1 \u2014 the tight R(1.5) = 5.94 would need a dirichletC2 \u2264\n0.57 build (documented as the tightening path; the fold is\nindifferent: \u0394 \u2248 +2.4 per side). -/\ntheorem hIntegral_Jlag_dogleg_norm_le {n : \u2115} {U XR : \u211d}\n    (hU : 0 < U) (hnU : (n : \u211d) \u2264 (4 / 9) * U ^ 2) (hXR : 3 \u2264 XR) :\n    \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264 (8.38 : \u211d) := by\n  have hc : (0 : \u211d) < Real.log 2 - 4 / 9 := by\n    have h := cdog_gt\n    linarith\n  have hpt : \u2200 \u03c3 \u2208 Set.Ioc 3 XR,\n      \u2016Jlag n ((\u03c3 : \u211d) + U * Complex.I)\u2016 \u2264\n        dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) :=\n    fun \u03c3 h\u03c3 => Jlag_dogleg_norm_le_envelope (by linarith [h\u03c3.1]) hU hnU\n  have hcontA : Continuous (fun \u03c3 : \u211d => Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) :=\n    Real.continuous_exp.comp (continuous_const.mul continuous_id)\n  have hcontB : Continuous (fun \u03c3 : \u211d => (2 : \u211d) ^ (-\u03c3)) := by\n    have h1 : Continuous (fun \u03c3 : \u211d => Real.exp (-(Real.log 2) * \u03c3)) :=\n      Real.continuous_exp.comp (continuous_const.mul continuous_id)\n    have h2 : (fun \u03c3 : \u211d => (2 : \u211d) ^ (-\u03c3)) =\n        (fun \u03c3 : \u211d => Real.exp (-(Real.log 2) * \u03c3)) := by\n      funext \u03c3\n      rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n      congr 1\n      ring\n    rw [h2]\n    exact h1\n  have hIntA : IntervalIntegrable (fun \u03c3 : \u211d => 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3))\n      MeasureTheory.volume 3 XR := by\n    apply ContinuousOn.intervalIntegrable\n    exact (hcontA.const_mul 4).continuousOn\n  have hIntB : IntervalIntegrable (fun \u03c3 : \u211d => 4 * (2 : \u211d) ^ (-\u03c3)) MeasureTheory.volume 3 XR := by\n    apply ContinuousOn.intervalIntegrable\n    exact (hcontB.const_mul 4).continuousOn\n  have hIntG : IntervalIntegrable (fun \u03c3 : \u211d =>\n      dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)))\n      MeasureTheory.volume 3 XR := by\n    have h := (hIntA.add hIntB).const_mul dirichletC2\n    convert h using 1\n  -- step 1: \u2016H\u2016 \u2264 \u222b envelope\n  have h1 : \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264\n      \u222b \u03c3 in (3 : \u211d)..XR,\n        dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := by\n    unfold HIntegral\n    apply intervalIntegral.norm_integral_le_of_norm_le hXR _ hIntG\n    exact Filter.Eventually.of_forall (fun \u03c3 h\u03c3 => hpt \u03c3 h\u03c3)\n  -- step 2: \u222b envelope = dirichletC2\u00b7(4\u222be^{\u2212c\u03c3} + 4\u222b2^{\u2212\u03c3})\n  have h2 : \u222b \u03c3 in (3 : \u211d)..XR,\n        dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3))\n      = dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n          (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3))) := by\n    rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_add hIntA hIntB]\n  -- step 3: the two integral bounds\n  have h3a : \u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) \u2264\n      Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by\n    rw [intervalIntegral.integral_const_mul]\n    have h := integral_exp_neg_le hc hXR\n    have he3c : Real.exp (-3 * (Real.log 2 - 4 / 9)) = Real.exp (4 / 3) / 8 := by\n      have h3l2 : Real.exp (-(3 * Real.log 2)) = 1 / 8 := by\n        have e1 : -(3 * Real.log 2) = Real.log (1 / 8) := by\n          rw [show ((1 : \u211d) / 8) = (2 ^ 3 : \u211d)\u207b\u00b9 by norm_num, Real.log_inv, Real.log_pow,\n            Nat.cast_ofNat]\n        rw [e1, Real.exp_log (by norm_num : (0 : \u211d) < 1 / 8)]\n      calc Real.exp (-3 * (Real.log 2 - 4 / 9))\n          = Real.exp ((4 / 3) + -(3 * Real.log 2)) := by congr 1; ring\n        _ = Real.exp (4 / 3) * Real.exp (-(3 * Real.log 2)) := by rw [Real.exp_add]\n        _ = Real.exp (4 / 3) / 8 := by rw [h3l2]; ring\n    rw [he3c] at h\n    calc 4 * \u222b \u03c3 in (3 : \u211d)..XR, Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)\n        \u2264 4 * ((Real.exp (4 / 3) / 8) / (Real.log 2 - 4 / 9)) :=\n          mul_le_mul_of_nonneg_left h (by norm_num)\n      _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by\n        field_simp [hc.ne']\n        ring\n  have h3b : \u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3) \u2264 1 / (2 * Real.log 2) := by\n    have h2e : (fun \u03c3 : \u211d => 4 * (2 : \u211d) ^ (-\u03c3)) =\n        (fun \u03c3 : \u211d => 4 * Real.exp (-(Real.log 2) * \u03c3)) := by\n      funext \u03c3\n      rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n      congr 1\n      ring\n    rw [h2e, intervalIntegral.integral_const_mul]\n    have h := integral_exp_neg_le (Real.log_pos (by norm_num : (1 : \u211d) < 2)) hXR\n    have h3l2 : Real.exp (-3 * Real.log 2) = 1 / 8 := by\n      have e1 : (-3 * Real.log 2) = Real.log (1 / 8) := by\n        rw [show ((1 : \u211d) / 8) = (2 ^ 3 : \u211d)\u207b\u00b9 by norm_num, Real.log_inv, Real.log_pow,\n          Nat.cast_ofNat]\n        ring\n      rw [e1, Real.exp_log (by norm_num : (0 : \u211d) < 1 / 8)]\n    rw [h3l2] at h\n    calc 4 * \u222b \u03c3 in (3 : \u211d)..XR, Real.exp (-(Real.log 2) * \u03c3)\n        \u2264 4 * ((1 / 8) / Real.log 2) := by\n          apply mul_le_mul_of_nonneg_left h (by norm_num : (0 : \u211d) \u2264 4)\n      _ = 1 / (2 * Real.log 2) := by\n        field_simp [(Real.log_pos (by norm_num : (1 : \u211d) < 2)).ne']\n        norm_num\n  -- step 4: the certified assembly\n  have hlog2 : (0.6931471803 : \u211d) \u2264 Real.log 2 := Real.log_two_gt_d9.le\n  have h48 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) \u2264 (7.6545 : \u211d) := by\n    have hcge := cdog_gt\n    have h1 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) \u2264 3.8073 / (2 * 0.2487) :=\n      div_le_div\u2080 (by norm_num : (0 : \u211d) \u2264 3.8073) exp_four_thirds_le\n        (by norm_num : (0 : \u211d) < 2 * 0.2487) (by linarith [hcge])\n    calc Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9))\n        \u2264 3.8073 / (2 * 0.2487) := h1\n      _ \u2264 7.6545 := by norm_num\n  have h72 : 1 / (2 * Real.log 2) \u2264 (0.7214 : \u211d) := by\n    have h1 : 1 / (2 * Real.log 2) \u2264 1 / (2 * 0.6931471803) :=\n      one_div_le_one_div_of_le (by positivity) (by linarith)\n    calc 1 / (2 * Real.log 2) \u2264 1 / (2 * 0.6931471803) := h1\n      _ \u2264 0.7214 := by norm_num\n  have hC2 : dirichletC2 \u2264 1 := dirichletC2_le_one\n  have hsum : dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n      (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3))) \u2264 (8.38 : \u211d) := by\n    have hA0 : (0 : \u211d) \u2264 Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by positivity\n    have hB0 : (0 : \u211d) \u2264 1 / (2 * Real.log 2) := by positivity\n    have hIntAB : (0 : \u211d) \u2264 (\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n        (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3)) := by\n      apply add_nonneg\n      \u00b7 apply intervalIntegral.integral_nonneg hXR\n        intro \u03c3 h\u03c3\n        positivity\n      \u00b7 apply intervalIntegral.integral_nonneg hXR\n        intro \u03c3 h\u03c3\n        positivity\n    calc dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n          (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3)))\n        \u2264 1 * (Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2)) := by\n          apply mul_le_mul hC2 (add_le_add h3a h3b) hIntAB (by norm_num)\n      _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2) := by ring\n      _ \u2264 7.6545 + 0.7214 := add_le_add h48 h72\n      _ \u2264 8.38 := by norm_num\n  calc \u2016HIntegral (Jlag n) 3 XR U\u2016\n      \u2264 \u222b \u03c3 in (3 : \u211d)..XR,\n          dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) := h1\n    _ = dirichletC2 * ((\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) +\n          (\u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3))) := h2\n    _ \u2264 8.38 := hsum\n\n/-! ## 6. The far-right vertical drop (DL-4, D-074 \u00a78) -/\n\n/-- **Kernel at the far-right vertical** (D-074 \u00a78): for n \u2265 16 and\nt\u00b2 \u2265 n, \u2016kFun n (2\u221an+it)\u2016 \u2264 e^{\u221an/2}+1. (The ii\u2032-4 lemma\n`kFun_shift_norm_le_exp_sqrt_half_add_one` takes re s \u2265 2\u221an, i.e.\nre w \u2265 2\u221an+1 \u2014 this is the w = 2\u221an variant: |1+1/(w\u22121)| \u2264\n1+(2\u221an)/((2\u221an\u22121)\u00b2+t\u00b2) \u2264 1+1/(2\u221an) since 4\u221an\u22121 \u2264 t\u00b2.) -/\ntheorem kFun_right_vertical_norm_le_exp_sqrt_half_add_one {n : \u2115} {t : \u211d}\n    (hn : 16 \u2264 n) (ht : (n : \u211d) \u2264 t ^ 2) :\n    \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n      Real.exp (Real.sqrt (n : \u211d) / 2) + 1 := by\n  have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n  have hsq : (0 : \u211d) < Real.sqrt (n : \u211d) := Real.sqrt_pos.mpr (by linarith)\n  have hw1 : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1 =\n      ((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I := by\n    push_cast\n    ring\n  have hs0 : ((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I \u2260 0 := by\n    intro h\n    have him : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).im = 0 := by\n      rw [h]; simp\n    simp at him\n    have ht0 : t = 0 := by\n      have h1 : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).im = t := by simp\n      linarith\n    rw [ht0] at ht\n    nlinarith [hnR]\n  have hle := norm_one_add_one_div_le hs0\n  have hre : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).re + 1 =\n      2 * Real.sqrt (n : \u211d) := by\n    simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n      Complex.sub_re, Complex.one_re]\n  have hns : Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) =\n      (2 * Real.sqrt (n : \u211d) - 1) ^ 2 + t ^ 2 := by\n    simp [Complex.normSq_apply]\n    ring\n  have hkey : (2 * Real.sqrt (n : \u211d)) /\n      Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n      1 / (2 * Real.sqrt (n : \u211d)) := by\n    rw [hns]\n    have hsqn : Real.sqrt (n : \u211d) ^ 2 = (n : \u211d) := Real.sq_sqrt (by linarith)\n    have h1 : 4 * Real.sqrt (n : \u211d) - 1 \u2264 t ^ 2 := by\n      have h2 : 4 * Real.sqrt (n : \u211d) \u2264 (n : \u211d) + 1 := by\n        have h3 : (4 * Real.sqrt (n : \u211d)) ^ 2 \u2264 ((n : \u211d) + 1) ^ 2 := by\n          rw [show (4 * Real.sqrt (n : \u211d)) ^ 2 = 16 * (Real.sqrt (n : \u211d) ^ 2) by ring, hsqn]\n          nlinarith [sq_nonneg ((n : \u211d) - 1), hnR]\n        nlinarith [hsq]\n      nlinarith [ht, h2]\n    rw [show (2 * Real.sqrt (n : \u211d) - 1) ^ 2 + t ^ 2 =\n        4 * (Real.sqrt (n : \u211d) ^ 2) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2 by ring, hsqn]\n    have h4 : (0 : \u211d) < 4 * (n : \u211d) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2 := by\n      nlinarith [ht, sq_nonneg t, hsq]\n    rw [div_le_iff\u2080 h4,\n      show (1 / (2 * Real.sqrt (n : \u211d))) * (4 * (n : \u211d) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2) =\n        (4 * (n : \u211d) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2) / (2 * Real.sqrt (n : \u211d)) by\n        field_simp [hsq.ne'],\n      le_div_iff\u2080 (by linarith [hsq] : (0 : \u211d) < 2 * Real.sqrt (n : \u211d))]\n    nlinarith [h1, ht, hsq, hsqn]\n  have hstep : 1 + ((((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).re + 1) /\n      Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n      1 + 1 / (2 * Real.sqrt (n : \u211d)) := by\n    rw [hre]\n    have h1 : (2 * Real.sqrt (n : \u211d)) /\n        Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n        1 / (2 * Real.sqrt (n : \u211d)) := hkey\n    linarith [h1]\n  have hpow1 : \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I))\u2016 ^ n \u2264\n      (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n :=\n    pow_le_pow_left\u2080 (norm_nonneg _) (hle.trans hstep) n\n  have hpow2 : (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n \u2264\n      Real.exp (Real.sqrt (n : \u211d) / 2) := by\n    calc (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n\n        \u2264 (Real.exp (1 / (2 * Real.sqrt (n : \u211d)))) ^ n := by\n          have h := Real.add_one_le_exp (1 / (2 * Real.sqrt (n : \u211d)))\n          exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n      _ = Real.exp ((n : \u211d) * (1 / (2 * Real.sqrt (n : \u211d)))) :=\n          (Real.exp_nat_mul _ n).symm\n      _ = Real.exp (Real.sqrt (n : \u211d) / 2) := by\n          congr 1\n          have hsqn : Real.sqrt (n : \u211d) ^ 2 = (n : \u211d) := Real.sq_sqrt (by linarith)\n          field_simp [hsq.ne']\n          nlinarith [hsqn]\n  have hwid : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) /\n      ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1) =\n      1 + 1 / (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) := by\n    rw [hw1]\n    field_simp [hs0]\n    push_cast\n    ring\n  unfold kFun\n  rw [hwid]\n  calc \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I)) ^ n - 1\u2016\n      \u2264 \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n        norm_sub_le _ _\n    _ = \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I))\u2016 ^ n + 1 := by\n        rw [norm_pow, norm_one]\n    _ \u2264 Real.exp (Real.sqrt (n : \u211d) / 2) + 1 := by linarith [hpow1.trans hpow2]\n\n/-- **The far-right vertical drop** (D-074 \u00a78 V_right): for n \u2265 16,\n0 < T \u2264 U, T\u00b2 \u2265 n, \u2016VIntegral (Jlag n) (2\u221an) T U\u2016 \u2264\n(U\u2212T)\u00b7(e^{\u221an/2}+1)\u00b72^{\u2212(2\u221an\u22122)}\u00b7dirichletC2 \u2014 exponentially tiny. -/\ntheorem vIntegral_Jlag_right_norm_le {n : \u2115} {T U : \u211d}\n    (hn : 16 \u2264 n) (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n    \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T U\u2016 \u2264\n      (U - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n        ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by\n  have hnorm : \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T U\u2016 =\n      \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 := by\n    unfold VIntegral\n    rw [norm_smul, Complex.norm_I, one_mul]\n  rw [hnorm]\n  have hbound : \u2200 t \u2208 Set.Ioc T U,\n      \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n        (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n          ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by\n    intro t ht\n    have htT : T < t := ht.1\n    have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n    have h1 := kFun_right_vertical_norm_le_exp_sqrt_half_add_one hn ht2\n    have h2 := norm_logDeriv_zeta_le_two_pow\n      (show (2 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) by\n        have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n        have hsq : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n          have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n            Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n          have h2 : Real.sqrt 16 = 4 := by\n            rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n          rwa [h2] at h1\n        linarith) (t := t)\n    have hnorm3 : \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 =\n        \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 *\n          \u2016logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 := by\n      show \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) *\n          (-logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I))\u2016 = _\n      rw [norm_mul, norm_neg]\n    rw [hnorm3]\n    exact mul_le_mul h1 h2 (norm_nonneg _)\n      (add_nonneg (Real.exp_nonneg _) (by norm_num))\n  have hint : \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n      ((Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n        ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2)) * |U - T| := by\n    apply intervalIntegral.norm_integral_le_of_norm_le_const\n    intro t ht\n    rw [Set.uIoc_of_le hTU] at ht\n    exact hbound t ht\n  have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n  rw [habs] at hint\n  calc \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016\n      \u2264 ((Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n          ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2)) * (U - T) := hint\n    _ = (U - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n          ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by ring\n\n/-! ## 7. The total right-horizontal bound (DL-5, D-074 \u00a73.4) -/\n\n/-- **The upper right-tail bound** (D-074 \u00a73.4): for n \u2265 16 and\nT \u2208 [\u221an, \u221an+1] (the T_cut window), U = (3/2)\u00b7T,\n\u2016HIntegral (Jlag n) 3 (2\u221an) T\u2016 \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)/2 + 8.38 +\nIIMaj(n)/2 \u2014 the exact deformation identity +\nV_left/H_high/V_right piece bounds, all in the zero-free region. -/\ntheorem hIntegral_Jlag_low_le_dogLegUpper {n : \u2115} {T : \u211d}\n    (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n    \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 \u2264\n      ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n        IIMaj (n : \u211d) / 2 := by\n  have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n  have hsqrt4 : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n    have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n      Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n    have h2 : Real.sqrt 16 = 4 := by\n      rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n    rwa [h2] at h1\n  have hT0 : (0 : \u211d) < T := by linarith\n  have hTn2 : (n : \u211d) \u2264 T ^ 2 := by\n    have h1 : (Real.sqrt (n : \u211d)) ^ 2 \u2264 T ^ 2 :=\n      pow_le_pow_left\u2080 (Real.sqrt_nonneg _) hTn 2\n    rwa [Real.sq_sqrt (by linarith [Real.sqrt_nonneg (n : \u211d)])] at h1\n  have hU0 : (0 : \u211d) < (3 / 2) * T := by linarith [hT0]\n  have hTU : T \u2264 (3 / 2) * T := by linarith [hT0]\n  have hnU : (n : \u211d) \u2264 (4 / 9) * ((3 / 2) * T) ^ 2 := by\n    have h1 : (4 / 9) * ((3 / 2) * T) ^ 2 = T ^ 2 := by\n      field_simp\n      ring\n    rw [h1]\n    exact hTn2\n  have hXR : (3 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) := by linarith\n  have hid := upper_right_horizontal_eq_dogleg hT0 hTU hXR (n := n)\n  have hH := hIntegral_Jlag_dogleg_norm_le hU0 hnU hXR (n := n)\n  have hVr := vIntegral_Jlag_right_norm_le hn hT0 hTU hTn2 (n := n)\n  have hVl := vIntegral_Jlag_three_norm_le hT0 hTU hTn2 (n := n)\n  have hlen : (3 / 2) * T - T \u2264 (Real.sqrt (n : \u211d) + 1) / 2 := by linarith [hTn1, hTn]\n  have hlen0 : (0 : \u211d) \u2264 (3 / 2) * T - T := by linarith [hT0]\n  -- V_left \u2264 ((\u221an+1)/2)\u00b7(e^{5/2}+1)/2\n  have hVl2 : \u2016VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016 \u2264\n      ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 := by\n    refine hVl.trans ?_\n    exact div_le_div_of_nonneg_right\n      (mul_le_mul hlen (le_refl _) (by positivity) (by positivity)) (by norm_num)\n  -- V_right \u2264 IIMaj/2\n  have hVr2 : \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016 \u2264\n      IIMaj (n : \u211d) / 2 := by\n    have hC2 : dirichletC2 \u2264 1 := dirichletC2_le_one\n    have hK : (0 : \u211d) < (Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n        ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by positivity\n    have eA : ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n        ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d)) =\n        (1 / 2) * ((Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n          ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by ring\n    have eB : IIMaj (n : \u211d) / 2 =\n        (0.57 : \u211d) * ((Real.sqrt (n : \u211d) + 1) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n          ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by\n      unfold IIMaj\n      ring\n    calc \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016\n        \u2264 ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n            ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := hVr\n      _ \u2264 ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n            ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d)) := by\n          have h1 : ((3 / 2) * T - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) \u2264\n              ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) :=\n            mul_le_mul hlen (le_refl _) (by positivity) (by positivity)\n          have h2 : (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2 \u2264\n              (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * (1 : \u211d) :=\n            mul_le_mul_of_nonneg_left hC2 (Real.rpow_nonneg (by norm_num) _)\n          exact mul_le_mul h1 h2\n            (mul_nonneg (Real.rpow_nonneg (by norm_num) _) dirichletC2_nonneg)\n            (by positivity)\n      _ \u2264 IIMaj (n : \u211d) / 2 := by\n          rw [eA, eB]\n          apply mul_le_mul_of_nonneg_right _ hK.le\n          norm_num\n  -- assemble via the exact identity\n  rw [hid]\n  calc \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T) -\n        VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T) +\n        VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016\n      \u2264 \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T)\u2016 +\n        \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T)\u2016 +\n        \u2016VIntegral (Jlag n) 3 T ((3 / 2) * T)\u2016 := by\n        have h1 := norm_add_le\n          (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T) -\n            VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T))\n          (VIntegral (Jlag n) 3 T ((3 / 2) * T))\n        have h2 := norm_sub_le\n          (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) ((3 / 2) * T))\n          (VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T ((3 / 2) * T))\n        linarith [h1, h2]\n    _ \u2264 (8.38 : \u211d) + IIMaj (n : \u211d) / 2 +\n        ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 :=\n        add_le_add (add_le_add hH hVr2) hVl2\n    _ = ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n        IIMaj (n : \u211d) / 2 := by ring\n\n/-- **The lower right-tail bound by conjugation** (D-074 \u00a73.4): the\nsame bound holds at im = \u2212T (the integrand is conjugation-symmetric,\nJlag_conj; the interval integral maps conj through). -/\ntheorem hIntegral_Jlag_low_neg_norm_le_dogLegUpper {n : \u2115} {T : \u211d}\n    (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n    \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264\n      ((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n        IIMaj (n : \u211d) / 2 := by\n  have hT0 : (0 : \u211d) < T := by\n    have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n    have hsqrt4 : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n      have h1 : Real.sqrt 16 \u2264 Real.sqrt (n : \u211d) :=\n        Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : \u211d) \u2264 (n : \u211d))\n      have h2 : Real.sqrt 16 = 4 := by\n        rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num\n      rwa [h2] at h1\n    linarith\n  have hconj : HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T) =\n      (starRingEnd \u2102) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T) := by\n    unfold HIntegral\n    rw [\u2190 intervalIntegral_conj]\n    apply intervalIntegral.integral_congr\n    intro \u03c3 h\u03c3\n    have hid2 : ((\u03c3 : \u211d) + (-T) * Complex.I) =\n        (starRingEnd \u2102) ((\u03c3 : \u211d) + T * Complex.I) := by\n      simp [Complex.ext_iff]\n    rw [hid2]\n    exact Jlag_conj n (by\n      intro h\n      have him : (((\u03c3 : \u211d) + T * Complex.I)).im = T := by simp\n      rw [h] at him\n      simp at him\n      linarith [hT0])\n  rw [hconj, Complex.norm_conj]\n  exact hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1\n\n/-- **THE TWO-SIDE RIGHT-HORIZONTAL BOUND** (the DL capstone for\nii\u2032-6-c): both horizontal right tails bounded by the dog-leg charge. -/\ntheorem dogLegUpper_two_sides {n : \u2115} {T : \u211d}\n    (hn : 16 \u2264 n) (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n    \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 +\n      \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264\n    2 * (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n      IIMaj (n : \u211d) / 2) := by\n  rw [show (2 : \u211d) * (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 +\n      (8.38 : \u211d) + IIMaj (n : \u211d) / 2) =\n      (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n        IIMaj (n : \u211d) / 2) +\n      (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n        IIMaj (n : \u211d) / 2) by ring]\n  exact add_le_add (hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1)\n    (hIntegral_Jlag_low_neg_norm_le_dogLegUpper hn hTn hTn1)\n\nend NguyenRH1\n\nend\n",
  "structuredPatch": [
    {
      "oldStart": 995,
      "oldLines": 7,
      "newStart": 995,
      "newLines": 7,
      "lines": [
        "   have hconj : HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) (-T) =",
        "       (starRingEnd \u2102) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T) := by",
        "     unfold HIntegral",
        "-    rw [\u2190 intervalIntegral_conj]",
        "+    rw [\u2190 RCLike.intervalIntegral_conj]",
        "     apply intervalIntegral.integral_congr",
        "     intro \u03c3 h\u03c3",
        "     have hid2 : ((\u03c3 : \u211d) + (-T) * Complex.I) ="
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
  "old_string": "      have h7 : HasDerivAt (fun y : \u211d => (\u2191y : \u2102)) (1 : \u2102) x := by\n        have h8 := Complex.ofRealCLM.hasDerivAt (x := x)\n        rw [Complex.ofRealCLM_apply] at h8\n        simpa using h8\n      have h9 : HasDerivAt Complex.Gamma (deriv Complex.Gamma (\u2191x : \u2102)) (\u2191x : \u2102) := by\n        apply (Complex.differentiableAt_Gamma _ _).hasDerivAt\n        intro m hmeq\n        rw [hmeq] at hx0\n        simp at hx0\n        have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n        linarith\n      have h10 := h9.comp x h7\n      -- comp gives deriv Gamma \u2191x * 1\n      rw [mul_one] at h10\n      have heq : (Complex.Gamma \u2218 fun y : \u211d => (\u2191y : \u2102)) = fun y : \u211d => Complex.Gamma (\u2191y) := rfl\n      rw [heq] at h10\n      exact h10.deriv\n    rw [h6] at h1\n    exact h1.deriv",
  "new_string": "      have h7 : HasDerivAt (fun y : \u211d => (\u2191y : \u2102)) (1 : \u2102) x := by\n        have h8 := Complex.ofRealCLM.hasDerivAt (x := x)\n        rw [Complex.ofRealCLM_apply] at h8\n        exact h8\n      have h9 : HasDerivAt Complex.Gamma (deriv Complex.Gamma (\u2191x : \u2102)) (\u2191x : \u2102) := by\n        apply (Complex.differentiableAt_Gamma _ _).hasDerivAt\n        intro m hmeq\n        have h2 : (x : \u211d) = -(m : \u211d) := by\n          have h3 : (\u2191x : \u2102).re = (-(m : \u2102)).re := by rw [hmeq]\n          simp at h3\n          exact h3\n        have hm : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n        linarith\n      have h10 := h9.comp x h7\n      -- comp gives deriv Gamma \u2191x * 1\n      rw [mul_one] at h10\n      have heq : (Complex.Gamma \u2218 fun y : \u211d => (\u2191y : \u2102)) = fun y : \u211d => Complex.Gamma (\u2191y) := rfl\n      rw [heq] at h10\n      exact h10.deriv\n    have h5 : (fun y : \u211d => Complex.Gamma (\u2191y)) = fun y : \u211d => (\u2191(Real.Gamma y) : \u2102) :=\n      funext fun y => Complex.Gamma_ofReal y\n    have h1d : deriv (fun y : \u211d => (\u2191(Real.Gamma y) : \u2102)) x = \u2191(deriv Real.Gamma x) := h1.deriv\n    rw [\u2190 h5] at h1d\n    rw [h6] at h1d\n    exact h1d"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean",
  "oldString": "          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]",
  "newString": "          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/-! ## 3. The separated reciprocal sum (C) -/\n\n/-- The right half of the V-split: for j\u2080 = \u2308\u2212re w\u2309\u208a and j > j\u2080,\n\u2016(w+j)\u207b\u00b9\u2016 \u2264 1/(j\u2212j\u2080) (real parts are 1-separated and j\u2080 catches up to\n\u2212re w). -/\ntheorem recip_norm_le_right {w : \u2102} {c : \u211d} (hdist : \u2200 m : \u2115, c \u2264 \u2016w + (m : \u2102)\u2016)\n    {j\u2080 : \u2115} (hj\u2080 : j\u2080 = \u2308-w.re\u2309\u208a) {j : \u2115} (hj : j\u2080 + 1 \u2264 j) :\n    \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 ((j - j\u2080 : \u2115) : \u211d)\u207b\u00b9 := by\n  have hj\u2080ge : -(w.re) \u2264 (j\u2080 : \u211d) := by rw [hj\u2080]; exact Nat.le_ceil _\n  have hrewj : (w + (j : \u2102)).re = w.re + (j : \u211d) := by\n    simp [Complex.add_re, Complex.natCast_re]\n  have hnorm : \u2016(w + (j : \u2102))\u207b\u00b9\u2016 = \u2016w + (j : \u2102)\u2016\u207b\u00b9 := norm_inv\n  rw [hnorm]\n  have hge : ((j - j\u2080 : \u2115) : \u211d) \u2264 \u2016w + (j : \u2102)\u2016 := by\n    have h1 : (w + (j : \u2102)).re \u2264 \u2016w + (j : \u2102)\u2016 := by\n      have h2 := Complex.abs_re_le_norm (w + (j : \u2102))\n      rwa [abs_of_nonneg (by\n        rw [hrewj]\n        have h3 : (0 : \u211d) \u2264 w.re + (j\u2080 : \u211d) := by linarith [hj\u2080ge]\n        have h4 : ((j\u2080 : \u211d) + 1) \u2264 (j : \u211d) := by exact_mod_cast hj\n        linarith [h3, h4])] at h2\n    refine le_trans ?_ h1\n    rw [hrewj]\n    have h3 : (0 : \u211d) \u2264 w.re + (j\u2080 : \u211d) := by linarith [hj\u2080ge]\n    have h4 : ((j - j\u2080 : \u2115) : \u211d) = (j : \u211d) - (j\u2080 : \u211d) := by\n      rw [Nat.cast_sub (by omega : j\u2080 \u2264 j)]\n    rw [h4]\n    linarith [h3]\n  have hpos : (0 : \u211d) < ((j - j\u2080 : \u2115) : \u211d) := by\n    have h1 : (1 : \u2115) \u2264 j - j\u2080 := by omega\n    have h2 : (0 : \u211d) < ((j - j\u2080 : \u2115) : \u211d) := by exact_mod_cast h1\n    exact h2\n  exact (inv_le_inv\u2080 (by linarith [hge, hpos]) hpos).mpr hge\n\n/-- The left half: for j < j\u2080 \u2212 1 (so j\u2080 \u2265 2 and the real part is still\nnegative), \u2016(w+j)\u207b\u00b9\u2016 \u2264 1/(j\u2080\u22121\u2212j). -/\ntheorem recip_norm_le_left {w : \u2102} {c : \u211d} (hdist : \u2200 m : \u2115, c \u2264 \u2016w + (m : \u2102)\u2016)\n    {j\u2080 : \u2115} (hj\u2080 : j\u2080 = \u2308-w.re\u2309\u208a) {j : \u2115} (hj : j + 1 \u2264 j\u2080 - 1) :\n    \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 ((j\u2080 - 1 - j : \u2115) : \u211d)\u207b\u00b9 := by\n  have hj\u2080lt : (j\u2080 : \u211d) < -w.re + 1 := by\n    rw [hj\u2080]\n    by_cases hre : 0 \u2264 -w.re\n    \u00b7 have h := Nat.ceil_lt_add_one hre\n      have h2 : ((\u2308-w.re\u2309\u208a : \u2115) : \u211d) < -w.re + 1 := by exact_mod_cast h\n      exact h2\n    \u00b7 push Not at hre\n      have h1 : \u2308-w.re\u2309\u208a = 0 := by\n        apply Nat.ceil_eq_zero.mpr\n        linarith [hre]\n      rw [h1] at hj\u2080\n      -- j\u2080 = 0 but j + 1 \u2264 j\u2080 \u2212 1 = 0 \u2212 1 = 0 in \u2115: impossible\n      omega\n  have hrewj : (w + (j : \u2102)).re = w.re + (j : \u211d) := by\n    simp [Complex.add_re, Complex.natCast_re]\n  have hneg : (w + (j : \u2102)).re < 0 := by\n    rw [hrewj]\n    have h4 : ((j : \u211d) + 1) \u2264 (j\u2080 : \u211d) - 1 := by exact_mod_cast hj\n    linarith [hj\u2080lt, h4]\n  have hnorm : \u2016(w + (j : \u2102))\u207b\u00b9\u2016 = \u2016w + (j : \u2102)\u2016\u207b\u00b9 := norm_inv\n  rw [hnorm]\n  have hge : ((j\u2080 - 1 - j : \u2115) : \u211d) \u2264 \u2016w + (j : \u2102)\u2016 := by\n    have h1 : |(w + (j : \u2102)).re| \u2264 \u2016w + (j : \u2102)\u2016 := Complex.abs_re_le_norm _\n    rw [hrewj] at h1\n    have h2 : |(w.re + (j : \u211d))| = -(w.re + (j : \u211d)) := abs_of_neg (by rwa [\u2190 hrewj])\n    rw [h2] at h1\n    refine le_trans ?_ h1\n    have h4 : ((j\u2080 - 1 - j : \u2115) : \u211d) = (j\u2080 : \u211d) - 1 - (j : \u211d) := by\n      rw [Nat.cast_sub (by omega : j \u2264 j\u2080 - 1), Nat.cast_sub (by omega : 1 \u2264 j\u2080)]\n      push_cast\n      ring\n    rw [h4]\n    linarith [hj\u2080lt]\n  have hpos : (0 : \u211d) < ((j\u2080 - 1 - j : \u2115) : \u211d) := by\n    have h1 : (1 : \u2115) \u2264 j\u2080 - 1 - j := by omega\n    exact_mod_cast h1\n  exact (inv_le_inv\u2080 (by linarith [hge, hpos]) hpos).mpr hge\n\n/-- **The separated reciprocal sum bound (C)**: for dist(w, \u2212\u2115) \u2265 c > 0,\n\u03a3_{j<m} \u2016(w+j)\u207b\u00b9\u2016 \u2264 2/c + 2 + 2\u00b7log m (the V-split: at most one term per\nside needs the dist condition; the rest telescope into the harmonic bound). -/\ntheorem digamma_recip_sum_le {c : \u211d} (hc : 0 < c) {w : \u2102}\n    (hdist : \u2200 m : \u2115, c \u2264 \u2016w + (m : \u2102)\u2016) {m : \u2115} (hm : \u2308-w.re\u2309\u208a + 1 \u2264 m) :\n    \u2211 j \u2208 Finset.range m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 2 / c + 2 + 2 * Real.log m := by\n  set j\u2080 := \u2308-w.re\u2309\u208a with hj\u2080\n  have hj\u2080m : j\u2080 \u2264 m := by omega\n  -- split range m = range j\u2080 \u222a Ico j\u2080 m\n  have hsplit : \u2211 j \u2208 Finset.range m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n      = \u2211 j \u2208 Finset.range j\u2080, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n        + \u2211 j \u2208 Finset.Ico j\u2080 m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 := by\n    rw [Finset.range_eq_Ico, Finset.range_eq_Ico,\n      \u2190 Finset.sum_Ico_consecutive _ (Nat.zero_le j\u2080) hj\u2080m]\n  rw [hsplit]\n  -- RIGHT side: Ico j\u2080 m \u2014 the first term by dist, the rest by recip_norm_le_right\n  have hright : \u2211 j \u2208 Finset.Ico j\u2080 m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n      \u2264 1 / c + (1 + Real.log m) := by\n    by_cases hj\u20801 : j\u2080 + 1 \u2264 m\n    \u00b7 -- Ico j\u2080 m = {j\u2080} \u222a Ico (j\u2080+1) m\n      have hdecomp : Finset.Ico j\u2080 m = {j\u2080} \u222a Finset.Ico (j\u2080 + 1) m := by\n        rw [Finset.Ico_union_Ico_eq_Ico (Nat.le_refl j\u2080) hj\u20801]\n        exact (Finset.Ico_self_singleton).symm... \n```\nHmm \u2014 Ico j\u2080 (j\u2080+1) = {j\u2080}: `Finset.Ico_self_singleton`? the name... `Finset.Ico_succ_singleton : Ico n (n+1) = {n}` \u2713 I believe. Then the union: Ico j\u2080 (j\u2080+1) \u222a Ico (j\u2080+1) m = Ico j\u2080 m via Finset.Ico_union_Ico_eq_Ico (le_refl) hj\u20801 \u2713. So Ico j\u2080 m = {j\u2080} \u222a Ico (j\u2080+1) m via rw [\u2190 Finset.Ico_succ_singleton... wait I need Ico j\u2080 m = {j\u2080} \u222a ...: {j\u2080} = Ico j\u2080 (j\u2080+1) via Ico_succ_singleton.symm; then Ico j\u2080 (j\u2080+1) \u222a Ico (j\u2080+1) m = Ico j\u2080 m via the union lemma. So:\n```\n      have hdecomp : Finset.Ico j\u2080 m = Finset.Ico j\u2080 (j\u2080 + 1) \u222a Finset.Ico (j\u2080 + 1) m :=\n        (Finset.Ico_union_Ico_eq_Ico (Nat.le_refl j\u2080) hj\u20801).symm\n      rw [hdecomp, Finset.Ico_succ_singleton]  -- hmm Ico j\u2080 (j\u2080+1) = {j\u2080}: Finset.Ico_succ_singleton : Ico n (n+1) = {n} \u2014 rw turns it into {j\u2080}: then sum over {j\u2080} \u222a ...: Finset.sum_union (disjoint) \u2014 the disjointness: {j\u2080} \u2229 Ico (j\u2080+1) m = \u2205: Finset.disjoint_singleton_left: j\u2080 \u2209 Ico (j\u2080+1) m: Finset.not_mem_Ico: j\u2080 < j\u2080+1 \u2264 ... hmm `Finset.Ico_disjoint_Ico_consecutive`? there's `Finset.Ico_disjoint_Ico_consecutive (a b c) : Disjoint (Ico a b) (Ico b c)` \u2713 I recall. So:\n      rw [hdecomp, Finset.Ico_succ_singleton,\n        Finset.sum_union (Finset.disjoint_singleton_left.mpr (by\n          simp [Finset.mem_Ico] : j\u2080 \u2209 Finset.Ico (j\u2080+1) m)),  -- hmm the disjoint_singleton_left form\n        Finset.sum_singleton]\n```\nThis is getting heavy. SIMPLER alternative: use `Finset.sum_Ico_succ_top`? no that's the top. For the BOTTOM: `Finset.sum_Ico_eq_sum_range` reindex the whole Ico (j\u2080+1) m part and handle the j\u2080 term separately via... actually cleanest: DON'T peel the first term; instead bound the FIRST term inline via a case split in the sum: \n\nAlternative cleaner structure: bound \u2211 Ico j\u2080 m directly:\n\u2211 j \u2208 Ico j\u2080 m, term_j = term_{j\u2080} + \u2211_{j \u2208 Ico (j\u2080+1) m} term_j \u2014 the peeling: `Finset.sum_Ico_succ_top`? no. There IS `Finset.sum_Ico_eq_sub`? no. The bottom-peel: `Finset.Ico.erase`... Or use: `Finset.sum_Ico_succ_bot`? hmm \u2014 sum over Ico (a) b with a < b = f a + \u2211 Ico (a+1) b: the lemma name might be `Finset.sum_Ico_eq_head_add_sum_tail`? not a thing. There IS: `Finset.sum_range_succ` and for Ico: `Finset.sum_Ico_eq_sum_range` + `Finset.sum_range_succ'`? Let me just do the reindex for the whole right side INCLUDING j\u2080's term with a per-term piecewise bound:\n\nFor j \u2208 Ico j\u2080 m: term_j \u2264 h j where h j := if j = j\u2080 then 1/c else ((j \u2212 j\u2080 : \u2115):\u211d)\u207b\u00b9. Then \u2211 = (peel j\u2080) ... still needs the peel. \n\nOK \u2014 the cleanest available: `Finset.sum_eq_sum_diff_singleton_add`? or `Finset.add_sum_erase`: \u2211_{Ico j\u2080 m} f = f j\u2080 + \u2211_{(Ico j\u2080 m).erase j\u2080} f \u2014 and (Ico j\u2080 m).erase j\u2080 = Ico (j\u2080+1) m: `Finset.Ico_erase_left : (Ico a b).erase a = Ico (a+1) b` \u2713 I believe that exists. So:\n```\n      rw [\u2190 Finset.add_sum_erase _ _ (Finset.left_mem_Ico.mpr (by omega : j\u2080 < m))]  -- hmm add_sum_erase : f a + \u2211 x \u2208 s.erase a, f x = \u2211 x \u2208 s, f x for a \u2208 s \u2014 so \u2190 direction turns the sum into f j\u2080 + erase-sum \u2713\n      rw [Finset.Ico_erase_left]  -- (Ico j\u2080 m).erase j\u2080 = Ico (j\u2080+1) m\n```\nFinset.left_mem_Ico : a \u2208 Ico a b \u2194 a < b \u2713 (I think). Then:\n```\n      -- term at j\u2080: \u2264 1/c\n      have hfirst : \u2016(w + (j\u2080 : \u2102))\u207b\u00b9\u2016 \u2264 1 / c := by\n        rw [norm_inv]\n        rw [show (1 : \u211d) / c = (c : \u211d)\u207b\u00b9 by rw [one_div]]\n        exact (inv_le_inv\u2080 hc (hdist j\u2080)).mpr (hdist j\u2080)  -- hmm inv_le_inv\u2080 (ha : 0 < a) (hb : 0 < b) : a\u207b\u00b9 \u2264 b\u207b\u00b9 \u2194 b \u2264 a: \u2016w+j\u2080\u2016\u207b\u00b9 \u2264 c\u207b\u00b9 \u27fa c \u2264 \u2016w+j\u2080\u2016: (inv_le_inv\u2080 (by linarith [hdist j\u2080, hc] : (0:\u211d) < \u2016w+j\u2080\u2016) hc).mpr (hdist j\u2080) \u2713\n      -- the rest: reindex to the harmonic bound\n      have hrest : \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 1 + Real.log m := by\n        calc \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n            \u2264 \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, ((j - j\u2080 : \u2115) : \u211d)\u207b\u00b9 :=\n              Finset.sum_le_sum fun j hj => recip_norm_le_right hdist hj\u2080 (by\n                rw [Finset.mem_Ico] at hj; exact hj.1)\n          _ = \u2211 i \u2208 Finset.range (m - (j\u2080 + 1)), ((i : \u211d) + 1)\u207b\u00b9 := by\n              rw [Finset.sum_Ico_eq_sum_range]  -- \u2211 i \u2208 range ((j\u2080+1) ... hmm: sum_Ico_eq_sum_range : \u2211 i \u2208 Ico a b, f i = \u2211 i \u2208 range (b \u2212 a), f (a + i): with a := j\u2080+1, b := m: \u2211 i \u2208 range (m \u2212 (j\u2080+1)), f (j\u2080+1+i): f (j\u2080+1+i) = (((j\u2080+1+i) \u2212 j\u2080 : \u2115):\u211d)\u207b\u00b9: (j\u2080+1+i) \u2212 j\u2080 = i+1: \n              apply Finset.sum_congr rfl\n              intro i _\n              -- ((j\u2080+1+i) \u2212 j\u2080 : \u2115) = i + 1\n              have h1 : (j\u2080 + 1 + i) - j\u2080 = i + 1 := by omega\n              rw [h1]  -- then casts: ((i+1 : \u2115):\u211d) = (i:\u211d)+1: Nat.cast_add_one\n              rw [Nat.cast_add_one]\n          _ \u2264 1 + Real.log (m - (j\u2080 + 1)) := by\n              have h := sum_one_div_le_one_add_log (m - (j\u2080 + 1))\n              -- h's form: \u2211 1/(\u2191n+1) \u2264 1 + log \u2191(m\u2212j\u2080\u22121): my form: \u2211 (\u2191i+1)\u207b\u00b9: simpa [one_div]\n              simpa [one_div] using h\n          _ \u2264 1 + Real.log m := by\n              gcongr  -- 1 + log(m\u2212j\u2080\u22121) \u2264 1 + log m: log mono: Real.log_le_log (0 < m\u2212j\u2080\u22121) (m\u2212j\u2080\u22121 \u2264 m): the 0 < fails if m = j\u2080+1 \u2014 but then the range is empty... hmm the sum range (m\u2212(j\u2080+1)) with m = j\u2080+1: range 0: sum = 0: and 0 \u2264 1 + log m \u2713 (log m \u2265 0 for m \u2265 1: m \u2265 j\u2080+1 \u2265 1 \u2713... wait m \u2265 1: from hm : j\u2080+1 \u2264 m and j\u2080 \u2265 0: m \u2265 1 \u2713). The gcongr needs 0 < \u2191(m\u2212j\u2080\u22121) \u2014 fails when m = j\u2080+1 (then m\u2212j\u2080\u22121 = 0: log 0 = 0 junk: the step (1 + log 0) = 1 + 0 = 1 \u2264 1 + log m \u27fa 0 \u2264 log m \u2713 m \u2265 1). Split: by_cases m = j\u2080+1: then the sum is over range 0 = 0: 0 \u2264 1 + log m \u2713. Else: 1 \u2264 m\u2212j\u2080\u22121: log mono \u2713. Let me write:\n              by_cases hcase : m - (j\u2080 + 1) = 0\n              \u00b7 have : m - (j\u2080 + 1) = 0 := hcase\n                -- the sum \u2211 i \u2208 range 0 = 0 \u2014 but we're at the SECOND calc step's goal: (1 + log \u2191(m\u2212j\u2080\u22121)) \u2264 1 + log \u2191m: with \u2191(m\u2212j\u2080\u22121) = 0: log 0 = 0: \n                rw [hcase]  -- \u2191(0:\u2115) = 0: Nat.cast_zero: log 0 = 0: Real.log_zero\n                simp [Real.log_zero]  -- 1 + 0 \u2264 1 + log \u2191m \u27fa 0 \u2264 log \u2191m: Real.log_nonneg (1 \u2264 \u2191m): m \u2265 1 \u2713\n                exact Real.log_nonneg (by exact_mod_cast (by omega : 1 \u2264 m))\n              \u00b7 have h1 : (1 : \u2115) \u2264 m - (j\u2080 + 1) := by omega\n                have h2 : (0 : \u211d) < ((m - (j\u2080 + 1) : \u2115) : \u211d) := by exact_mod_cast h1\n                have h3 : ((m - (j\u2080 + 1) : \u2115) : \u211d) \u2264 (m : \u211d) := by\n                  rw [Nat.cast_sub (by omega : j\u2080 + 1 \u2264 m)]\n                  push_cast\n                  have h4 : (0 : \u211d) \u2264 (j\u2080 : \u211d) := by positivity\n                  linarith [h4]\n                have h4 : Real.log ((m - (j\u2080 + 1) : \u2115) : \u211d) \u2264 Real.log (m : \u211d) :=\n                  Real.log_le_log h2 h3\n                linarith [h4]\n      -- combine\n      calc \u2211 j \u2208 Finset.Ico j\u2080 m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016\n          = \u2016(w + (j\u2080 : \u2102))\u207b\u00b9\u2016 + \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 := by\n            rw [Finset.add_sum_erase _ _ (Finset.left_mem_Ico.mpr (by omega : j\u2080 < m)),\n              Finset.Ico_erase_left]\n        _ \u2264 1 / c + (1 + Real.log m) := add_le_add hfirst hrest\n    \u00b7 -- \u00ac(j\u2080+1 \u2264 m) \u27f9 m \u2264 j\u2080: the Ico is empty\n      push Not at hj\u20801\n      have hempty : Finset.Ico j\u2080 m = \u2205 := Finset.Ico_eq_empty_of_le (by omega : m \u2264 j\u2080)  -- Finset.Ico_eq_empty_of_le (h : b \u2264 a) : Ico a b = \u2205? check name \u2014 maybe `Finset.Ico_eq_empty_iff : Ico a b = \u2205 \u2194 b \u2264 a` \u2014 use .mpr\n      rw [hempty]\n      simp  -- \u2211 \u2205 = 0 \u2264 1/c + (1 + log m): positivity... needs 1/c > 0 and log m \u2265 0: m \u2265 j\u2080+1\u2212... hmm here m \u2264 j\u2080: log m could be log 0 = 0 (m = 0) or log of small \u2014 m \u2264 j\u2080 but from hm : j\u2080+1 \u2264 m?? \u2014 WAIT hm : j\u2080 + 1 \u2264 m is the THEOREM's hypothesis \u2014 and the by_cases hj\u20801 : j\u2080+1 \u2264 m is ALWAYS true by hm!! So the else branch is vacuous: hj\u20801 contradicts hm: omega closes:\n      omega  -- hm : j\u2080 + 1 \u2264 m and hj\u20801 : \u00ac(j\u2080+1 \u2264 m) \u2014 False \u27f9 anything\n```\nWait \u2014 hm : \u2308\u2212w.re\u2309\u208a + 1 \u2264 m i.e. j\u2080 + 1 \u2264 m \u2014 so the by_cases's second branch is vacuous \u2713 just `omega` (deriving False from hm and hj\u20801). Hmm \u2014 but the goal in that branch after `push Not at hj\u20801`: hj\u20801 : \u00ac j\u2080 + 1 \u2264 m; hm : j\u2080 + 1 \u2264 m: `exact absurd hm hj\u20801` closes any goal \u2713 cleaner: `exact absurd hm hj\u20801`. So drop the by_cases entirely \u2014 just use hj\u20801 := hm. Simplify: the right side always has j\u2080+1 \u2264 m \u2713 no by_cases needed!\n\nSimilarly the LEFT side: range j\u2080: if j\u2080 = 0: empty \u2713 handle via by_cases (j\u2080 = 0); else peel j\u2080\u22121 from the TOP: range j\u2080 = range (j\u2080\u22121) \u222a {j\u2080\u22121}... via Finset.sum_range_succ with j\u2080 = (j\u2080\u22121)+1: \u2211 range j\u2080 f = \u2211 range (j\u2080\u22121) f + f (j\u2080\u22121) (with j\u2080\u22121+1 = j\u2080 by omega-rewrite). The f (j\u2080\u22121) term \u2264 1/c (dist). The range (j\u2080\u22121) part: j \u2264 j\u2080\u22122 \u27f9 recip_norm_le_left (hj : j + 1 \u2264 j\u2080 \u2212 1): reindex: \u2211 j \u2208 range (j\u2080\u22121), ((j\u2080\u22121\u2212j : \u2115):\u211d)\u207b\u00b9 = \u2211 i \u2208 range (j\u2080\u22121), ((i:\u211d)+1)\u207b\u00b9 (reverse the range! j \u21a6 j\u2080\u22121\u2212j is an order-reversing bijection on range (j\u2080\u22121) \u2014 `Finset.sum_range_reflect`?? there IS `Finset.sum_range_reflect (f) (n) : \u2211 i \u2208 range n, f (n \u2212 1 \u2212 i) = \u2211 i \u2208 range n, f i` \u2713 I recall!). So \u2211 j \u2208 range (j\u2080\u22121), g (j\u2080\u22121\u2212j) = \u2211 j \u2208 range (j\u2080\u22121), g j with g j := ((j+1 : \u2115):\u211d)\u207b\u00b9?? hmm: my term after recip_norm_le_left: ((j\u2080\u22121\u2212j : \u2115):\u211d)\u207b\u00b9: let g x := ((x:\u2115):\u211d)\u207b\u00b9: the term is g (j\u2080\u22121\u2212j) with... j\u2080\u22121\u2212j for j \u2208 range (j\u2080\u22121): j\u2080\u22121\u2212j \u2208 {j\u2080\u22121, j\u2080\u22122, ..., 1}: sum_range_reflect: \u2211 j \u2208 range (j\u2080\u22121), g (j\u2080\u22121\u2212j) = \u2211 j \u2208 range (j\u2080\u22121), g j?? \u2014 sum_range_reflect : \u2211 i \u2208 range n, f (n \u2212 1 \u2212 i) = \u2211 i \u2208 range n, f i: with n := j\u2080\u22121: f (n\u22121\u2212i) = f (j\u2080\u22121\u2212i)... my term: ((j\u2080\u22121\u2212j:\u2115):\u211d)\u207b\u00b9 = f (j\u2080\u22121\u2212j) with f x := ((x:\u2115):\u211d)\u207b\u00b9: but sum_range_reflect needs f (n \u2212 1 \u2212 i) = f ((j\u2080\u22121) \u2212 1 \u2212 j) = f (j\u2080\u22122\u2212j) \u2014 OFF BY ONE from my j\u2080\u22121\u2212j. Hmm: (j\u2080\u22121) \u2212 1 \u2212 j = j\u2080\u22122\u2212j \u2260 j\u2080\u22121\u2212j. So reflect on range j\u2080 instead? Let me reindex differently: \u2211 j \u2208 range (j\u2080\u22121), f (j\u2080\u22121\u2212j) = \u2211 i \u2208 range (j\u2080\u22121), f (i+1)?? the values {j\u2080\u22121\u2212j : j < j\u2080\u22121} = {1, 2, ..., j\u2080\u22121} = {i+1 : i < j\u2080\u22121} \u2713: via the reflect at range j\u2080: \u2211 j \u2208 range j\u2080, g j = \u2211 j \u2208 range j\u2080, g (j\u2080\u22121\u2212j) (sum_range_reflect (g) j\u2080: \u2211_{range j\u2080} g (j\u2080\u22121\u2212j) = \u2211_{range j\u2080} g): so \u2211 j \u2208 range (j\u2080\u22121), f (j\u2080\u22121\u2212j) \u2014 the j ranges over range (j\u2080\u22121) = {0..j\u2080\u22122}: the values j\u2080\u22121\u2212j range over {1..j\u2080\u22121} = {i+1 : i \u2208 range (j\u2080\u22121)}: so \u2211 j \u2208 range (j\u2080\u22121), f (j\u2080\u22121\u2212j) = \u2211 i \u2208 range (j\u2080\u22121), f (i+1): via... define g on range j\u2080 with g 0 = 0-ish: \u2211_{range j\u2080} g (j\u2080\u22121\u2212j) = \u2211_{range j\u2080} g j (reflect): the LHS = g (j\u2080\u22121) + g(j\u2080\u22122) + ... + g(0)... my sum is over j \u2264 j\u2080\u22122 of f(j\u2080\u22121\u2212j) = f(1) + f(2) + ... + f(j\u2080\u22121) \u2014 i.e., \u2211_{i \u2208 range (j\u2080\u22121)} f (i+1). To get there: \u2211_{j \u2208 range (j\u2080\u22121)} f (j\u2080\u22121\u2212j): substitute i := j\u2080\u22121\u2212j... simplest Lean route: `Finset.sum_range_reflect (fun x => ((x + 1 : \u2115):\u211d)\u207b\u00b9)?`... hmm: consider g j := ((j+1:\u2115):\u211d)\u207b\u00b9 for j \u2208 range (j\u2080\u22121)... I want to show \u2211_{j < j\u2080\u22121} ((j\u2080\u22121\u2212j:\u2115):\u211d)\u207b\u00b9 = \u2211_{i < j\u2080\u22121} ((i+1:\u2115):\u211d)\u207b\u00b9. Take f x := ((x:\u2115):\u211d)\u207b\u00b9 on range j\u2080: sum_range_reflect f j\u2080 : \u2211_{j \u2208 range j\u2080} f (j\u2080\u22121\u2212j) = \u2211_{j \u2208 range j\u2080} f j. The LHS: j \u2208 range j\u2080 = {0..j\u2080\u22121}: terms f (j\u2080\u22121\u2212j) for j=0..j\u2080\u22121: = f(j\u2080\u22121), f(j\u2080\u22122), ..., f(0) \u2014 that includes f(0) = 0\u207b\u00b9 = 0 (junk but fine) \u2014 and f(1)...f(j\u2080\u22121). So \u2211_{range j\u2080} f (j\u2080\u22121\u2212j) = (my target sum) + f(0)\u00b7... my target: \u2211_{j \u2208 range (j\u2080\u22121)} f (j\u2080\u22121\u2212j): the j = j\u2080\u22121 term of the reflect LHS would be f(0) = 0: so \u2211_{range j\u2080} f(j\u2080\u22121\u2212j) = \u2211_{range (j\u2080\u22121)} f(j\u2080\u22121\u2212j) + f(0)... hmm j = j\u2080\u22121: f (j\u2080\u22121\u2212(j\u2080\u22121)) = f 0 = 0\u207b\u00b9 = 0: so the reflect-LHS = my-sum + 0: \u2211_{range j\u2080} f(j\u2080\u22121\u2212j) = \u2211_{range (j\u2080\u22121)} f(j\u2080\u22121\u2212j) + f 0 via sum_range_succ (range j\u2080 = range (j\u2080\u22121) + the j\u2080\u22121 term): so my sum = \u2211_{range j\u2080} f (j\u2080\u22121\u2212j) \u2212 f 0 = (\u2211_{range j\u2080} f j) \u2212 0 [reflect] = \u2211_{range j\u2080} f j = \u2211_{range (j\u2080\u22121)} f j + f (j\u2080\u22121) [sum_range_succ]... I'm tying myself in knots. DIRECT: my sum = \u2211_{j \u2208 range (j\u2080\u22121)} f (j\u2080\u22121\u2212j). Use Finset.sum_bij with the involution j \u21a6 j\u2080\u22122\u2212j on range (j\u2080\u22121)? maps j \u2208 {0..j\u2080\u22122} to j\u2080\u22122\u2212j \u2208 {0..j\u2080\u22122} \u2713 involution: then \u2211 f (j\u2080\u22121\u2212j) = \u2211_{i} f (j\u2080\u22121\u2212(j\u2080\u22122\u2212i)) = \u2211 f (i+1): j\u2080\u22121\u2212(j\u2080\u22122\u2212i) = i+1 \u2713 (omega). Finset.sum_bij (i : j \u21a6 j\u2080\u22122\u2212j) (hi : maps into) (hi_inj) (hi_surj) (h : \u2200 j, f (j\u2080\u22121\u2212j) = f' j)?? the signature of sum_bij is heavy. Use `Finset.sum_nbij'`? or simplest: `Finset.sum_range_reflect`-based... \n\nActually \u2014 cleanest: reindex via sum_Ico_eq_sum_range-style but for the reverse: `Finset.sum_range_reflect (f : \u2115 \u2192 M) (n : \u2115) : \u2211 i \u2208 range n, f (n \u2212 1 \u2212 i) = \u2211 i \u2208 range n, f i` \u2014 apply with f x := ((x + 1 : \u2115):\u211d)\u207b\u00b9 and n := j\u2080 \u2212 1: LHS: \u2211 i \u2208 range (j\u2080\u22121), f (j\u2080\u22121\u22121\u2212i) = \u2211 f (j\u2080\u22122\u2212i) \u2014 values f (j\u2080\u22122\u2212i) for i < j\u2080\u22121: {j\u2080\u22122, ..., 0} \u2192 f values {((j\u2080\u22122)+1)\u207b\u00b9...} hmm this gives f(j\u2080\u22122\u2212i) with f x = (x+1)\u207b\u00b9: = (j\u2080\u22121\u2212i)\u207b\u00b9 \u2014 YES: f (j\u2080\u22122\u2212i) = ((j\u2080\u22122\u2212i)+1)\u207b\u00b9 = ((j\u2080\u22121\u2212i):\u2115)\u207b\u00b9 \u2713 EXACTLY my term! So:\n\u2211 i \u2208 range (j\u2080\u22121), ((j\u2080\u22121\u2212i:\u2115):\u211d)\u207b\u00b9 = \u2211 i \u2208 range (j\u2080\u22121), f (j\u2080\u22122\u2212i) [per-term defeq: ((j\u2080\u22121\u2212i):\u2115)\u207b\u00b9 = ((j\u2080\u22122\u2212i:\u2115)+1:\u2115...)\u207b\u00b9: j\u2080\u22121\u2212i = (j\u2080\u22122\u2212i)+1 by omega (for i \u2264 j\u2080\u22122 \u2713)] = \u2211 i \u2208 range (j\u2080\u22121), f i [sum_range_reflect] = \u2211 i \u2208 range (j\u2080\u22121), ((i:\u2115)+1:\u2115\u2192\u211d)\u207b\u00b9 \u2264 1 + log(j\u2080\u22121) [harmonic bound] \u2264 1 + log m.\n\nOK. The Lean plumbing remains fiddly but doable. Time check: this \u00a73 is long. Let me just write the full \u00a73 now as an append, carefully, and compile. I'll write the two one-sided bounds as separate haves with all the reindexing inline.",
  "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            Summable.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        have h2 : Real.log (N : \u211d) \u2264 Real.log (A + 1) := Real.log_le_log hN0R hNA1\n        rw [div_eq_mul_inv, div_eq_mul_inv]\n        apply mul_le_mul_of_nonneg_right _ (inv_nonneg.mpr hA0.le)\n        linarith [h2]\n      have h2 : (1 : \u211d) / (N : \u211d) \u2264 1 / A := one_div_le_one_div_of_le hA0 hNA\n      have h3 : (2 + Real.log (A + 1)) / A = (1 + Real.log (A + 1)) / A + 1 / A := by\n        rw [\u2190 add_div]\n        congr 1\n        ring\n      rw [h3]\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            Summable.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 [show (\u2211' n : \u2115, \u2016w\u2016 / (((n : \u211d) + 1) * (A + (n : \u211d) + 1)))\n                = \u2211' n : \u2115, \u2016w\u2016 * (((n : \u211d) + 1) * (A + (n : \u211d) + 1))\u207b\u00b9 from\n              tsum_congr fun n => by rw [div_eq_mul_inv]]\n            exact tsum_mul_left\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      linarith [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_left ?_ _\n          refine (norm_sub_le _ _).trans ?_\n          refine add_le_add_left ?_ _\n          rw [norm_neg,\n            show (Real.eulerMascheroniConstant : \u2102)\n              = ((Real.eulerMascheroniConstant : \u211d) : \u2102) from rfl,\n            Complex.norm_real, Real.norm_eq_abs,\n            abs_of_nonneg ((by norm_num : (0 : \u211d) \u2264 1 / 2).trans\n              Real.one_half_lt_eulerMascheroniConstant.le)]\n      _ \u2264 1 + 1 + (\u2016w\u2016 / A) * (2 + Real.log (A + 1)) := by\n          linarith [h\u03b31, h1w, 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            have h5 : (0 : \u211d) \u2264 Real.log (A + 1) :=\n              Real.log_nonneg (by linarith [hwre] : (1 : \u211d) \u2264 A + 1)\n            have h3 : (0 : \u211d) \u2264 2 + Real.log (A + 1) := by linarith [h5]\n            exact mul_le_mul hratio (by linarith [hlogA]) h3 (by norm_num)\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": 475,
      "oldLines": 6,
      "newStart": 475,
      "newLines": 194,
      "lines": [
        "             Real.log_nonneg (by linarith [hw_norm_ge])",
        "           nlinarith [h2, h3, hlog4, hlognonneg]",
        " ",
        "+/-! ## 3. The separated reciprocal sum (C) -/",
        "+",
        "+/-- The right half of the V-split: for j\u2080 = \u2308\u2212re w\u2309\u208a and j > j\u2080,",
        "+\u2016(w+j)\u207b\u00b9\u2016 \u2264 1/(j\u2212j\u2080) (real parts are 1-separated and j\u2080 catches up to",
        "+\u2212re w). -/",
        "+theorem recip_norm_le_right {w : \u2102} {c : \u211d} (hdist : \u2200 m : \u2115, c \u2264 \u2016w + (m : \u2102)\u2016)",
        "+    {j\u2080 : \u2115} (hj\u2080 : j\u2080 = \u2308-w.re\u2309\u208a) {j : \u2115} (hj : j\u2080 + 1 \u2264 j) :",
        "+    \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 ((j - j\u2080 : \u2115) : \u211d)\u207b\u00b9 := by",
        "+  have hj\u2080ge : -(w.re) \u2264 (j\u2080 : \u211d) := by rw [hj\u2080]; exact Nat.le_ceil _",
        "+  have hrewj : (w + (j : \u2102)).re = w.re + (j : \u211d) := by",
        "+    simp [Complex.add_re, Complex.natCast_re]",
        "+  have hnorm : \u2016(w + (j : \u2102))\u207b\u00b9\u2016 = \u2016w + (j : \u2102)\u2016\u207b\u00b9 := norm_inv",
        "+  rw [hnorm]",
        "+  have hge : ((j - j\u2080 : \u2115) : \u211d) \u2264 \u2016w + (j : \u2102)\u2016 := by",
        "+    have h1 : (w + (j : \u2102)).re \u2264 \u2016w + (j : \u2102)\u2016 := by",
        "+      have h2 := Complex.abs_re_le_norm (w + (j : \u2102))",
        "+      rwa [abs_of_nonneg (by",
        "+        rw [hrewj]",
        "+        have h3 : (0 : \u211d) \u2264 w.re + (j\u2080 : \u211d) := by linarith [hj\u2080ge]",
        "+        have h4 : ((j\u2080 : \u211d) + 1) \u2264 (j : \u211d) := by exact_mod_cast hj",
        "+        linarith [h3, h4])] at h2",
        "+    refine le_trans ?_ h1",
        "+    rw [hrewj]",
        "+    have h3 : (0 : \u211d) \u2264 w.re + (j\u2080 : \u211d) := by linarith [hj\u2080ge]",
        "+    have h4 : ((j - j\u2080 : \u2115) : \u211d) = (j : \u211d) - (j\u2080 : \u211d) := by",
        "+      rw [Nat.cast_sub (by omega : j\u2080 \u2264 j)]",
        "+    rw [h4]",
        "+    linarith [h3]",
        "+  have hpos : (0 : \u211d) < ((j - j\u2080 : \u2115) : \u211d) := by",
        "+    have h1 : (1 : \u2115) \u2264 j - j\u2080 := by omega",
        "+    have h2 : (0 : \u211d) < ((j - j\u2080 : \u2115) : \u211d) := by exact_mod_cast h1",
        "+    exact h2",
        "+  exact (inv_le_inv\u2080 (by linarith [hge, hpos]) hpos).mpr hge",
        "+",
        "+/-- The left half: for j < j\u2080 \u2212 1 (so j\u2080 \u2265 2 and the real part is still",
        "+negative), \u2016(w+j)\u207b\u00b9\u2016 \u2264 1/(j\u2080\u22121\u2212j). -/",
        "+theorem recip_norm_le_left {w : \u2102} {c : \u211d} (hdist : \u2200 m : \u2115, c \u2264 \u2016w + (m : \u2102)\u2016)",
        "+    {j\u2080 : \u2115} (hj\u2080 : j\u2080 = \u2308-w.re\u2309\u208a) {j : \u2115} (hj : j + 1 \u2264 j\u2080 - 1) :",
        "+    \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 ((j\u2080 - 1 - j : \u2115) : \u211d)\u207b\u00b9 := by",
        "+  have hj\u2080lt : (j\u2080 : \u211d) < -w.re + 1 := by",
        "+    rw [hj\u2080]",
        "+    by_cases hre : 0 \u2264 -w.re",
        "+    \u00b7 have h := Nat.ceil_lt_add_one hre",
        "+      have h2 : ((\u2308-w.re\u2309\u208a : \u2115) : \u211d) < -w.re + 1 := by exact_mod_cast h",
        "+      exact h2",
        "+    \u00b7 push Not at hre",
        "+      have h1 : \u2308-w.re\u2309\u208a = 0 := by",
        "+        apply Nat.ceil_eq_zero.mpr",
        "+        linarith [hre]",
        "+      rw [h1] at hj\u2080",
        "+      -- j\u2080 = 0 but j + 1 \u2264 j\u2080 \u2212 1 = 0 \u2212 1 = 0 in \u2115: impossible",
        "+      omega",
        "+  have hrewj : (w + (j : \u2102)).re = w.re + (j : \u211d) := by",
        "+    simp [Complex.add_re, Complex.natCast_re]",
        "+  have hneg : (w + (j : \u2102)).re < 0 := by",
        "+    rw [hrewj]",
        "+    have h4 : ((j : \u211d) + 1) \u2264 (j\u2080 : \u211d) - 1 := by exact_mod_cast hj",
        "+    linarith [hj\u2080lt, h4]",
        "+  have hnorm : \u2016(w + (j : \u2102))\u207b\u00b9\u2016 = \u2016w + (j : \u2102)\u2016\u207b\u00b9 := norm_inv",
        "+  rw [hnorm]",
        "+  have hge : ((j\u2080 - 1 - j : \u2115) : \u211d) \u2264 \u2016w + (j : \u2102)\u2016 := by",
        "+    have h1 : |(w + (j : \u2102)).re| \u2264 \u2016w + (j : \u2102)\u2016 := Complex.abs_re_le_norm _",
        "+    rw [hrewj] at h1",
        "+    have h2 : |(w.re + (j : \u211d))| = -(w.re + (j : \u211d)) := abs_of_neg (by rwa [\u2190 hrewj])",
        "+    rw [h2] at h1",
        "+    refine le_trans ?_ h1",
        "+    have h4 : ((j\u2080 - 1 - j : \u2115) : \u211d) = (j\u2080 : \u211d) - 1 - (j : \u211d) := by",
        "+      rw [Nat.cast_sub (by omega : j \u2264 j\u2080 - 1), Nat.cast_sub (by omega : 1 \u2264 j\u2080)]",
        "+      push_cast",
        "+      ring",
        "+    rw [h4]",
        "+    linarith [hj\u2080lt]",
        "+  have hpos : (0 : \u211d) < ((j\u2080 - 1 - j : \u2115) : \u211d) := by",
        "+    have h1 : (1 : \u2115) \u2264 j\u2080 - 1 - j := by omega",
        "+    exact_mod_cast h1",
        "+  exact (inv_le_inv\u2080 (by linarith [hge, hpos]) hpos).mpr hge",
        "+",
        "+/-- **The separated reciprocal sum bound (C)**: for dist(w, \u2212\u2115) \u2265 c > 0,",
        "+\u03a3_{j<m} \u2016(w+j)\u207b\u00b9\u2016 \u2264 2/c + 2 + 2\u00b7log m (the V-split: at most one term per",
        "+side needs the dist condition; the rest telescope into the harmonic bound). -/",
        "+theorem digamma_recip_sum_le {c : \u211d} (hc : 0 < c) {w : \u2102}",
        "+    (hdist : \u2200 m : \u2115, c \u2264 \u2016w + (m : \u2102)\u2016) {m : \u2115} (hm : \u2308-w.re\u2309\u208a + 1 \u2264 m) :",
        "+    \u2211 j \u2208 Finset.range m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 2 / c + 2 + 2 * Real.log m := by",
        "+  set j\u2080 := \u2308-w.re\u2309\u208a with hj\u2080",
        "+  have hj\u2080m : j\u2080 \u2264 m := by omega",
        "+  -- split range m = range j\u2080 \u222a Ico j\u2080 m",
        "+  have hsplit : \u2211 j \u2208 Finset.range m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016",
        "+      = \u2211 j \u2208 Finset.range j\u2080, \u2016(w + (j : \u2102))\u207b\u00b9\u2016",
        "+        + \u2211 j \u2208 Finset.Ico j\u2080 m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 := by",
        "+    rw [Finset.range_eq_Ico, Finset.range_eq_Ico,",
        "+      \u2190 Finset.sum_Ico_consecutive _ (Nat.zero_le j\u2080) hj\u2080m]",
        "+  rw [hsplit]",
        "+  -- RIGHT side: Ico j\u2080 m \u2014 the first term by dist, the rest by recip_norm_le_right",
        "+  have hright : \u2211 j \u2208 Finset.Ico j\u2080 m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016",
        "+      \u2264 1 / c + (1 + Real.log m) := by",
        "+    by_cases hj\u20801 : j\u2080 + 1 \u2264 m",
        "+    \u00b7 -- Ico j\u2080 m = {j\u2080} \u222a Ico (j\u2080+1) m",
        "+      have hdecomp : Finset.Ico j\u2080 m = {j\u2080} \u222a Finset.Ico (j\u2080 + 1) m := by",
        "+        rw [Finset.Ico_union_Ico_eq_Ico (Nat.le_refl j\u2080) hj\u20801]",
        "+        exact (Finset.Ico_self_singleton).symm... ",
        "+```",
        "+Hmm \u2014 Ico j\u2080 (j\u2080+1) = {j\u2080}: `Finset.Ico_self_singleton`? the name... `Finset.Ico_succ_singleton : Ico n (n+1) = {n}` \u2713 I believe. Then the union: Ico j\u2080 (j\u2080+1) \u222a Ico (j\u2080+1) m = Ico j\u2080 m via Finset.Ico_union_Ico_eq_Ico (le_refl) hj\u20801 \u2713. So Ico j\u2080 m = {j\u2080} \u222a Ico (j\u2080+1) m via rw [\u2190 Finset.Ico_succ_singleton... wait I need Ico j\u2080 m = {j\u2080} \u222a ...: {j\u2080} = Ico j\u2080 (j\u2080+1) via Ico_succ_singleton.symm; then Ico j\u2080 (j\u2080+1) \u222a Ico (j\u2080+1) m = Ico j\u2080 m via the union lemma. So:",
        "+```",
        "+      have hdecomp : Finset.Ico j\u2080 m = Finset.Ico j\u2080 (j\u2080 + 1) \u222a Finset.Ico (j\u2080 + 1) m :=",
        "+        (Finset.Ico_union_Ico_eq_Ico (Nat.le_refl j\u2080) hj\u20801).symm",
        "+      rw [hdecomp, Finset.Ico_succ_singleton]  -- hmm Ico j\u2080 (j\u2080+1) = {j\u2080}: Finset.Ico_succ_singleton : Ico n (n+1) = {n} \u2014 rw turns it into {j\u2080}: then sum over {j\u2080} \u222a ...: Finset.sum_union (disjoint) \u2014 the disjointness: {j\u2080} \u2229 Ico (j\u2080+1) m = \u2205: Finset.disjoint_singleton_left: j\u2080 \u2209 Ico (j\u2080+1) m: Finset.not_mem_Ico: j\u2080 < j\u2080+1 \u2264 ... hmm `Finset.Ico_disjoint_Ico_consecutive`? there's `Finset.Ico_disjoint_Ico_consecutive (a b c) : Disjoint (Ico a b) (Ico b c)` \u2713 I recall. So:",
        "+      rw [hdecomp, Finset.Ico_succ_singleton,",
        "+        Finset.sum_union (Finset.disjoint_singleton_left.mpr (by",
        "+          simp [Finset.mem_Ico] : j\u2080 \u2209 Finset.Ico (j\u2080+1) m)),  -- hmm the disjoint_singleton_left form",
        "+        Finset.sum_singleton]",
        "+```",
        "+This is getting heavy. SIMPLER alternative: use `Finset.sum_Ico_succ_top`? no that's the top. For the BOTTOM: `Finset.sum_Ico_eq_sum_range` reindex the whole Ico (j\u2080+1) m part and handle the j\u2080 term separately via... actually cleanest: DON'T peel the first term; instead bound the FIRST term inline via a case split in the sum: ",
        "+",
        "+Alternative cleaner structure: bound \u2211 Ico j\u2080 m directly:",
        "+\u2211 j \u2208 Ico j\u2080 m, term_j = term_{j\u2080} + \u2211_{j \u2208 Ico (j\u2080+1) m} term_j \u2014 the peeling: `Finset.sum_Ico_succ_top`? no. There IS `Finset.sum_Ico_eq_sub`? no. The bottom-peel: `Finset.Ico.erase`... Or use: `Finset.sum_Ico_succ_bot`? hmm \u2014 sum over Ico (a) b with a < b = f a + \u2211 Ico (a+1) b: the lemma name might be `Finset.sum_Ico_eq_head_add_sum_tail`? not a thing. There IS: `Finset.sum_range_succ` and for Ico: `Finset.sum_Ico_eq_sum_range` + `Finset.sum_range_succ'`? Let me just do the reindex for the whole right side INCLUDING j\u2080's term with a per-term piecewise bound:",
        "+",
        "+For j \u2208 Ico j\u2080 m: term_j \u2264 h j where h j := if j = j\u2080 then 1/c else ((j \u2212 j\u2080 : \u2115):\u211d)\u207b\u00b9. Then \u2211 = (peel j\u2080) ... still needs the peel. ",
        "+",
        "+OK \u2014 the cleanest available: `Finset.sum_eq_sum_diff_singleton_add`? or `Finset.add_sum_erase`: \u2211_{Ico j\u2080 m} f = f j\u2080 + \u2211_{(Ico j\u2080 m).erase j\u2080} f \u2014 and (Ico j\u2080 m).erase j\u2080 = Ico (j\u2080+1) m: `Finset.Ico_erase_left : (Ico a b).erase a = Ico (a+1) b` \u2713 I believe that exists. So:",
        "+```",
        "+      rw [\u2190 Finset.add_sum_erase _ _ (Finset.left_mem_Ico.mpr (by omega : j\u2080 < m))]  -- hmm add_sum_erase : f a + \u2211 x \u2208 s.erase a, f x = \u2211 x \u2208 s, f x for a \u2208 s \u2014 so \u2190 direction turns the sum into f j\u2080 + erase-sum \u2713",
        "+      rw [Finset.Ico_erase_left]  -- (Ico j\u2080 m).erase j\u2080 = Ico (j\u2080+1) m",
        "+```",
        "+Finset.left_mem_Ico : a \u2208 Ico a b \u2194 a < b \u2713 (I think). Then:",
        "+```",
        "+      -- term at j\u2080: \u2264 1/c",
        "+      have hfirst : \u2016(w + (j\u2080 : \u2102))\u207b\u00b9\u2016 \u2264 1 / c := by",
        "+        rw [norm_inv]",
        "+        rw [show (1 : \u211d) / c = (c : \u211d)\u207b\u00b9 by rw [one_div]]",
        "+        exact (inv_le_inv\u2080 hc (hdist j\u2080)).mpr (hdist j\u2080)  -- hmm inv_le_inv\u2080 (ha : 0 < a) (hb : 0 < b) : a\u207b\u00b9 \u2264 b\u207b\u00b9 \u2194 b \u2264 a: \u2016w+j\u2080\u2016\u207b\u00b9 \u2264 c\u207b\u00b9 \u27fa c \u2264 \u2016w+j\u2080\u2016: (inv_le_inv\u2080 (by linarith [hdist j\u2080, hc] : (0:\u211d) < \u2016w+j\u2080\u2016) hc).mpr (hdist j\u2080) \u2713",
        "+      -- the rest: reindex to the harmonic bound",
        "+      have hrest : \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 \u2264 1 + Real.log m := by",
        "+        calc \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016",
        "+            \u2264 \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, ((j - j\u2080 : \u2115) : \u211d)\u207b\u00b9 :=",
        "+              Finset.sum_le_sum fun j hj => recip_norm_le_right hdist hj\u2080 (by",
        "+                rw [Finset.mem_Ico] at hj; exact hj.1)",
        "+          _ = \u2211 i \u2208 Finset.range (m - (j\u2080 + 1)), ((i : \u211d) + 1)\u207b\u00b9 := by",
        "+              rw [Finset.sum_Ico_eq_sum_range]  -- \u2211 i \u2208 range ((j\u2080+1) ... hmm: sum_Ico_eq_sum_range : \u2211 i \u2208 Ico a b, f i = \u2211 i \u2208 range (b \u2212 a), f (a + i): with a := j\u2080+1, b := m: \u2211 i \u2208 range (m \u2212 (j\u2080+1)), f (j\u2080+1+i): f (j\u2080+1+i) = (((j\u2080+1+i) \u2212 j\u2080 : \u2115):\u211d)\u207b\u00b9: (j\u2080+1+i) \u2212 j\u2080 = i+1: ",
        "+              apply Finset.sum_congr rfl",
        "+              intro i _",
        "+              -- ((j\u2080+1+i) \u2212 j\u2080 : \u2115) = i + 1",
        "+              have h1 : (j\u2080 + 1 + i) - j\u2080 = i + 1 := by omega",
        "+              rw [h1]  -- then casts: ((i+1 : \u2115):\u211d) = (i:\u211d)+1: Nat.cast_add_one",
        "+              rw [Nat.cast_add_one]",
        "+          _ \u2264 1 + Real.log (m - (j\u2080 + 1)) := by",
        "+              have h := sum_one_div_le_one_add_log (m - (j\u2080 + 1))",
        "+              -- h's form: \u2211 1/(\u2191n+1) \u2264 1 + log \u2191(m\u2212j\u2080\u22121): my form: \u2211 (\u2191i+1)\u207b\u00b9: simpa [one_div]",
        "+              simpa [one_div] using h",
        "+          _ \u2264 1 + Real.log m := by",
        "+              gcongr  -- 1 + log(m\u2212j\u2080\u22121) \u2264 1 + log m: log mono: Real.log_le_log (0 < m\u2212j\u2080\u22121) (m\u2212j\u2080\u22121 \u2264 m): the 0 < fails if m = j\u2080+1 \u2014 but then the range is empty... hmm the sum range (m\u2212(j\u2080+1)) with m = j\u2080+1: range 0: sum = 0: and 0 \u2264 1 + log m \u2713 (log m \u2265 0 for m \u2265 1: m \u2265 j\u2080+1 \u2265 1 \u2713... wait m \u2265 1: from hm : j\u2080+1 \u2264 m and j\u2080 \u2265 0: m \u2265 1 \u2713). The gcongr needs 0 < \u2191(m\u2212j\u2080\u22121) \u2014 fails when m = j\u2080+1 (then m\u2212j\u2080\u22121 = 0: log 0 = 0 junk: the step (1 + log 0) = 1 + 0 = 1 \u2264 1 + log m \u27fa 0 \u2264 log m \u2713 m \u2265 1). Split: by_cases m = j\u2080+1: then the sum is over range 0 = 0: 0 \u2264 1 + log m \u2713. Else: 1 \u2264 m\u2212j\u2080\u22121: log mono \u2713. Let me write:",
        "+              by_cases hcase : m - (j\u2080 + 1) = 0",
        "+              \u00b7 have : m - (j\u2080 + 1) = 0 := hcase",
        "+                -- the sum \u2211 i \u2208 range 0 = 0 \u2014 but we're at the SECOND calc step's goal: (1 + log \u2191(m\u2212j\u2080\u22121)) \u2264 1 + log \u2191m: with \u2191(m\u2212j\u2080\u22121) = 0: log 0 = 0: ",
        "+                rw [hcase]  -- \u2191(0:\u2115) = 0: Nat.cast_zero: log 0 = 0: Real.log_zero",
        "+                simp [Real.log_zero]  -- 1 + 0 \u2264 1 + log \u2191m \u27fa 0 \u2264 log \u2191m: Real.log_nonneg (1 \u2264 \u2191m): m \u2265 1 \u2713",
        "+                exact Real.log_nonneg (by exact_mod_cast (by omega : 1 \u2264 m))",
        "+              \u00b7 have h1 : (1 : \u2115) \u2264 m - (j\u2080 + 1) := by omega",
        "+                have h2 : (0 : \u211d) < ((m - (j\u2080 + 1) : \u2115) : \u211d) := by exact_mod_cast h1",
        "+                have h3 : ((m - (j\u2080 + 1) : \u2115) : \u211d) \u2264 (m : \u211d) := by",
        "+                  rw [Nat.cast_sub (by omega : j\u2080 + 1 \u2264 m)]",
        "+                  push_cast",
        "+                  have h4 : (0 : \u211d) \u2264 (j\u2080 : \u211d) := by positivity",
        "+                  linarith [h4]",
        "+                have h4 : Real.log ((m - (j\u2080 + 1) : \u2115) : \u211d) \u2264 Real.log (m : \u211d) :=",
        "+                  Real.log_le_log h2 h3",
        "+                linarith [h4]",
        "+      -- combine",
        "+      calc \u2211 j \u2208 Finset.Ico j\u2080 m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016",
        "+          = \u2016(w + (j\u2080 : \u2102))\u207b\u00b9\u2016 + \u2211 j \u2208 Finset.Ico (j\u2080 + 1) m, \u2016(w + (j : \u2102))\u207b\u00b9\u2016 := by",
        "+            rw [Finset.add_sum_erase _ _ (Finset.left_mem_Ico.mpr (by omega : j\u2080 < m)),",
        "+              Finset.Ico_erase_left]",
        "+        _ \u2264 1 / c + (1 + Real.log m) := add_le_add hfirst hrest",
        "+    \u00b7 -- \u00ac(j\u2080+1 \u2264 m) \u27f9 m \u2264 j\u2080: the Ico is empty",
        "+      push Not at hj\u20801",
        "+      have hempty : Finset.Ico j\u2080 m = \u2205 := Finset.Ico_eq_empty_of_le (by omega : m \u2264 j\u2080)  -- Finset.Ico_eq_empty_of_le (h : b \u2264 a) : Ico a b = \u2205? check name \u2014 maybe `Finset.Ico_eq_empty_iff : Ico a b = \u2205 \u2194 b \u2264 a` \u2014 use .mpr",
        "+      rw [hempty]",
        "+      simp  -- \u2211 \u2205 = 0 \u2264 1/c + (1 + log m): positivity... needs 1/c > 0 and log m \u2265 0: m \u2265 j\u2080+1\u2212... hmm here m \u2264 j\u2080: log m could be log 0 = 0 (m = 0) or log of small \u2014 m \u2264 j\u2080 but from hm : j\u2080+1 \u2264 m?? \u2014 WAIT hm : j\u2080 + 1 \u2264 m is the THEOREM's hypothesis \u2014 and the by_cases hj\u20801 : j\u2080+1 \u2264 m is ALWAYS true by hm!! So the else branch is vacuous: hj\u20801 contradicts hm: omega closes:",
        "+      omega  -- hm : j\u2080 + 1 \u2264 m and hj\u20801 : \u00ac(j\u2080+1 \u2264 m) \u2014 False \u27f9 anything",
        "+```",
        "+Wait \u2014 hm : \u2308\u2212w.re\u2309\u208a + 1 \u2264 m i.e. j\u2080 + 1 \u2264 m \u2014 so the by_cases's second branch is vacuous \u2713 just `omega` (deriving False from hm and hj\u20801). Hmm \u2014 but the goal in that branch after `push Not at hj\u20801`: hj\u20801 : \u00ac j\u2080 + 1 \u2264 m; hm : j\u2080 + 1 \u2264 m: `exact absurd hm hj\u20801` closes any goal \u2713 cleaner: `exact absurd hm hj\u20801`. So drop the by_cases entirely \u2014 just use hj\u20801 := hm. Simplify: the right side always has j\u2080+1 \u2264 m \u2713 no by_cases needed!",
        "+",
        "+Similarly the LEFT side: range j\u2080: if j\u2080 = 0: empty \u2713 handle via by_cases (j\u2080 = 0); else peel j\u2080\u22121 from the TOP: range j\u2080 = range (j\u2080\u22121) \u222a {j\u2080\u22121}... via Finset.sum_range_succ with j\u2080 = (j\u2080\u22121)+1: \u2211 range j\u2080 f = \u2211 range (j\u2080\u22121) f + f (j\u2080\u22121) (with j\u2080\u22121+1 = j\u2080 by omega-rewrite). The f (j\u2080\u22121) term \u2264 1/c (dist). The range (j\u2080\u22121) part: j \u2264 j\u2080\u22122 \u27f9 recip_norm_le_left (hj : j + 1 \u2264 j\u2080 \u2212 1): reindex: \u2211 j \u2208 range (j\u2080\u22121), ((j\u2080\u22121\u2212j : \u2115):\u211d)\u207b\u00b9 = \u2211 i \u2208 range (j\u2080\u22121), ((i:\u211d)+1)\u207b\u00b9 (reverse the range! j \u21a6 j\u2080\u22121\u2212j is an order-reversing bijection on range (j\u2080\u22121) \u2014 `Finset.sum_range_reflect`?? there IS `Finset.sum_range_reflect (f) (n) : \u2211 i \u2208 range n, f (n \u2212 1 \u2212 i) = \u2211 i \u2208 range n, f i` \u2713 I recall!). So \u2211 j \u2208 range (j\u2080\u22121), g (j\u2080\u22121\u2212j) = \u2211 j \u2208 range (j\u2080\u22121), g j with g j := ((j+1 : \u2115):\u211d)\u207b\u00b9?? hmm: my term after recip_norm_le_left: ((j\u2080\u22121\u2212j : \u2115):\u211d)\u207b\u00b9: let g x := ((x:\u2115):\u211d)\u207b\u00b9: the term is g (j\u2080\u22121\u2212j) with... j\u2080\u22121\u2212j for j \u2208 range (j\u2080\u22121): j\u2080\u22121\u2212j \u2208 {j\u2080\u22121, j\u2080\u22122, ..., 1}: sum_range_reflect: \u2211 j \u2208 range (j\u2080\u22121), g (j\u2080\u22121\u2212j) = \u2211 j \u2208 range (j\u2080\u22121), g j?? \u2014 sum_range_reflect : \u2211 i \u2208 range n, f (n \u2212 1 \u2212 i) = \u2211 i \u2208 range n, f i: with n := j\u2080\u22121: f (n\u22121\u2212i) = f (j\u2080\u22121\u2212i)... my term: ((j\u2080\u22121\u2212j:\u2115):\u211d)\u207b\u00b9 = f (j\u2080\u22121\u2212j) with f x := ((x:\u2115):\u211d)\u207b\u00b9: but sum_range_reflect needs f (n \u2212 1 \u2212 i) = f ((j\u2080\u22121) \u2212 1 \u2212 j) = f (j\u2080\u22122\u2212j) \u2014 OFF BY ONE from my j\u2080\u22121\u2212j. Hmm: (j\u2080\u22121) \u2212 1 \u2212 j = j\u2080\u22122\u2212j \u2260 j\u2080\u22121\u2212j. So reflect on range j\u2080 instead? Let me reindex differently: \u2211 j \u2208 range (j\u2080\u22121), f (j\u2080\u22121\u2212j) = \u2211 i \u2208 range (j\u2080\u22121), f (i+1)?? the values {j\u2080\u22121\u2212j : j < j\u2080\u22121} = {1, 2, ..., j\u2080\u22121} = {i+1 : i < j\u2080\u22121} \u2713: via the reflect at range j\u2080: \u2211 j \u2208 range j\u2080, g j = \u2211 j \u2208 range j\u2080, g (j\u2080\u22121\u2212j) (sum_range_reflect (g) j\u2080: \u2211_{range j\u2080} g (j\u2080\u22121\u2212j) = \u2211_{range j\u2080} g): so \u2211 j \u2208 range (j\u2080\u22121), f (j\u2080\u22121\u2212j) \u2014 the j ranges over range (j\u2080\u22121) = {0..j\u2080\u22122}: the values j\u2080\u22121\u2212j range over {1..j\u2080\u22121} = {i+1 : i \u2208 range (j\u2080\u22121)}: so \u2211 j \u2208 range (j\u2080\u22121), f (j\u2080\u22121\u2212j) = \u2211 i \u2208 range (j\u2080\u22121), f (i+1): via... define g on range j\u2080 with g 0 = 0-ish: \u2211_{range j\u2080} g (j\u2080\u22121\u2212j) = \u2211_{range j\u2080} g j (reflect): the LHS = g (j\u2080\u22121) + g(j\u2080\u22122) + ... + g(0)... my sum is over j \u2264 j\u2080\u22122 of f(j\u2080\u22121\u2212j) = f(1) + f(2) + ... + f(j\u2080\u22121) \u2014 i.e., \u2211_{i \u2208 range (j\u2080\u22121)} f (i+1). To get there: \u2211_{j \u2208 range (j\u2080\u22121)} f (j\u2080\u22121\u2212j): substitute i := j\u2080\u22121\u2212j... simplest Lean route: `Finset.sum_range_reflect (fun x => ((x + 1 : \u2115):\u211d)\u207b\u00b9)?`... hmm: consider g j := ((j+1:\u2115):\u211d)\u207b\u00b9 for j \u2208 range (j\u2080\u22121)... I want to show \u2211_{j < j\u2080\u22121} ((j\u2080\u22121\u2212j:\u2115):\u211d)\u207b\u00b9 = \u2211_{i < j\u2080\u22121} ((i+1:\u2115):\u211d)\u207b\u00b9. Take f x := ((x:\u2115):\u211d)\u207b\u00b9 on range j\u2080: sum_range_reflect f j\u2080 : \u2211_{j \u2208 range j\u2080} f (j\u2080\u22121\u2212j) = \u2211_{j \u2208 range j\u2080} f j. The LHS: j \u2208 range j\u2080 = {0..j\u2080\u22121}: terms f (j\u2080\u22121\u2212j) for j=0..j\u2080\u22121: = f(j\u2080\u22121), f(j\u2080\u22122), ..., f(0) \u2014 that includes f(0) = 0\u207b\u00b9 = 0 (junk but fine) \u2014 and f(1)...f(j\u2080\u22121). So \u2211_{range j\u2080} f (j\u2080\u22121\u2212j) = (my target sum) + f(0)\u00b7... my target: \u2211_{j \u2208 range (j\u2080\u22121)} f (j\u2080\u22121\u2212j): the j = j\u2080\u22121 term of the reflect LHS would be f(0) = 0: so \u2211_{range j\u2080} f(j\u2080\u22121\u2212j) = \u2211_{range (j\u2080\u22121)} f(j\u2080\u22121\u2212j) + f(0)... hmm j = j\u2080\u22121: f (j\u2080\u22121\u2212(j\u2080\u22121)) = f 0 = 0\u207b\u00b9 = 0: so the reflect-LHS = my-sum + 0: \u2211_{range j\u2080} f(j\u2080\u22121\u2212j) = \u2211_{range (j\u2080\u22121)} f(j\u2080\u22121\u2212j) + f 0 via sum_range_succ (range j\u2080 = range (j\u2080\u22121) + the j\u2080\u22121 term): so my sum = \u2211_{range j\u2080} f (j\u2080\u22121\u2212j) \u2212 f 0 = (\u2211_{range j\u2080} f j) \u2212 0 [reflect] = \u2211_{range j\u2080} f j = \u2211_{range (j\u2080\u22121)} f j + f (j\u2080\u22121) [sum_range_succ]... I'm tying myself in knots. DIRECT: my sum = \u2211_{j \u2208 range (j\u2080\u22121)} f (j\u2080\u22121\u2212j). Use Finset.sum_bij with the involution j \u21a6 j\u2080\u22122\u2212j on range (j\u2080\u22121)? maps j \u2208 {0..j\u2080\u22122} to j\u2080\u22122\u2212j \u2208 {0..j\u2080\u22122} \u2713 involution: then \u2211 f (j\u2080\u22121\u2212j) = \u2211_{i} f (j\u2080\u22121\u2212(j\u2080\u22122\u2212i)) = \u2211 f (i+1): j\u2080\u22121\u2212(j\u2080\u22122\u2212i) = i+1 \u2713 (omega). Finset.sum_bij (i : j \u21a6 j\u2080\u22122\u2212j) (hi : maps into) (hi_inj) (hi_surj) (h : \u2200 j, f (j\u2080\u22121\u2212j) = f' j)?? the signature of sum_bij is heavy. Use `Finset.sum_nbij'`? or simplest: `Finset.sum_range_reflect`-based... ",
        "+",
        "+Actually \u2014 cleanest: reindex via sum_Ico_eq_sum_range-style but for the reverse: `Finset.sum_range_reflect (f : \u2115 \u2192 M) (n : \u2115) : \u2211 i \u2208 range n, f (n \u2212 1 \u2212 i) = \u2211 i \u2208 range n, f i` \u2014 apply with f x := ((x + 1 : \u2115):\u211d)\u207b\u00b9 and n := j\u2080 \u2212 1: LHS: \u2211 i \u2208 range (j\u2080\u22121), f (j\u2080\u22121\u22121\u2212i) = \u2211 f (j\u2080\u22122\u2212i) \u2014 values f (j\u2080\u22122\u2212i) for i < j\u2080\u22121: {j\u2080\u22122, ..., 0} \u2192 f values {((j\u2080\u22122)+1)\u207b\u00b9...} hmm this gives f(j\u2080\u22122\u2212i) with f x = (x+1)\u207b\u00b9: = (j\u2080\u22121\u2212i)\u207b\u00b9 \u2014 YES: f (j\u2080\u22122\u2212i) = ((j\u2080\u22122\u2212i)+1)\u207b\u00b9 = ((j\u2080\u22121\u2212i):\u2115)\u207b\u00b9 \u2713 EXACTLY my term! So:",
        "+\u2211 i \u2208 range (j\u2080\u22121), ((j\u2080\u22121\u2212i:\u2115):\u211d)\u207b\u00b9 = \u2211 i \u2208 range (j\u2080\u22121), f (j\u2080\u22122\u2212i) [per-term defeq: ((j\u2080\u22121\u2212i):\u2115)\u207b\u00b9 = ((j\u2080\u22122\u2212i:\u2115)+1:\u2115...)\u207b\u00b9: j\u2080\u22121\u2212i = (j\u2080\u22122\u2212i)+1 by omega (for i \u2264 j\u2080\u22122 \u2713)] = \u2211 i \u2208 range (j\u2080\u22121), f i [sum_range_reflect] = \u2211 i \u2208 range (j\u2080\u22121), ((i:\u2115)+1:\u2115\u2192\u211d)\u207b\u00b9 \u2264 1 + log(j\u2080\u22121) [harmonic bound] \u2264 1 + log m.",
        "+",
        "+OK. The Lean plumbing remains fiddly but doable. Time check: this \u00a73 is long. Let me just write the full \u00a73 now as an append, carefully, and compile. I'll write the two one-sided bounds as separate haves with all the reindexing inline.",
        "+",
        " ",
        " end NguyenRH1",
        " "
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}