Parity counts over finite fields

TheoremLower bound on odd-parity pairs in a finite field#✓fully proved

Let a finite field be written as s binary coordinates. For a nonempty set V of exponents below m, the number of pairs (a, b) for which an odd number of the dot products bits (a ^ E) ⬝ᵥ bits b equal one satisfies the cleared-denominator lower bound

|F| ^ 2 ≤ 2 * oddPairs + (m - 1) * |F|.

This is a one-sided odd-frequency estimate.

theorem odd_dotProduct_power_count
    (bits : F ≃ₗ[ZMod 2] (Fin s → ZMod 2))
    (V : Finset (Fin m)) (hV : V.Nonempty) :
    Fintype.card F ^ 2 ≤
      2 * #{p : F × F |
        Odd #{E ∈ V |
          dotProduct (bits (p.1 ^ E.val)) (bits p.2) = 1}} +
        (m - 1) * Fintype.card F

Used by 1

Used byAt least 15/32 of field pairs have odd parity

TheoremAt least 15/32 of field pairs have odd parity#✓fully proved

Under 16 * m ≤ 2 ^ s, at least 15 / 32 of the field pairs have odd parity across any nonempty exponent set V. Fractions are cleared in the statement.

theorem odd_dotProduct_power_count_of_sixteen_mul_le
    (bits : F ≃ₗ[ZMod 2] (Fin s → ZMod 2))
    (h16 : 16 * m ≤ 2 ^ s) (V : Finset (Fin m)) (hV : V.Nonempty) :
    15 * Fintype.card F ^ 2 ≤
      32 * #{p : F × F |
        Odd #{E ∈ V |
          dotProduct (bits (p.1 ^ E.val)) (bits p.2) = 1}}

Uses 1

Proof usesLower bound on odd-parity pairs in a finite field

TheoremAt most half of field pairs have dot product one#✓fully proved

For one exponent E, at most half of all field pairs satisfy dotProduct (bits (a ^ E)) (bits b) = 1.

theorem dotProduct_power_count_le_half
    (bits : F ≃ₗ[ZMod 2] (Fin s → ZMod 2)) (E : Fin m) :
    2 * #{p : F × F |
      dotProduct (bits (p.1 ^ E.val)) (bits p.2) = 1} ≤
        Fintype.card F ^ 2

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.