zeta_mul_pow_eq_sigma — Mathlib

English

For all k, the convolution with zeta of pow k equals σ_k: ζ * pow(k) = σ_k.

Русский

Для любого k выполняется: ζ * pow(k) = σ_k (посредством свёртки) .

LaTeX

$$$ \zeta * \mathrm{pow}(k) = \sigma_k $$$

Lean4

theorem zeta_mul_pow_eq_sigma {k : ℕ} : ζ * pow k = σ k :=
  by
  ext
  rw [sigma, zeta_mul_apply]
  apply sum_congr rfl
  intro x hx
  rw [pow_apply, if_neg (not_and_of_not_right _ _)]
  contrapose! hx
  simp [hx]

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