differentiable_LFunctionTrivChar₁

English

The function s ↦ LFunctionTrivChar₁ n s is differentiable in ℂ for every n with NeZero n.

Русский

Функция s ↦ LFunctionTrivChar₁ n s дифференцируема по комплексной плоскости для каждого n с NeZero n.

LaTeX

$$$\text{Differentiable}(LFunctionTrivChar_1(n))$$$

Lean4

/-- `s ↦ (s - 1) * L χ s` is an entire function when `χ` is a trivial Dirichlet character. -/
theorem differentiable_LFunctionTrivChar₁ : Differentiable ℂ (LFunctionTrivChar₁ n) :=
  by
  rw [← differentiableOn_univ, ← differentiableOn_compl_singleton_and_continuousAt_iff (c := 1) Filter.univ_mem]
  refine
    ⟨DifferentiableOn.congr (f := fun s ↦ (s - 1) * LFunctionTrivChar n s)
        (fun _ hs ↦ DifferentiableAt.differentiableWithinAt <| by fun_prop (disch := simp_all)) fun _ hs ↦
        Function.update_of_ne (Set.mem_diff_singleton.mp hs).2 ..,
      continuousWithinAt_compl_self.mp ?_⟩
  simpa using LFunctionTrivChar_residue_one

Похожие утверждения