differentiable_completedLFunction₀

English

The auxiliary completed L-function with even/odd Hurwitz zeta terms is differentiable in the complex variable.

Русский

Вспомогательная завершенная L-функция дифференцируема по комплексной переменной.

LaTeX

$$$$\text{Differentiable}_{\mathbb{C}}\left(\mathrm{completedLFunction}_{0}(\Phi)\right).$$$$

Lean4

/-- The function `completedLFunction₀ Φ` is differentiable. -/
theorem differentiable_completedLFunction₀ (Φ : ZMod N → ℂ) : Differentiable ℂ (completedLFunction₀ Φ) :=
  by
  refine .add ?_ ?_ <;> refine .mul (by fun_prop) (.fun_sum fun i _ ↦ .const_mul ?_ _)
  exacts [differentiable_completedHurwitzZetaEven₀ _, differentiable_completedHurwitzZetaOdd _]

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