differentiable_hurwitzZetaEven_sub_hurwitzZetaEven

English

For any a,b ∈ UnitAddCircle, the difference hurwitzZetaEven a s − hurwitzZetaEven b s is differentiable (as a function of s).

Русский

Для любых a,b ∈ UnitAddCircle разность hurwitzZetaEven a s − hurwitzZetaEven b s дифференцируема по переменной s.

LaTeX

$$$\\forall a,b:\\text{UnitAddCircle},\\ \\mathrm{Differentiable}_{\\mathbb{C}}\\bigl( s \\mapsto \\mathrm{hurwitzZetaEven}(a,s) - \\mathrm{hurwitzZetaEven}(b,s) \\bigr).$$$

Lean4

theorem differentiable_hurwitzZetaEven_sub_hurwitzZetaEven (a b : UnitAddCircle) :
    Differentiable ℂ (fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) :=
  by
  intro z
  rcases ne_or_eq z 1 with hz | rfl
  · exact (differentiableAt_hurwitzZetaEven a hz).sub (differentiableAt_hurwitzZetaEven b hz)
  · convert
      (differentiableAt_hurwitzZetaEven_sub_one_div a).fun_sub (differentiableAt_hurwitzZetaEven_sub_one_div b) using
      2 with s
    abel

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