Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.zetaTimesSMinusOne_entire_continuousAt_one

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:496 to 509

Source documentation

The residue theorem for ζ gives continuity of the removable extension at 1.

Exact Lean statement

theorem zetaTimesSMinusOne_entire_continuousAt_one :
    ContinuousAt zetaTimesSMinusOne_entire (1 : ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zetaTimesSMinusOne_entire_continuousAt_one :    ContinuousAt zetaTimesSMinusOne_entire (1 : ℂ) := by  have h :      ContinuousAt        (Function.update (fun s : ℂ => (s - 1) * riemannZeta s) (1 : ℂ) (1 : ℂ))        (1 : ℂ) :=    (continuousAt_update_same (f := fun s : ℂ => (s - 1) * riemannZeta s)        (x := (1 : ℂ)) (y := (1 : ℂ))).2      (riemannZeta_residue_one : Tendsto (fun s : ℂ => (s - 1) * riemannZeta s)        (𝓝[≠] (1 : ℂ)) (𝓝 (1 : ℂ)))  change    ContinuousAt (Function.update (fun s : ℂ => (s - 1) * riemannZeta s) (1 : ℂ) (1 : ℂ))      (1 : ℂ)  exact h