Parity products modulo powers of two

DefinitionEven indicator of a natural number#✓fully proved

The integer indicator that a natural number is even.

def evenIndicator (q : ℕ) : ℤ := if Even q then 1 else 0

Used by 3

Used byTruncated subset expansion of parity products modulo powers of two · Subset sum of parity coefficients is the even-cardinality indicator · Twice the even indicator is one plus the parity sign

DefinitionCoefficients of the even-indicator expansion#✓fully proved

The coefficients of the even-indicator expansion: one at zero and (-1) ^ i * 2 ^ (i - 1) at positive indices.

def parityCoeff (i : ℕ) : ℤ := if i = 0 then 1 else (-1) ^ i * 2 ^ (i - 1)

Used by 3

Used byTruncated subset expansion of parity products modulo powers of two · Subset sum of parity coefficients is the even-cardinality indicator · Twice a parity coefficient is a sign coefficient

TheoremTwice a parity coefficient is a sign coefficient#✓fully proved

Twice the parity coefficient is the sign coefficient, with a correction at zero.

theorem two_mul_parityCoeff (i : ℕ) :
    2 * parityCoeff i = (-2) ^ i + if i = 0 then 1 else 0

Uses 1 · Used by 1

Statement usesCoefficients of the even-indicator expansion

Used bySubset sum of parity coefficients is the even-cardinality indicator

TheoremTwice the even indicator is one plus the parity sign#✓fully proved

Twice the even indicator is one plus the parity sign.

theorem two_mul_evenIndicator (q : ℕ) : 2 * evenIndicator q = 1 + (-1) ^ q

Uses 1 · Used by 1

Statement usesEven indicator of a natural number

Used bySubset sum of parity coefficients is the even-cardinality indicator

TheoremSubset sum of parity coefficients is the even-cardinality indicator#✓fully proved

Summing parity coefficients over all subsets gives the even-cardinality indicator.

theorem sum_powerset_parityCoeff {E : Type*} (A : Finset E) :
    ∑ s ∈ A.powerset, parityCoeff #s = evenIndicator #A

Uses 4 · Used by 1

Statement usesEven indicator of a natural number · Coefficients of the even-indicator expansion

Proof usesTwice the even indicator is one plus the parity sign · Twice a parity coefficient is a sign coefficient

Used byTruncated subset expansion of parity products modulo powers of two

TheoremTruncated subset expansion of parity products modulo powers of two#✓fully proved

A product of even-cardinality indicators and parity signs is congruent to its finite subset expansion cut off at total degree M. Each even-indicator factor costs at most one power of two, so the cutoff must satisfy ν - 1 + #J₁ ≤ M, with 1 ≤ ν. Indices outside J₁ ∪ J₂ select only the empty subset.

theorem prod_evenIndicator_mul_prod_neg_one_pow_modEq {J₁ J₂ : Finset (Fin r)}
    (hJ : Disjoint J₁ J₂) (A : Fin r → Finset E) {ν M : ℕ} (hν : 1 ≤ ν)
    (hM : ν - 1 + #J₁ ≤ M) :
    (∏ j ∈ J₁, evenIndicator #(A j)) * ∏ j ∈ J₂, (-1 : ℤ) ^ #(A j) ≡
      ∑ S ∈ (Fintype.piFinset fun j : Fin r =>
        if j ∈ J₁ ∪ J₂ then (A j).powerset else {∅}).filter (fun S => ∑ j, #(S j) ≤ M),
        (∏ j ∈ J₁, parityCoeff #(S j)) * ∏ j ∈ J₂, (-2 : ℤ) ^ #(S j)
      [ZMOD 2 ^ ν]

Uses 3

Statement usesEven indicator of a natural number · Coefficients of the even-indicator expansion

Proof usesSubset sum of parity coefficients is the even-cardinality indicator

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.