← Session 30 — ii′-5e squeeze capstone + 5f perimeter repair
thinking (241 chars)
The sorry draft is at lines 599–618 (from `rw [← hint]` through the digamma_diff_le sorry). I'll replace lines 599–618 with the complete hbound proof + the complete digamma_diff_le. Let me do the edit with the exact old text (lines 599–618).
Replacing the sorry draft (lines 599–618) with the complete proofs.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean",
"old_string": " rw [\u2190 hint]\n have hbound : \u2200 y \u2208 Set.uIoc (0 : \u211d) 1,\n \u2016((z y)\u207b\u00b9) * ((c : \u211d) : \u2102)\u2016 \u2264 5 / t := by\n intro y hy\n have h1 : \u2016((z y)\u207b\u00b9) * ((c : \u211d) : \u2102)\u2016 = \u2016z y\u2016\u207b\u00b9 * |c| := by\n rw [norm_mul, norm_inv]\n rw [show ((c : \u211d) : \u2102) = (((|c| : \u211d)) : \u2102) * ... ] -- hmm no\n sorry\n sorry\n sorry\n\n/-- **Piece 6** (D-069 \u00a73): the digamma difference\n\u00bd\u2016\u03c8(s/2) \u2212 \u03c8(s\u2080/2)\u2016 \u2264 6/t. Via the +2 shift (re(w+2) \u2265 3/4), Zeta23's\ndigamma_stirling at w+2 and w\u2080, the recurrence \u03c8(w) = \u03c8(w+2) \u2212 w\u207b\u00b9 \u2212\n(w+1)\u207b\u00b9, and the segment-FTC log bound. -/\ntheorem digamma_diff_le {t : \u211d} (ht : 10 \u2264 t) {s : \u2102}\n (h\u03c3lo : -5 / 2 \u2264 s.re) (h\u03c3hi : s.re \u2264 3) (him : s.im = t) :\n \u2016(Complex.digamma (s / 2) - Complex.digamma ((2 + t * Complex.I) / 2)) / 2\u2016\n \u2264 6 / t := by\n sorry\n\nend NguyenRH1\n\nend",
"new_string": " rw [\u2190 hint]\n have hbound : \u2200 y \u2208 Set.\u0399 (0 : \u211d) 1,\n \u2016((z y)\u207b\u00b9) * ((c : \u211d) : \u2102)\u2016 \u2264 5 / t := by\n intro y _\n have hzy : (0 : \u211d) < \u2016z y\u2016 := by\n have h := hznorm y\n positivity\n have h1 : \u2016((z y)\u207b\u00b9) * ((c : \u211d) : \u2102)\u2016 = \u2016z y\u2016\u207b\u00b9 * |c| := by\n rw [norm_mul, norm_inv, Complex.norm_real]\n rw [h1]\n have h2 : \u2016z y\u2016\u207b\u00b9 \u2264 (t / 2)\u207b\u00b9 := by\n rw [inv_le_inv\u2080 hzy (by positivity : (0 : \u211d) < t / 2)]\n exact hznorm y\n calc \u2016z y\u2016\u207b\u00b9 * |c| \u2264 (t / 2)\u207b\u00b9 * (5 / 2) :=\n mul_le_mul h2 hcle (abs_nonneg _) (by positivity)\n _ = 5 / t := by field_simp\n calc \u2016\u222b y in (0 : \u211d)..(1 : \u211d), ((z y)\u207b\u00b9) * ((c : \u211d) : \u2102)\u2016\n \u2264 (5 / t) * |1 - 0| := intervalIntegral.norm_integral_le_of_norm_le_const hbound\n _ = 5 / t := by norm_num [abs_one]\n\n/-- **Piece 6** (D-069 \u00a73): the digamma difference\n\u00bd\u2016\u03c8(s/2) \u2212 \u03c8(s\u2080/2)\u2016 \u2264 6/t. Via the +2 shift (re(w+2) \u2265 3/4), Zeta23's\ndigamma_stirling at w+2 and w\u2080, the recurrence \u03c8(w) = \u03c8(w+2) \u2212 w\u207b\u00b9 \u2212\n(w+1)\u207b\u00b9, and the segment-FTC log bound. -/\ntheorem digamma_diff_le {t : \u211d} (ht : 10 \u2264 t) {s : \u2102}\n (h\u03c3lo : -5 / 2 \u2264 s.re) (h\u03c3hi : s.re \u2264 3) (him : s.im = t) :\n \u2016(Complex.digamma (s / 2) - Complex.digamma ((2 + t * Complex.I) / 2)) / 2\u2016\n \u2264 6 / t := by\n have ht0 : (0 : \u211d) < t := by linarith\n set w : \u2102 := s / 2 with hw\n set w\u2080 : \u2102 := (2 + t * Complex.I) / 2 with hw\u2080\n have hw\u2080eq : w\u2080 = 1 + (t / 2) * Complex.I := by rw [hw\u2080]; ring\n have hwim : w.im = t / 2 := by rw [hw]; simp [him]\n have hw\u2080im : w\u2080.im = t / 2 := by rw [hw\u2080eq]; simp\n have himw : w.im \u2260 0 := by rw [hwim]; positivity\n have hwre : w.re = s.re / 2 := by rw [hw]; simp\n have hw\u2080re : (0 : \u211d) < w\u2080.re := by rw [hw\u2080eq]; simp\n -- the recurrence: \u03c8(w + 2) = \u03c8(w) + w\u207b\u00b9 + (w+1)\u207b\u00b9\n have hrec : Complex.digamma (w + 2) = Complex.digamma w + (w\u207b\u00b9 + (w + 1)\u207b\u00b9) := by\n have h := digamma_add_natCast himw 2\n rw [show w + ((2 : \u2115) : \u2102) = w + 2 by push_cast; ring] at h\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h\n simp only [Nat.cast_zero, add_zero, Nat.cast_one, zero_add] at h\n exact h\n -- the Stirling bounds at w + 2 and w\u2080\n have hvre : (0 : \u211d) < (w + 2).re := by\n have h : (w + 2).re = w.re + 2 := by simp\n rw [h, hwre]\n linarith [h\u03c3lo]\n have hvim : (w + 2).im = t / 2 := by\n have h : (w + 2).im = w.im := by simp\n rw [h, hwim]\n have hStir1 := StirlingVert.digamma_stirling hvre (by\n rw [hvim, abs_of_nonneg (by linarith : (0 : \u211d) \u2264 t / 2)]; linarith)\n have hStir2 := StirlingVert.digamma_stirling hw\u2080re (by\n rw [hw\u2080im, abs_of_nonneg (by linarith : (0 : \u211d) \u2264 t / 2)]; linarith)\n -- the remainders\n set r1 : \u2102 := Complex.digamma (w + 2) - Complex.log (w + 2) + (1 / 2) / (w + 2) with hr1\n set r0 : \u2102 := Complex.digamma w\u2080 - Complex.log w\u2080 + (1 / 2) / w\u2080 with hr0\n have hr1le : \u2016r1\u2016 \u2264 3 / (t / 2) ^ 2 := by\n have h := hStir1\n rw [hvim] at h\n exact h\n have hr0le : \u2016r0\u2016 \u2264 3 / (t / 2) ^ 2 := by\n have h := hStir2\n rw [hw\u2080im] at h\n exact h\n -- the decomposition\n have hdecomp : Complex.digamma w - Complex.digamma w\u2080\n = (Complex.log (w + 2) - Complex.log w\u2080)\n + ((1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2)) - w\u207b\u00b9 - (w + 1)\u207b\u00b9 + (r1 - r0) := by\n rw [hr1, hr0]\n linear_combination hrec\n -- the pieces\n have hL : \u2016Complex.log (w + 2) - Complex.log w\u2080\u2016 \u2264 5 / t := by\n rw [hw, hw\u2080eq]\n exact log_diff_le ht h\u03c3lo h\u03c3hi him\n have hw0norm : t / 2 \u2264 \u2016w\u2080\u2016 := by\n have h1 := abs_im_le_norm w\u2080\n rw [hw\u2080im, abs_of_nonneg (by linarith : (0 : \u211d) \u2264 t / 2)] at h1\n exact h1\n have hw2norm : t / 2 \u2264 \u2016w + 2\u2016 := by\n have h1 := abs_im_le_norm (w + 2)\n rw [hvim, abs_of_nonneg (by linarith : (0 : \u211d) \u2264 t / 2)] at h1\n exact h1\n have hwnorm : t / 2 \u2264 \u2016w\u2016 := by\n have h1 := abs_im_le_norm w\n rw [hwim, abs_of_nonneg (by linarith : (0 : \u211d) \u2264 t / 2)] at h1\n exact h1\n have hw1norm : t / 2 \u2264 \u2016w + 1\u2016 := by\n have h1 := abs_im_le_norm (w + 1)\n have h2 : (w + 1).im = t / 2 := by simp [hwim]\n rw [h2, abs_of_nonneg (by linarith : (0 : \u211d) \u2264 t / 2)] at h1\n exact h1\n have hw\u20800 : w\u2080 \u2260 0 := by\n intro h\n rw [h, norm_zero] at hw0norm\n linarith\n have hw2 : w + 2 \u2260 0 := by\n intro h\n rw [h, norm_zero] at hw2norm\n linarith\n have hw0 : w \u2260 0 := by\n intro h\n rw [h, norm_zero] at hwnorm\n linarith\n have hw1 : w + 1 \u2260 0 := by\n intro h\n rw [h, norm_zero] at hw1norm\n linarith\n have h12 : \u2016(1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2)\u2016 \u2264 5 / t ^ 2 := by\n have h1 : (1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2)\n = (1 / 2) * ((w + 2 - w\u2080) / (w\u2080 * (w + 2))) := by\n field_simp\n ring\n have hsub : w + 2 - w\u2080 = ((s.re / 2 + 1 : \u211d) : \u2102) := by\n have ht1 : w\u2080 + ((s.re / 2 + 1 : \u211d) : \u2102) = w + 2 := by\n rw [hw, hw\u2080eq]\n rw [Complex.ext_iff]\n constructor\n \u00b7 simp [hwre]\n ring_nf\n \u00b7 simp [hw\u2080im]\n rw [hwim]\n linear_combination ht1\n rw [h1, hsub, norm_mul, norm_div, Complex.norm_real]\n have hc : |s.re / 2 + 1| \u2264 5 / 2 := by\n rw [abs_le]\n constructor <;> linarith\n have h12n : \u2016(1 / 2 : \u2102)\u2016 = 1 / 2 := by\n rw [show (1 / 2 : \u2102) = ((1 / 2 : \u211d) : \u2102) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [h12n]\n have hprod : (t / 2) * (t / 2) \u2264 \u2016w\u2080\u2016 * \u2016w + 2\u2016 :=\n mul_le_mul hw0norm hw2norm (by positivity) (by positivity)\n calc (1 / 2) * (|s.re / 2 + 1| / (\u2016w\u2080\u2016 * \u2016w + 2\u2016))\n \u2264 (1 / 2) * ((5 / 2) / (\u2016w\u2080\u2016 * \u2016w + 2\u2016)) := by\n apply mul_le_mul_of_nonneg_left _ (by norm_num)\n exact div_le_div_of_nonneg_right hc (by positivity)\n _ \u2264 (1 / 2) * ((5 / 2) / ((t / 2) * (t / 2))) := by\n apply mul_le_mul_of_nonneg_left _ (by norm_num)\n exact div_le_div_of_nonneg_left (by norm_num) (by positivity) hprod\n _ = 5 / t ^ 2 := by field_simp; ring\n have hw1b : \u2016(w : \u2102)\u207b\u00b9\u2016 \u2264 2 / t := by\n rw [norm_inv]\n have hpos : (0 : \u211d) < \u2016w\u2016 := by positivity\n calc \u2016w\u2016\u207b\u00b9 \u2264 (t / 2)\u207b\u00b9 := by\n rw [inv_le_inv\u2080 hpos (by positivity : (0 : \u211d) < t / 2)]\n exact hwnorm\n _ = 2 / t := by rw [inv_div]\n have hw1'b : \u2016(w + 1 : \u2102)\u207b\u00b9\u2016 \u2264 2 / t := by\n rw [norm_inv]\n have hpos : (0 : \u211d) < \u2016w + 1\u2016 := by positivity\n calc \u2016w + 1\u2016\u207b\u00b9 \u2264 (t / 2)\u207b\u00b9 := by\n rw [inv_le_inv\u2080 hpos (by positivity : (0 : \u211d) < t / 2)]\n exact hw1norm\n _ = 2 / t := by rw [inv_div]\n -- the norm chain\n have hnorm : \u2016Complex.digamma w - Complex.digamma w\u2080\u2016\n \u2264 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (3 / (t / 2) ^ 2 + 3 / (t / 2) ^ 2) := by\n rw [hdecomp]\n have hc1 : \u2016(Complex.log (w + 2) - Complex.log w\u2080)\n + ((1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2)) - w\u207b\u00b9 - (w + 1)\u207b\u00b9 + (r1 - r0)\u2016\n \u2264 \u2016(Complex.log (w + 2) - Complex.log w\u2080)\n + ((1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2)) - w\u207b\u00b9 - (w + 1)\u207b\u00b9\u2016 + \u2016r1 - r0\u2016 :=\n norm_add_le _ _\n have hc2 : \u2016(Complex.log (w + 2) - Complex.log w\u2080)\n + ((1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2)) - w\u207b\u00b9 - (w + 1)\u207b\u00b9\u2016\n \u2264 \u2016(Complex.log (w + 2) - Complex.log w\u2080)\n + ((1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2)) - w\u207b\u00b9\u2016 + \u2016(w + 1)\u207b\u00b9\u2016 :=\n norm_sub_le _ _\n have hc3 : \u2016(Complex.log (w + 2) - Complex.log w\u2080)\n + ((1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2)) - w\u207b\u00b9\u2016\n \u2264 \u2016(Complex.log (w + 2) - Complex.log w\u2080)\n + ((1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2))\u2016 + \u2016w\u207b\u00b9\u2016 :=\n norm_sub_le _ _\n have hc4 : \u2016(Complex.log (w + 2) - Complex.log w\u2080)\n + ((1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2))\u2016\n \u2264 \u2016Complex.log (w + 2) - Complex.log w\u2080\u2016\n + \u2016(1 / 2 : \u2102) / w\u2080 - (1 / 2) / (w + 2)\u2016 :=\n norm_add_le _ _\n have hc5 : \u2016r1 - r0\u2016 \u2264 \u2016r1\u2016 + \u2016r0\u2016 := norm_sub_le _ _\n linarith [hc1, hc2, hc3, hc4, hc5, hL, h12, hw1b, hw1'b, hr1le, hr0le]\n -- the fold to 6/t\n have h2norm : \u2016(2 : \u2102)\u2016 = 2 := by\n rw [show (2 : \u2102) = ((2 : \u211d) : \u2102) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [hw, hw\u2080, norm_div, h2norm]\n rw [div_le_iff\u2080 (by norm_num : (0 : \u211d) < 2)]\n have h1 : (3 : \u211d) / (t / 2) ^ 2 = 12 / t ^ 2 := by\n field_simp\n ring\n have hsum : 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (12 / t ^ 2 + 12 / t ^ 2)\n = 9 / t + 29 / t ^ 2 := by\n field_simp\n ring\n have hkey : 9 / t + 29 / t ^ 2 \u2264 12 / t := by\n rw [show (12 : \u211d) / t = 12 * t / t ^ 2 by field_simp; ring]\n rw [show 9 / t + 29 / t ^ 2 = (9 * t + 29) / t ^ 2 by field_simp; ring]\n apply div_le_div_of_nonneg_right _ (by positivity : (0 : \u211d) \u2264 t ^ 2)\n nlinarith [ht]\n calc \u2016Complex.digamma w - Complex.digamma w\u2080\u2016\n \u2264 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (3 / (t / 2) ^ 2 + 3 / (t / 2) ^ 2) := hnorm\n _ = 9 / t + 29 / t ^ 2 := by rw [h1]; rw [hsum]\n _ \u2264 12 / t := hkey\n _ = 6 / t * 2 := by ring\n\nend NguyenRH1\n\nend"
}
raw content_json (database row)
[{"type":"thinking","thinking":"The sorry draft is at lines 599–618 (from `rw [← hint]` through the digamma_diff_le sorry). I'll replace lines 599–618 with the complete hbound proof + the complete digamma_diff_le. Let me do the edit with the exact old text (lines 599–618).","signature":""},{"type":"text","text":"Replacing the sorry draft (lines 599–618) with the complete proofs."},{"type":"tool_use","id":"Edit_225","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":" rw [← hint]\n have hbound : ∀ y ∈ Set.uIoc (0 : ℝ) 1,\n ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ ≤ 5 / t := by\n intro y hy\n have h1 : ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ = ‖z y‖⁻¹ * |c| := by\n rw [norm_mul, norm_inv]\n rw [show ((c : ℝ) : ℂ) = (((|c| : ℝ)) : ℂ) * ... ] -- hmm no\n sorry\n sorry\n sorry\n\n/-- **Piece 6** (D-069 §3): the digamma difference\n½‖ψ(s/2) − ψ(s₀/2)‖ ≤ 6/t. Via the +2 shift (re(w+2) ≥ 3/4), Zeta23's\ndigamma_stirling at w+2 and w₀, the recurrence ψ(w) = ψ(w+2) − w⁻¹ −\n(w+1)⁻¹, and the segment-FTC log bound. -/\ntheorem digamma_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) :\n ‖(Complex.digamma (s / 2) - Complex.digamma ((2 + t * Complex.I) / 2)) / 2‖\n ≤ 6 / t := by\n sorry\n\nend NguyenRH1\n\nend","new_string":" rw [← hint]\n have hbound : ∀ y ∈ Set.Ι (0 : ℝ) 1,\n ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ ≤ 5 / t := by\n intro y _\n have hzy : (0 : ℝ) < ‖z y‖ := by\n have h := hznorm y\n positivity\n have h1 : ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ = ‖z y‖⁻¹ * |c| := by\n rw [norm_mul, norm_inv, Complex.norm_real]\n rw [h1]\n have h2 : ‖z y‖⁻¹ ≤ (t / 2)⁻¹ := by\n rw [inv_le_inv₀ hzy (by positivity : (0 : ℝ) < t / 2)]\n exact hznorm y\n calc ‖z y‖⁻¹ * |c| ≤ (t / 2)⁻¹ * (5 / 2) :=\n mul_le_mul h2 hcle (abs_nonneg _) (by positivity)\n _ = 5 / t := by field_simp\n calc ‖∫ y in (0 : ℝ)..(1 : ℝ), ((z y)⁻¹) * ((c : ℝ) : ℂ)‖\n ≤ (5 / t) * |1 - 0| := intervalIntegral.norm_integral_le_of_norm_le_const hbound\n _ = 5 / t := by norm_num [abs_one]\n\n/-- **Piece 6** (D-069 §3): the digamma difference\n½‖ψ(s/2) − ψ(s₀/2)‖ ≤ 6/t. Via the +2 shift (re(w+2) ≥ 3/4), Zeta23's\ndigamma_stirling at w+2 and w₀, the recurrence ψ(w) = ψ(w+2) − w⁻¹ −\n(w+1)⁻¹, and the segment-FTC log bound. -/\ntheorem digamma_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) :\n ‖(Complex.digamma (s / 2) - Complex.digamma ((2 + t * Complex.I) / 2)) / 2‖\n ≤ 6 / t := by\n have ht0 : (0 : ℝ) < t := by linarith\n set w : ℂ := s / 2 with hw\n set w₀ : ℂ := (2 + t * Complex.I) / 2 with hw₀\n have hw₀eq : w₀ = 1 + (t / 2) * Complex.I := by rw [hw₀]; ring\n have hwim : w.im = t / 2 := by rw [hw]; simp [him]\n have hw₀im : w₀.im = t / 2 := by rw [hw₀eq]; simp\n have himw : w.im ≠ 0 := by rw [hwim]; positivity\n have hwre : w.re = s.re / 2 := by rw [hw]; simp\n have hw₀re : (0 : ℝ) < w₀.re := by rw [hw₀eq]; simp\n -- the recurrence: ψ(w + 2) = ψ(w) + w⁻¹ + (w+1)⁻¹\n have hrec : Complex.digamma (w + 2) = Complex.digamma w + (w⁻¹ + (w + 1)⁻¹) := by\n have h := digamma_add_natCast himw 2\n rw [show w + ((2 : ℕ) : ℂ) = w + 2 by push_cast; ring] at h\n rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h\n simp only [Nat.cast_zero, add_zero, Nat.cast_one, zero_add] at h\n exact h\n -- the Stirling bounds at w + 2 and w₀\n have hvre : (0 : ℝ) < (w + 2).re := by\n have h : (w + 2).re = w.re + 2 := by simp\n rw [h, hwre]\n linarith [hσlo]\n have hvim : (w + 2).im = t / 2 := by\n have h : (w + 2).im = w.im := by simp\n rw [h, hwim]\n have hStir1 := StirlingVert.digamma_stirling hvre (by\n rw [hvim, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)]; linarith)\n have hStir2 := StirlingVert.digamma_stirling hw₀re (by\n rw [hw₀im, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)]; linarith)\n -- the remainders\n set r1 : ℂ := Complex.digamma (w + 2) - Complex.log (w + 2) + (1 / 2) / (w + 2) with hr1\n set r0 : ℂ := Complex.digamma w₀ - Complex.log w₀ + (1 / 2) / w₀ with hr0\n have hr1le : ‖r1‖ ≤ 3 / (t / 2) ^ 2 := by\n have h := hStir1\n rw [hvim] at h\n exact h\n have hr0le : ‖r0‖ ≤ 3 / (t / 2) ^ 2 := by\n have h := hStir2\n rw [hw₀im] at h\n exact h\n -- the decomposition\n have hdecomp : Complex.digamma w - Complex.digamma w₀\n = (Complex.log (w + 2) - Complex.log w₀)\n + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹ + (r1 - r0) := by\n rw [hr1, hr0]\n linear_combination hrec\n -- the pieces\n have hL : ‖Complex.log (w + 2) - Complex.log w₀‖ ≤ 5 / t := by\n rw [hw, hw₀eq]\n exact log_diff_le ht hσlo hσhi him\n have hw0norm : t / 2 ≤ ‖w₀‖ := by\n have h1 := abs_im_le_norm w₀\n rw [hw₀im, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n exact h1\n have hw2norm : t / 2 ≤ ‖w + 2‖ := by\n have h1 := abs_im_le_norm (w + 2)\n rw [hvim, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n exact h1\n have hwnorm : t / 2 ≤ ‖w‖ := by\n have h1 := abs_im_le_norm w\n rw [hwim, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n exact h1\n have hw1norm : t / 2 ≤ ‖w + 1‖ := by\n have h1 := abs_im_le_norm (w + 1)\n have h2 : (w + 1).im = t / 2 := by simp [hwim]\n rw [h2, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n exact h1\n have hw₀0 : w₀ ≠ 0 := by\n intro h\n rw [h, norm_zero] at hw0norm\n linarith\n have hw2 : w + 2 ≠ 0 := by\n intro h\n rw [h, norm_zero] at hw2norm\n linarith\n have hw0 : w ≠ 0 := by\n intro h\n rw [h, norm_zero] at hwnorm\n linarith\n have hw1 : w + 1 ≠ 0 := by\n intro h\n rw [h, norm_zero] at hw1norm\n linarith\n have h12 : ‖(1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)‖ ≤ 5 / t ^ 2 := by\n have h1 : (1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)\n = (1 / 2) * ((w + 2 - w₀) / (w₀ * (w + 2))) := by\n field_simp\n ring\n have hsub : w + 2 - w₀ = ((s.re / 2 + 1 : ℝ) : ℂ) := by\n have ht1 : w₀ + ((s.re / 2 + 1 : ℝ) : ℂ) = w + 2 := by\n rw [hw, hw₀eq]\n rw [Complex.ext_iff]\n constructor\n · simp [hwre]\n ring_nf\n · simp [hw₀im]\n rw [hwim]\n linear_combination ht1\n rw [h1, hsub, norm_mul, norm_div, Complex.norm_real]\n have hc : |s.re / 2 + 1| ≤ 5 / 2 := by\n rw [abs_le]\n constructor <;> linarith\n have h12n : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by\n rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [h12n]\n have hprod : (t / 2) * (t / 2) ≤ ‖w₀‖ * ‖w + 2‖ :=\n mul_le_mul hw0norm hw2norm (by positivity) (by positivity)\n calc (1 / 2) * (|s.re / 2 + 1| / (‖w₀‖ * ‖w + 2‖))\n ≤ (1 / 2) * ((5 / 2) / (‖w₀‖ * ‖w + 2‖)) := by\n apply mul_le_mul_of_nonneg_left _ (by norm_num)\n exact div_le_div_of_nonneg_right hc (by positivity)\n _ ≤ (1 / 2) * ((5 / 2) / ((t / 2) * (t / 2))) := by\n apply mul_le_mul_of_nonneg_left _ (by norm_num)\n exact div_le_div_of_nonneg_left (by norm_num) (by positivity) hprod\n _ = 5 / t ^ 2 := by field_simp; ring\n have hw1b : ‖(w : ℂ)⁻¹‖ ≤ 2 / t := by\n rw [norm_inv]\n have hpos : (0 : ℝ) < ‖w‖ := by positivity\n calc ‖w‖⁻¹ ≤ (t / 2)⁻¹ := by\n rw [inv_le_inv₀ hpos (by positivity : (0 : ℝ) < t / 2)]\n exact hwnorm\n _ = 2 / t := by rw [inv_div]\n have hw1'b : ‖(w + 1 : ℂ)⁻¹‖ ≤ 2 / t := by\n rw [norm_inv]\n have hpos : (0 : ℝ) < ‖w + 1‖ := by positivity\n calc ‖w + 1‖⁻¹ ≤ (t / 2)⁻¹ := by\n rw [inv_le_inv₀ hpos (by positivity : (0 : ℝ) < t / 2)]\n exact hw1norm\n _ = 2 / t := by rw [inv_div]\n -- the norm chain\n have hnorm : ‖Complex.digamma w - Complex.digamma w₀‖\n ≤ 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (3 / (t / 2) ^ 2 + 3 / (t / 2) ^ 2) := by\n rw [hdecomp]\n have hc1 : ‖(Complex.log (w + 2) - Complex.log w₀)\n + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹ + (r1 - r0)‖\n ≤ ‖(Complex.log (w + 2) - Complex.log w₀)\n + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹‖ + ‖r1 - r0‖ :=\n norm_add_le _ _\n have hc2 : ‖(Complex.log (w + 2) - Complex.log w₀)\n + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹‖\n ≤ ‖(Complex.log (w + 2) - Complex.log w₀)\n + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹‖ + ‖(w + 1)⁻¹‖ :=\n norm_sub_le _ _\n have hc3 : ‖(Complex.log (w + 2) - Complex.log w₀)\n + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹‖\n ≤ ‖(Complex.log (w + 2) - Complex.log w₀)\n + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2))‖ + ‖w⁻¹‖ :=\n norm_sub_le _ _\n have hc4 : ‖(Complex.log (w + 2) - Complex.log w₀)\n + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2))‖\n ≤ ‖Complex.log (w + 2) - Complex.log w₀‖\n + ‖(1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)‖ :=\n norm_add_le _ _\n have hc5 : ‖r1 - r0‖ ≤ ‖r1‖ + ‖r0‖ := norm_sub_le _ _\n linarith [hc1, hc2, hc3, hc4, hc5, hL, h12, hw1b, hw1'b, hr1le, hr0le]\n -- the fold to 6/t\n have h2norm : ‖(2 : ℂ)‖ = 2 := by\n rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n norm_num\n rw [hw, hw₀, norm_div, h2norm]\n rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2)]\n have h1 : (3 : ℝ) / (t / 2) ^ 2 = 12 / t ^ 2 := by\n field_simp\n ring\n have hsum : 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (12 / t ^ 2 + 12 / t ^ 2)\n = 9 / t + 29 / t ^ 2 := by\n field_simp\n ring\n have hkey : 9 / t + 29 / t ^ 2 ≤ 12 / t := by\n rw [show (12 : ℝ) / t = 12 * t / t ^ 2 by field_simp; ring]\n rw [show 9 / t + 29 / t ^ 2 = (9 * t + 29) / t ^ 2 by field_simp; ring]\n apply div_le_div_of_nonneg_right _ (by positivity : (0 : ℝ) ≤ t ^ 2)\n nlinarith [ht]\n calc ‖Complex.digamma w - Complex.digamma w₀‖\n ≤ 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (3 / (t / 2) ^ 2 + 3 / (t / 2) ^ 2) := hnorm\n _ = 9 / t + 29 / t ^ 2 := by rw [h1]; rw [hsum]\n _ ≤ 12 / t := hkey\n _ = 6 / t * 2 := by ring\n\nend NguyenRH1\n\nend"},"extra_content":null}]