siftedSum_eq_sum_support_mul_ite — Mathlib

English

The sifted sum equals the sum over the support of weights times the indicator that gcd(prodPrimes, d) = 1.

Русский

Сдвинутый сумма равна сумме по поддержке весов, умноженной на индикатор, что gcd(prodPrimes, d) = 1.

LaTeX

$$siftedSum = ∑_{d ∈ s.support} s.weights(d) · [\\gcd(s.prodPrimes, d) = 1]$$

Lean4

theorem siftedSum_eq_sum_support_mul_ite :
    s.siftedSum = ∑ d ∈ s.support, s.weights d * if Nat.gcd s.prodPrimes d = 1 then 1 else 0 :=
  by
  dsimp only [siftedSum]
  simp_rw [mul_ite, mul_one, mul_zero]

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