Sparse Ball Cardinality Formula

Explicit formula for the cardinality of sparseBallCeil d k x in terms of binomial coefficients.

For a k-sparse binary vector x in {0,1}^d, the ball of radius < ⌈k/2⌉ around x has cardinality: |ball(x)| = Σ_{j=0}^{R-1} C(k,j) · C(d-k,j) where R = (k+3)/4 (in ℕ).

The proof constructs a bijection between ball elements and pairs (J, K) where J ⊆ supp(x) with |J| = j, K ⊆ supp(x)ᶜ with |K| = j.

def SparseVarshamovGilbert.boolSupport {d : ℕ} (x : Fin d → Bool) : Finset (Fin d)

Support of a binary vector as a Finset.

def SparseVarshamovGilbert.flipVec {d : ℕ} (x : Fin d → Bool) (J K : Finset (Fin d)) : Fin d → Bool

Flip operation: given x, set positions in J to false and positions in K to true.

theorem SparseVarshamovGilbert.boolSupport_card {d k : ℕ} (x : SparseVec d k) : (boolSupport ↑x).card = k

Support of x equals its filter set, which has cardinality l0norm.

theorem SparseVarshamovGilbert.compl_boolSupport_card {d k : ℕ} (hkd : k ≤ d) (x : SparseVec d k) : (Finset.univ \ boolSupport ↑x).card = d - k

Complement of support has cardinality d - k.

theorem SparseVarshamovGilbert.disjoint_of_support_subsets {d : ℕ} {x : Fin d → Bool} {J K : Finset (Fin d)} (hJ : J ⊆ boolSupport x) (hK : K ⊆ Finset.univ \ boolSupport x) : Disjoint J K

J ⊆ support(x) and K ⊆ complement implies J and K are disjoint.

theorem SparseVarshamovGilbert.boolSupport_flipVec {d : ℕ} (x : Fin d → Bool) (J K : Finset (Fin d)) (hDisj : Disjoint J K) : boolSupport (flipVec x J K) = boolSupport x \ J ∪ K

support(flipVec x J K) = (support x \ J) ∪ K.

theorem SparseVarshamovGilbert.flipVec_preserves_l0norm {d : ℕ} (x : Fin d → Bool) (J K : Finset (Fin d)) (hJ : J ⊆ boolSupport x) (hK : K ⊆ Finset.univ \ boolSupport x) (hJK : J.card = K.card) : l0norm (flipVec x J K) = l0norm x

flipVec preserves l0norm when J ⊆ support, K ⊆ complement, |J| = |K|.

theorem SparseVarshamovGilbert.disagree_eq_union {d : ℕ} (x : Fin d → Bool) (J K : Finset (Fin d)) (hJ : J ⊆ boolSupport x) (hK : K ⊆ Finset.univ \ boolSupport x) : {i : Fin d | x i ≠ flipVec x J K i} = J ∪ K

The positions where x and flipVec x J K differ are exactly J ∪ K.

theorem SparseVarshamovGilbert.hammingDist_of_flipVec {d : ℕ} (x : Fin d → Bool) (J K : Finset (Fin d)) (hJ : J ⊆ boolSupport x) (hK : K ⊆ Finset.univ \ boolSupport x) (hDisj : Disjoint J K) : hammingDist x (flipVec x J K) = J.card + K.card

hammingDist between x and flipVec x J K equals |J| + |K|.

theorem SparseVarshamovGilbert.flipVec_reconstructs {d : ℕ} (x y : Fin d → Bool) : flipVec x (boolSupport x \ boolSupport y) (boolSupport y \ boolSupport x) = y

Reconstruction: any y equals flipVec x J K where J = supp(x)\supp(y), K = supp(y)\supp(x).

theorem SparseVarshamovGilbert.sdiff_boolSupport_card_eq {d k : ℕ} (x y : Fin d → Bool) (hx : l0norm x = k) (hy : l0norm y = k) : (boolSupport x \ boolSupport y).card = (boolSupport y \ boolSupport x).card

For equal-weight vectors, |supp(x)\supp(y)| = |supp(y)\supp(x)|.

theorem SparseVarshamovGilbert.hammingDist_eq_two_mul_sdiff {d k : ℕ} (x y : Fin d → Bool) (hx : l0norm x = k) (hy : l0norm y = k) : hammingDist x y = 2 * (boolSupport x \ boolSupport y).card

For equal-weight vectors, hammingDist = 2 * |supp(x)\supp(y)|.

theorem SparseVarshamovGilbert.sparse_ball_card (d k : ℕ) (_hk : 0 < k) (hkd : k ≤ d) (x : SparseVec d k) : (sparseBallCeil d k x).card = ∑ j ∈ Finset.range ((k + 3) / 4), k.choose j * (d - k).choose j

The ball size formula: |sparseBallCeil d k x| = Σ_{j<R} C(k,j)·C(d-k,j) where R = (k+3)/4.

The constraint hammingDist < (k+1)/2 with hammingDist = 2j yields j < (k+3)/4.