{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-010-suzuki-W-function.py",
  "limit": 28,
  "offset": 155
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCrux.lean",
    "content": "    rw [hLiExt_of_ne hs0]\n    have hh : hLi (1 + s) = 1 - s * (deriv zetaA (1 + s) / zetaA (1 + s)) := by\n      rw [hLi]\n      ring_nf\n    rw [hh]\n    have hX : (1 - (1 - s * (deriv zetaA (1 + s) / zetaA (1 + s)))) / s =\n        deriv zetaA (1 + s) / zetaA (1 + s) := by\n      have e : 1 - (1 - s * (deriv zetaA (1 + s) / zetaA (1 + s))) =\n          s * (deriv zetaA (1 + s) / zetaA (1 + s)) := by ring\n      rw [e, mul_div_cancel_left\u2080 _ hs0]\n    rw [hX]\n    have hzeq : (fun w : \u2102 => (w - 1) * riemannZeta w) =\u1da0[\ud835\udcdd (1 + s)] zetaA := by\n      filter_upwards [eventually_ne_nhds hs1'] with z hz\n      exact (zetaA_apply hz).symm\n    have hderiv_zetaA : deriv zetaA (1 + s) =\n        riemannZeta (1 + s) + s * deriv riemannZeta (1 + s) := by\n      rw [\u2190 hzeq.deriv_eq]\n      have hsplit : (fun w : \u2102 => (w - 1) * riemannZeta w) =\n          (fun w : \u2102 => w - 1) * riemannZeta := rfl\n      have hf : DifferentiableAt \u2102 (fun w : \u2102 => w - 1) (1 + s) := differentiableAt_id.sub_const 1\n      rw [hsplit, deriv_mul hf (differentiableAt_riemannZeta hs1')]\n      have h1 : deriv (fun w : \u2102 => w - 1) (1 + s) = 1 := by\n        simp using ((hasDerivAt_id' (1 + s)).sub_const 1).deriv\n      rw [h1]\n      ring",
    "numLines": 25,
    "startLine": 188,
    "totalLines": 428
  }
}