integral_bernoulliFun_eq_zero — Mathlib

English

For k ≠ 0, the integral of bernoulliFun k over [0,1] is zero.

Русский

Для k ≠ 0 интеграл bernoulliFun k по [0,1] равен нулю.

LaTeX

$$$$ \\int_{0}^{1} bernoulliFun(k)(x) \\, dx = 0 \\quad (k \\neq 0). $$$$

Lean4

theorem integral_bernoulliFun_eq_zero {k : ℕ} (hk : k ≠ 0) : ∫ x : ℝ in 0..1, bernoulliFun k x = 0 :=
  by
  rw [integral_eq_sub_of_hasDerivAt (fun x _ => antideriv_bernoulliFun k x)
      ((Polynomial.continuous _).intervalIntegrable _ _)]
  rw [bernoulliFun_eval_one]
  split_ifs with h
  · exfalso; exact hk (Nat.succ_inj.mp h)
  · simp

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