Analysis of Boolean Functions in Lean

1.1. On analysis of Boolean functions🔗

Definition1.1.1
uses 0used by 0✓L∃∀N
Tagssection-1-1support

Section 1.1. The sign representation of the Hamming cube is \{-1,1\}^n, and its additive representation is \mathbb F_2^n. For two strings x and y in a common product, their Hamming distance is \Delta(x,y)=\#\{i:x_i\ne y_i\}, the number of coordinates at which they differ.

Lean code for Definition1.1.1●3 definitions
  • abbrevdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    abbrev FABL.SignCube (n : ℕ) : Type
    abbrev FABL.SignCube (n : ℕ) : Type
    The sign cube `{-1, 1}ⁿ`.
  • abbrevdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    abbrev FABL.F₂Cube (n : ℕ) : Type
    abbrev FABL.F₂Cube (n : ℕ) : Type
    The additive Boolean cube `𝔽₂ⁿ`.
  • defdefined in Mathlib/InformationTheory/Hamming.lean
    complete
    def hammingDist.{u_2, u_3} {ι : Type u_2} {β : ι → Type u_3} [Fintype ι]
  [(i : ι) → DecidableEq (β i)] (x y : (i : ι) → β i) : ℕ
    def hammingDist.{u_2, u_3} {ι : Type u_2}
  {β : ι → Type u_3} [Fintype ι]
  [(i : ι) → DecidableEq (β i)]
  (x y : (i : ι) → β i) : ℕ
    The Hamming distance function to the naturals.