Source indexedlemma · leanprover/lean4:v4.32.0

Backlund.zetaSurrogate_differentiable

PrimeNumberTheoremAnd.Backlund.ZeroCountCrude · PrimeNumberTheoremAnd/Backlund/ZeroCountCrude.lean:59 to 78

Source documentation

The surrogate is entire: differentiable off 1 by congruence with (s - 1) · ζ(s), and at 1 by the removable-singularity criterion with the residue limit.

Exact Lean statement

lemma zetaSurrogate_differentiable : Differentiable ℂ zetaSurrogate

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma zetaSurrogate_differentiable : Differentiable ℂ zetaSurrogate := by  rw [← differentiableOn_univ,    ← Complex.differentiableOn_compl_singleton_and_continuousAt_iff      (c := (1 : ℂ)) Filter.univ_mem]  constructor  · intro s hs    have hs1 : s ≠ 1 := by simpa using hs.2    have hd : DifferentiableAt ℂ (fun w : ℂ ↦ (w - 1) * riemannZeta w) s :=      (differentiableAt_id.sub_const 1).mul (differentiableAt_riemannZeta hs1)    exact (hd.congr_of_eventuallyEq (zetaSurrogate_eventuallyEq hs1)).differentiableWithinAt  · have h1 : zetaSurrogate 1 = 1 := if_pos rfl    have hev : (fun w : ℂ ↦ (w - 1) * riemannZeta w) =ᶠ[nhdsWithin 1 {(1 : ℂ)}ᶜ]        zetaSurrogate := by      filter_upwards [self_mem_nhdsWithin] with w hw      simp [zetaSurrogate, Set.mem_compl_singleton_iff.mp hw]    have key : Filter.Tendsto zetaSurrogate (nhdsWithin 1 {(1 : ℂ)}ᶜ)        (nhds (zetaSurrogate 1)) := by      rw [h1]      exact Filter.Tendsto.congr' hev riemannZeta_residue_one    exact continuousWithinAt_compl_self.mp key