Decomposition of the bit-swap permutation matrix

DefinitionAntisymmetric two-bit singlet vector#✓fully proved

The unnormalized antisymmetric two-bit vector, in order 00, 01, 10, 11.

def bitSinglet (p : Bool × Bool) : ℤ :=
  if p.1 = p.2 then 0 else if p.1 then -1 else 1

Used by 5

Used byBinomial entry bound for bit-swap pieces · One-bit swap matrix as identity minus singlet outer product · Piece of an n-bit swap with i antisymmetric factors · Bit-swap pieces vanish beyond the number of bits · Bit-swap pieces sum to the swap permutation matrix

TheoremOne-bit swap matrix as identity minus singlet outer product#✓fully proved

The one-bit swap matrix is the identity minus the singlet outer product.

theorem bitSwap_eq_one_sub_vecMulVec :
    (Equiv.prodComm Bool Bool).toPEquiv.toMatrix =
      (1 : Matrix (Bool × Bool) (Bool × Bool) ℤ) - vecMulVec bitSinglet bitSinglet

Uses 1 · Used by 1

Statement usesAntisymmetric two-bit singlet vector

Used byBit-swap pieces sum to the swap permutation matrix

DefinitionPiece of an n-bit swap with i antisymmetric factors#✓fully proved

The part of an n-bit swap with exactly i antisymmetric factors.

def bitSwapPiece (n i : ℕ) :
    Matrix ((Fin n → Bool) × (Fin n → Bool)) ((Fin n → Bool) × (Fin n → Bool)) ℤ :=
  fun p q => ∑ S ∈ powersetCard i (univ : Finset (Fin n)),
    (∏ k ∈ S, -(bitSinglet (p.1 k, p.2 k) * bitSinglet (q.1 k, q.2 k))) *
      ∏ k ∈ Sᶜ, (1 : Matrix (Bool × Bool) (Bool × Bool) ℤ)
        (p.1 k, p.2 k) (q.1 k, q.2 k)

Uses 1 · Used by 4

Statement usesAntisymmetric two-bit singlet vector

Used byBinomial entry bound for bit-swap pieces · Uniform power-of-two entry bound for bit-swap pieces · Bit-swap pieces vanish beyond the number of bits · Bit-swap pieces sum to the swap permutation matrix

TheoremBit-swap pieces sum to the swap permutation matrix#✓fully proved

The n + 1 grouped pieces sum to the permutation matrix swapping the two bit strings.

theorem sum_bitSwapPiece (n : ℕ) (p q : (Fin n → Bool) × (Fin n → Bool)) :
    ∑ i ∈ range (n + 1), bitSwapPiece n i p q =
      (Equiv.prodComm (Fin n → Bool) (Fin n → Bool)).toPEquiv.toMatrix p q

Uses 3

Statement usesPiece of an n-bit swap with i antisymmetric factors

Proof usesAntisymmetric two-bit singlet vector · One-bit swap matrix as identity minus singlet outer product

TheoremBit-swap pieces vanish beyond the number of bits#✓fully proved

There is no piece containing more antisymmetric factors than bit positions.

theorem bitSwapPiece_eq_zero_of_lt {n i : ℕ} (h : n < i) : bitSwapPiece n i = 0

Uses 2

Statement usesPiece of an n-bit swap with i antisymmetric factors

Proof usesAntisymmetric two-bit singlet vector

TheoremBinomial entry bound for bit-swap pieces#✓fully proved

Each entry of the ith piece is bounded by the number of i-subsets of the bit positions.

theorem abs_bitSwapPiece_le_choose (n i : ℕ) (p q : (Fin n → Bool) × (Fin n → Bool)) :
    |bitSwapPiece n i p q| ≤ (n.choose i : ℤ)

Uses 2 · Used by 1

Statement usesPiece of an n-bit swap with i antisymmetric factors

Proof usesAntisymmetric two-bit singlet vector

Used byUniform power-of-two entry bound for bit-swap pieces

TheoremUniform power-of-two entry bound for bit-swap pieces#✓fully proved

The uniform entry bound used in the source: every piece has absolute value at most 2 ^ n.

theorem abs_bitSwapPiece_le_two_pow (n i : ℕ)
    (p q : (Fin n → Bool) × (Fin n → Bool)) : |bitSwapPiece n i p q| ≤ 2 ^ n

Uses 2

Statement usesPiece of an n-bit swap with i antisymmetric factors

Proof usesBinomial entry bound for bit-swap pieces

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.