completedHurwitzZetaOdd_neg — Mathlib

English

The odd part remains odd under negation of the first argument: completedHurwitzZetaOdd(-a, s) = - completedHurwitzZetaOdd(a, s).

Русский

Нечетная часть остаётся нечетной при замене первого аргумента на −a.

LaTeX

$$$$ completedHurwitzZetaOdd(-a, s) = - completedHurwitzZetaOdd(a, s). $$$$

Lean4

theorem completedHurwitzZetaOdd_neg (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaOdd (-a) s = -completedHurwitzZetaOdd a s := by
  simp [completedHurwitzZetaOdd, StrongFEPair.Λ, hurwitzOddFEPair, mellin, oddKernel_neg, integral_neg, neg_div]

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