Source indexedtheorem · leanprover/lean4:v4.32.0

ZetaAbelFractKernel.hasDerivAt_in_param

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean:129 to 138

Mathematical statement

Exact Lean statement

theorem hasDerivAt_in_param (u : ℝ) (hu : 1 < u) (z : ℂ) :
    HasDerivAt (fun w => zetaAbelFractKernel w u)
      (-((Real.log u) : ℂ) * zetaAbelFractKernel z u) z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem hasDerivAt_in_param (u : ℝ) (hu : 1 < u) (z : ℂ) :    HasDerivAt (fun w => zetaAbelFractKernel w u)      (-((Real.log u) : ℂ) * zetaAbelFractKernel z u) z := by  have h := HasDerivAt.const_mul_ofReal_cpow_neg_sub_one ((Int.fract u : ℝ) : ℂ)    (lt_trans zero_lt_one hu) z  have hfun : (fun w => zetaAbelFractKernel w u) = fun w => ((Int.fract u : ℝ) : ℂ) * (u : ℂ) ^ (-w - 1) := by    ext w; simp [zetaAbelFractKernel]  exact (h.congr_of_eventuallyEq (EventuallyEq.of_eq hfun)).congr_deriv (by    simp [zetaAbelFractKernel, Complex.ofReal_log (x := u) (hx := le_of_lt (lt_trans zero_lt_one hu)),      mul_comm, mul_assoc, mul_left_comm])