Documentation

Complexity.Foundations.Data.BitString.Sign

Bits as numbers: 0/1 values and ±1 signs #

Analysis on the Boolean cube reads a bit in two ways. As a value in a commutative ring R, a bit is 0 or 1 (BitString.bitVal); this is the reading of multilinear polynomials and of 𝔽₂. As a real sign, a bit is 1 or -1 (BitString.signVal), with false ↦ 1 and true ↦ -1; this is the reading of Fourier analysis, under which exclusive or becomes multiplication (BitString.signVal_xor) O'Donnell, Chapter 1. The two readings are related by signVal b = 1 - 2 bitVal b (BitString.signVal_eq_one_sub_two_mul_bitVal).

This module holds only these atoms, so that modules which read bits as numbers need not import the Fourier or low-degree theory built on them.

Main definitions #

Main results #

References #

Bits read as 0 or 1 #

source
def Cslib.BitString.bitVal (R : Type u_1) [CommRing R] (b : Bool) :
R

A bit read as 0 or 1 in R.

Instances For
    source
    @[simp]
    theorem Cslib.BitString.bitVal_true {R : Type u_1} [CommRing R] :
    bitVal R true = 1

    The bit true reads as 1.

    source
    @[simp]
    theorem Cslib.BitString.bitVal_false {R : Type u_1} [CommRing R] :
    bitVal R false = 0

    The bit false reads as 0.

    source
    theorem Cslib.BitString.bitVal_pow {R : Type u_1} [CommRing R] (b : Bool) {k : ℕ} (hk : k ≠ 0) :
    bitVal R b ^ k = bitVal R b

    A bit read in R is idempotent.

    source
    theorem Cslib.BitString.bitVal_not {R : Type u_1} [CommRing R] (b : Bool) :
    (bitVal R !b) = 1 - bitVal R b

    Negating a bit sends its value v in R to 1 - v.

    Bits read as signs #

    source
    def Cslib.BitString.signVal (b : Bool) :
    ℝ

    A bit read as a real sign: false ↦ 1 and true ↦ -1.

    Instances For
      source
      @[simp]
      theorem Cslib.BitString.signVal_false :
      signVal false = 1

      The bit false reads as the sign 1.

      source
      @[simp]
      theorem Cslib.BitString.signVal_true :
      signVal true = -1

      The bit true reads as the sign -1.

      source
      @[simp]
      theorem Cslib.BitString.signVal_not (b : Bool) :
      (signVal !b) = -signVal b

      Negating a bit negates its sign.

      source
      theorem Cslib.BitString.signVal_mul_self (b : Bool) :
      signVal b * signVal b = 1

      A sign squares to one.

      source
      @[simp]
      theorem Cslib.BitString.abs_signVal (b : Bool) :
      |signVal b| = 1

      A sign has absolute value one.

      source
      theorem Cslib.BitString.signVal_mul_signVal (a b : Bool) :
      signVal a * signVal b = if a = b then 1 else -1

      The product of two signs records whether the bits agree.

      source
      @[simp]
      theorem Cslib.BitString.signVal_xor (a b : Bool) :
      signVal (a ^^ b) = signVal a * signVal b

      The sign of an exclusive or is the product of the signs.

      source
      theorem Cslib.BitString.sq_signVal_sub_signVal (a b : Bool) :
      (signVal a - signVal b) ^ 2 = 2 - 2 * (signVal a * signVal b)

      The squared difference of two signs is two minus twice their product.

      source
      theorem Cslib.BitString.signVal_eq_neg_one_pow (b : Bool) :
      signVal b = (-1) ^ b.toNat

      The real sign of a bit as a power of -1.

      Signs as powers of -1 in a commutative ring #

      source
      theorem Cslib.BitString.neg_one_pow_toNat_xor {R : Type u_1} [CommRing R] (a b : Bool) :
      (-1) ^ (a ^^ b).toNat = (-1) ^ a.toNat * (-1) ^ b.toNat

      The sign (-1) ^ b of an exclusive or is the product of the signs.

      source
      theorem Cslib.BitString.neg_one_pow_toNat_eq_one_sub_two_mul_bitVal {R : Type u_1} [CommRing R] (b : Bool) :
      (-1) ^ b.toNat = 1 - 2 * bitVal R b

      The sign (-1) ^ b of a bit, as a polynomial in the bit: 1 - 2 b.

      source
      theorem Cslib.BitString.signVal_eq_one_sub_two_mul_bitVal (b : Bool) :
      signVal b = 1 - 2 * bitVal ℝ b

      The real sign of a bit is 1 - 2 b for the bit b read as 0 or 1.