{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean",
  "offset": 483,
  "limit": 70
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigammaLeft.lean",
    "content": "theorem 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",
    "numLines": 70,
    "startLine": 483,
    "totalLines": 668
  }
}