LFunction_apply_zero_of_even — Mathlib

English

If Φ is even, then L(Φ, 0) = −Φ(0)/2.

Русский

Если Φ четная, тогда L(Φ, 0) = −Φ(0)/2.

LaTeX

$$$$L(\Phi, 0) = -\frac{\Phi(0)}{2}.$$$$

Lean4

/-- Explicit formula for `LFunction Φ 0` when `Φ` is even. -/
@[simp]
theorem LFunction_apply_zero_of_even (hΦ : Φ.Even) : LFunction Φ 0 = -Φ 0 / 2 := by
  simp only [LFunction_def_even hΦ, neg_zero, cpow_zero, hurwitzZetaEven_apply_zero, toAddCircle_eq_zero, mul_ite,
    mul_div, mul_neg_one, mul_zero, sum_ite_eq', Finset.mem_univ, ↓reduceIte, one_mul]

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