Theorems · Theorem · number theory

HurwitzZeta.differentiableAt_update_of_residue

∀ {Λ : ℂ → ℂ},
  (∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s) →
    ∀ {L : ℂ},
      Filter.Tendsto (fun s => s * Λ s) (nhdsWithin 0 {0}ᶜ) (nhds L) →
        ∀ (s : ℂ), s ≠ 1 → DifferentiableAt ℂ (Function.update (fun s => Λ s / s.Gammaℝ) 0 (L / 2)) s

Technical lemma which will give us differentiability of Hurwitz zeta at s = 0.

Defined in

Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Cited by

2 results in Mathlib

Foundations

Depth 288 from the axioms · uses propext, Classical.choice, Quot.sound