bernoulliFourierCoeff_zero — Mathlib

English

The zeroth Fourier coefficient of B_k is zero when k ≠ 0.

Русский

Нулевой коэффициент по частоте для B_k равен нулю, если k ≠ 0.

LaTeX

$$$$ bernoulliFourierCoeff(k, 0) = 0 \\quad (k \\neq 0). $$$$

Lean4

/-- The `0`-th Fourier coefficient of `Bₖ(x)`. -/
theorem bernoulliFourierCoeff_zero {k : ℕ} (hk : k ≠ 0) : bernoulliFourierCoeff k 0 = 0 := by
  simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero, div_one, one_smul,
    intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk, ofReal_zero]

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