Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.zetaTimesSMinusOne_entire_differentiableOn_compl_singleton

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:480 to 493

Source documentation

Away from 1, the removable extension is holomorphic as (s - 1)ζ(s).

Exact Lean statement

theorem zetaTimesSMinusOne_entire_differentiableOn_compl_singleton :
    DifferentiableOn ℂ zetaTimesSMinusOne_entire (Set.univ \ ({1} : Set ℂ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zetaTimesSMinusOne_entire_differentiableOn_compl_singleton :    DifferentiableOn ℂ zetaTimesSMinusOne_entire (Set.univ \ ({1} : Set ℂ)) := by  intro s hs  have hs1 : s ≠ 1 := by    simpa [Set.mem_singleton_iff] using hs.2  have h1 : DifferentiableAt ℂ (fun s => s - 1) s := differentiableAt_id.sub_const 1  have h2 : DifferentiableAt ℂ riemannZeta s := differentiableAt_riemannZeta hs1  have hmul : DifferentiableAt ℂ (fun s => (s - 1) * riemannZeta s) s := by    simpa [mul_assoc, mul_left_comm, mul_comm] using! (h1.mul h2)  refine (hmul.differentiableWithinAt.congr (fun x hx => ?_) ?_)  · have hx1 : x ≠ (1 : ℂ) := by      simpa [Set.mem_singleton_iff] using hx.2    exact zetaTimesSMinusOne_entire_eq_mul_riemannZeta hx1  · exact zetaTimesSMinusOne_entire_eq_mul_riemannZeta hs1