{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
  "offset": 790,
  "limit": 22
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
    "content": "/-- The (1/2 + m)-power series is summable (norm \u2264 2^{k+1}/(m+1)^{k+1}). -/\nlemma summable_zpow_half_add_nat (k : \u2115) (hk : 1 \u2264 k) :\n    Summable (fun m : \u2115 => ((1 / 2 : \u2102) + \u2191m) ^ (-(k : \u2124) - 1)) := by\n  apply Summable.of_norm_bounded (summable_div_add_one_pow (2 ^ (k + 1)) (k + 1) (by omega))\n  intro m\n  have hpos : (0 : \u211d) < (m : \u211d) + 1 / 2 := by positivity\n  have h1 : \u2016((1 / 2 : \u2102) + \u2191m)\u2016 = (m : \u211d) + 1 / 2 := by\n    have e : ((1 / 2 : \u2102) + \u2191m) = \u2191((m : \u211d) + 1 / 2) := by push_cast; ring\n    rw [e, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg hpos.le]\n  rw [norm_zpow, h1]\n  rw [show (-(k : \u2124) - 1 : \u2124) = -(((k + 1 : \u2115) : \u2124)) by push_cast; ring, zpow_neg, zpow_natCast]\n  rw [div_eq_mul_inv, \u2190 one_div, \u2190 one_div]\n  apply one_div_le_one_div_of_le (by positivity)\n  have h2 : ((m : \u211d) + 1) ^ (k + 1) \u2264 2 ^ (k + 1) * ((m + 1 / 2 : \u211d)) ^ (k + 1) := by\n    rw [show (2 : \u211d) ^ (k + 1) * ((m + 1 / 2 : \u211d)) ^ (k + 1) =\n      (2 * (m + 1 / 2 : \u211d)) ^ (k + 1) by rw [mul_pow]]\n    apply pow_le_pow_left\u2080 (by positivity : (0 : \u211d) \u2264 (m : \u211d) + 1)\n    \u00b7 ring_nf\n      linarith [Nat.cast_nonneg (\u03b1 := \u211d) m]\n  exact h2\n\n/-- The polygamma values of DinfC at 1/2 (j \u2265 1). -/",
    "numLines": 22,
    "startLine": 790,
    "totalLines": 871
  }
}