Analysis of Boolean Functions in Lean

1.6. Highlight: Almost linear functions and the BLR Test🔗

Definition1.6.1
uses 0used by 1✓L∃∀N
Tagssection-1-6fidelity-exact

Definition 1.28. A function f:\mathbb F_2^n\to\mathbb F_2 is linear if either of the following equivalent conditions holds:

  1. f(x+y)=f(x)+f(y) for all x,y\in\mathbb F_2^n;

  2. There is some a\in\mathbb F_2^n such that f(x)=a\mathbin{\cdot}x for every x\in\mathbb F_2^n; equivalently, there is some S\subseteq[n] such that f(x)=\sum_{i\in S}x_i for every x\in\mathbb F_2^n.

Lean code for Definition1.6.1●4 declarations
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.IsF₂Linear {n : ℕ} (f : FABL.F₂Cube n → FABL.𝔽₂) : Prop
    def FABL.IsF₂Linear {n : ℕ}
  (f : FABL.F₂Cube n → FABL.𝔽₂) : Prop
    O'Donnell, Definition 1.28, condition (1): additivity of an `𝔽₂`-valued function.
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.f₂DotProduct {n : ℕ} (a x : FABL.F₂Cube n) : FABL.𝔽₂
    def FABL.f₂DotProduct {n : ℕ}
  (a x : FABL.F₂Cube n) : FABL.𝔽₂
    The standard dot product on `𝔽₂ⁿ`.
  • theoremdefined in FABL/Chapter01/BLR.lean
    complete
    theorem FABL.isF₂Linear_iff_exists_dotProduct {n : ℕ}
  (f : FABL.F₂Cube n → FABL.𝔽₂) :
  FABL.IsF₂Linear f ↔
    ∃ a, ∀ (x : FABL.F₂Cube n), f x = FABL.f₂DotProduct a x
    theorem FABL.isF₂Linear_iff_exists_dotProduct
  {n : ℕ} (f : FABL.F₂Cube n → FABL.𝔽₂) :
  FABL.IsF₂Linear f ↔
    ∃ a,
      ∀ (x : FABL.F₂Cube n),
        f x = FABL.f₂DotProduct a x
    O'Donnell, Definition 1.28: the additive and dot-product descriptions of linear functions are
equivalent. The book delegates this obligation to Exercise 1.26.
  • theoremdefined in FABL/Chapter01/BLR.lean
    complete
    theorem FABL.isF₂Linear_iff_exists_coordinateSum {n : ℕ}
  (f : FABL.F₂Cube n → FABL.𝔽₂) :
  FABL.IsF₂Linear f ↔
    ∃ S, ∀ (x : FABL.F₂Cube n), f x = (FABL.coordinateSum S) x
    theorem FABL.isF₂Linear_iff_exists_coordinateSum
  {n : ℕ} (f : FABL.F₂Cube n → FABL.𝔽₂) :
  FABL.IsF₂Linear f ↔
    ∃ S,
      ∀ (x : FABL.F₂Cube n),
        f x = (FABL.coordinateSum S) x
    The subset-coordinate-sum form of O'Donnell's Definition 1.28.
Definition1.6.2
uses 1
Used by 3
Reverse dependency previews
Preview
Theorem 1.6.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-6fidelity-conservative-generalization-of-common-codomain

Definition 1.29. If f and g are Boolean-valued functions, they are \epsilon-close if \operatorname{dist}(f,g)\le\epsilon; otherwise they are \epsilon-far. If \mathcal P is a nonempty property of n-bit Boolean functions, define \operatorname{dist}(f,\mathcal P) =\min_{g\in\mathcal P}\operatorname{dist}(f,g). The function f is \epsilon-close to \mathcal P if \operatorname{dist}(f,\mathcal P)\le\epsilon; equivalently, if it is \epsilon-close to some g\in\mathcal P.

Lean code for Definition1.6.2●6 declarations
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.IsClose.{u_1, u_2} {Ω : Type u_1} {β : Type u_2} [Fintype Ω]
  [Nonempty Ω] [DecidableEq β] (ε : ℝ) (f g : Ω → β) : Prop
    def FABL.IsClose.{u_1, u_2} {Ω : Type u_1}
  {β : Type u_2} [Fintype Ω] [Nonempty Ω]
  [DecidableEq β] (ε : ℝ) (f g : Ω → β) :
  Prop
    O'Donnell, Definition 1.29: `f` and `g` are `ε`-close.
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.IsFar.{u_1, u_2} {Ω : Type u_1} {β : Type u_2} [Fintype Ω]
  [Nonempty Ω] [DecidableEq β] (ε : ℝ) (f g : Ω → β) : Prop
    def FABL.IsFar.{u_1, u_2} {Ω : Type u_1}
  {β : Type u_2} [Fintype Ω] [Nonempty Ω]
  [DecidableEq β] (ε : ℝ) (f g : Ω → β) :
  Prop
    O'Donnell, Definition 1.29: `f` and `g` are `ε`-far.
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.distanceToProperty.{u_1, u_2} {Ω : Type u_1} {β : Type u_2}
  [Fintype Ω] [Nonempty Ω] [Finite β] [DecidableEq β] (f : Ω → β)
  (P : (Ω → β) → Prop) (hP : ∃ g, P g) : ℝ
    def FABL.distanceToProperty.{u_1, u_2}
  {Ω : Type u_1} {β : Type u_2}
  [Fintype Ω] [Nonempty Ω] [Finite β]
  [DecidableEq β] (f : Ω → β)
  (P : (Ω → β) → Prop) (hP : ∃ g, P g) : ℝ
    Distance from `f` to a nonempty property of finite-domain functions.
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.IsCloseToProperty.{u_1, u_2} {Ω : Type u_1} {β : Type u_2}
  [Fintype Ω] [Nonempty Ω] [DecidableEq β] (ε : ℝ) (f : Ω → β)
  (P : (Ω → β) → Prop) : Prop
    def FABL.IsCloseToProperty.{u_1, u_2}
  {Ω : Type u_1} {β : Type u_2}
  [Fintype Ω] [Nonempty Ω] [DecidableEq β]
  (ε : ℝ) (f : Ω → β)
  (P : (Ω → β) → Prop) : Prop
    Being close to a property, in the existential form stated in Definition 1.29.
  • theoremdefined in FABL/Chapter01/BLR.lean
    complete
    theorem FABL.exists_relativeHammingDist_eq_distanceToProperty.{u_1, u_2}
  {Ω : Type u_1} {β : Type u_2} [Fintype Ω] [Nonempty Ω] [Finite β]
  [DecidableEq β] (f : Ω → β) (P : (Ω → β) → Prop) (hP : ∃ g, P g) :
  ∃ g,
    P g ∧ FABL.relativeHammingDist f g = FABL.distanceToProperty f P hP
    theorem FABL.exists_relativeHammingDist_eq_distanceToProperty.{u_1,
    u_2}
  {Ω : Type u_1} {β : Type u_2}
  [Fintype Ω] [Nonempty Ω] [Finite β]
  [DecidableEq β] (f : Ω → β)
  (P : (Ω → β) → Prop) (hP : ∃ g, P g) :
  ∃ g,
    P g ∧
      FABL.relativeHammingDist f g =
        FABL.distanceToProperty f P hP
    The minimum defining distance to a property is attained.
  • theoremdefined in FABL/Chapter01/BLR.lean
    complete
    theorem FABL.isCloseToProperty_iff_distanceToProperty_le.{u_1, u_2}
  {Ω : Type u_1} {β : Type u_2} [Fintype Ω] [Nonempty Ω] [Finite β]
  [DecidableEq β] (ε : ℝ) (f : Ω → β) (P : (Ω → β) → Prop)
  (hP : ∃ g, P g) :
  FABL.IsCloseToProperty ε f P ↔ FABL.distanceToProperty f P hP ≤ ε
    theorem FABL.isCloseToProperty_iff_distanceToProperty_le.{u_1,
    u_2}
  {Ω : Type u_1} {β : Type u_2}
  [Fintype Ω] [Nonempty Ω] [Finite β]
  [DecidableEq β] (ε : ℝ) (f : Ω → β)
  (P : (Ω → β) → Prop) (hP : ∃ g, P g) :
  FABL.IsCloseToProperty ε f P ↔
    FABL.distanceToProperty f P hP ≤ ε
    The existential and minimum-distance formulations of closeness to a property agree.
Definition1.6.3
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 1.6.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-6fidelity-exact

BLR Test. Given query access to f:\mathbb F_2^n\to\mathbb F_2:

  1. Choose independent uniform \boldsymbol{x},\boldsymbol{y}\in\mathbb F_2^n.

  2. Query f at \boldsymbol{x}, \boldsymbol{y}, and \boldsymbol{x}+\boldsymbol{y}.

  3. Accept if f(\boldsymbol{x})+f(\boldsymbol{y})=f(\boldsymbol{x}+\boldsymbol{y}).

Lean code for Definition1.6.3●2 definitions
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.blrAccepts {n : ℕ} (f : FABL.F₂Cube n → FABL.𝔽₂)
  (x y : FABL.F₂Cube n) : Prop
    def FABL.blrAccepts {n : ℕ}
  (f : FABL.F₂Cube n → FABL.𝔽₂)
  (x y : FABL.F₂Cube n) : Prop
    The acceptance predicate of the named BLR Test.
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.blrAcceptanceProbability {n : ℕ} (f : FABL.F₂Cube n → FABL.𝔽₂) : ℝ
    def FABL.blrAcceptanceProbability {n : ℕ}
  (f : FABL.F₂Cube n → FABL.𝔽₂) : ℝ
    The acceptance probability of the BLR Test under independent uniform `x,y`.
Lemma1.6.4
Statement uses 3
Statement dependency previews
Preview
Theorem 1.4.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-1-6support

Equation (1.10). If f:\mathbb F_2^n\to\mathbb F_2 and F is its \{-1,1\}-valued encoding, then 2\Pr[\text{BLR accepts }f]-1 =\sum_{S\subseteq[n]}\widehat F(S)^3.

Lean code for Lemma1.6.4●4 declarations
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.signEncode (b : FABL.𝔽₂) : FABL.Sign
    def FABL.signEncode (b : FABL.𝔽₂) : FABL.Sign
    Encode `0,1 ∈ 𝔽₂` as `1,-1 ∈ Sign`.
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.realSignEncodedFunction {n : ℕ} (f : FABL.F₂Cube n → FABL.𝔽₂) :
  FABL.F₂Cube n → ℝ
    def FABL.realSignEncodedFunction {n : ℕ}
  (f : FABL.F₂Cube n → FABL.𝔽₂) :
  FABL.F₂Cube n → ℝ
    The real-valued sign encoding used by the Fourier proof of BLR.
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.binaryParitySign {n : ℕ} (S : Finset (Fin n)) :
  FABL.F₂Cube n → FABL.Sign
    def FABL.binaryParitySign {n : ℕ}
  (S : Finset (Fin n)) :
  FABL.F₂Cube n → FABL.Sign
    The sign-valued parity indexed by `S`.
  • theoremdefined in FABL/Chapter01/BLR.lean
    complete
    theorem FABL.two_mul_blrAcceptanceProbability_sub_one_eq_sum_cube_fourierCoeff
  {n : ℕ} (f : FABL.F₂Cube n → FABL.𝔽₂) :
  2 * FABL.blrAcceptanceProbability f - 1 =
    ∑ S, FABL.binaryFourierCoeff (FABL.realSignEncodedFunction f) S ^ 3
    theorem FABL.two_mul_blrAcceptanceProbability_sub_one_eq_sum_cube_fourierCoeff
  {n : ℕ} (f : FABL.F₂Cube n → FABL.𝔽₂) :
  2 * FABL.blrAcceptanceProbability f -
      1 =
    ∑ S,
      FABL.binaryFourierCoeff
          (FABL.realSignEncodedFunction f)
          S ^
        3
    Equation (1.10) in the proof of O'Donnell, Theorem 1.30, in its natural acceptance-probability
form.
Theorem1.6.5
Statement uses 8
Statement dependency previews
Preview
Theorem 1.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-1-6fidelity-exact

Theorem 1.30. Suppose the BLR Test accepts f:\mathbb F_2^n\to\mathbb F_2 with probability 1-\epsilon. Then f is \epsilon-close to being linear.

Lean code for Theorem1.6.5●1 theorem
  • theoremdefined in FABL/Chapter01/BLR.lean
    complete
    theorem FABL.close_to_linear_of_blrAcceptanceProbability_eq {n : ℕ}
  (f : FABL.F₂Cube n → FABL.𝔽₂) (ε : ℝ)
  (haccept : FABL.blrAcceptanceProbability f = 1 - ε) :
  FABL.IsCloseToProperty ε f FABL.IsF₂Linear
    theorem FABL.close_to_linear_of_blrAcceptanceProbability_eq
  {n : ℕ} (f : FABL.F₂Cube n → FABL.𝔽₂)
  (ε : ℝ)
  (haccept :
    FABL.blrAcceptanceProbability f =
      1 - ε) :
  FABL.IsCloseToProperty ε f
    FABL.IsF₂Linear
    O'Donnell, Theorem 1.30: high BLR acceptance implies closeness to a linear function.
Proposition1.6.6
Statement uses 2
Statement dependency previews
Preview
Definition 1.2.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-1-6fidelity-exact-pointwise-quantifier-order

Proposition 1.31. Suppose f:\mathbb F_2^n\to\{-1,1\} is \epsilon-close to the linear function \chi_S. Then, for every x\in\mathbb F_2^n, the following algorithm outputs \chi_S(x) with probability at least 1-2\epsilon:

  1. Choose uniform \boldsymbol{y}\in\mathbb F_2^n.

  2. Query f at \boldsymbol{y} and x+\boldsymbol{y}.

  3. Output f(\boldsymbol{y})f(x+\boldsymbol{y}).

The probability bound holds for every requested x.

Lean code for Proposition1.6.6●2 declarations
  • defdefined in FABL/Chapter01/BLR.lean
    complete
    def FABL.localCorrection {n : ℕ} (f : FABL.F₂Cube n → FABL.Sign)
  (x y : FABL.F₂Cube n) : FABL.Sign
    def FABL.localCorrection {n : ℕ}
  (f : FABL.F₂Cube n → FABL.Sign)
  (x y : FABL.F₂Cube n) : FABL.Sign
    The two-query local correction procedure from O'Donnell, Proposition 1.31.
  • theoremdefined in FABL/Chapter01/BLR.lean
    complete
    theorem FABL.localCorrection_successProbability {n : ℕ}
  (f : FABL.F₂Cube n → FABL.Sign) (S : Finset (Fin n)) (ε : ℝ)
  (hclose : FABL.IsClose ε f (FABL.binaryParitySign S))
  (x : FABL.F₂Cube n) :
  1 - 2 * ε ≤
    FABL.uniformProbability fun y =>
      FABL.localCorrection f x y = FABL.binaryParitySign S x
    theorem FABL.localCorrection_successProbability
  {n : ℕ} (f : FABL.F₂Cube n → FABL.Sign)
  (S : Finset (Fin n)) (ε : ℝ)
  (hclose :
    FABL.IsClose ε f
      (FABL.binaryParitySign S))
  (x : FABL.F₂Cube n) :
  1 - 2 * ε ≤
    FABL.uniformProbability fun y =>
      FABL.localCorrection f x y =
        FABL.binaryParitySign S x
    O'Donnell, Proposition 1.31. The quantifier order is pointwise in the requested input `x`.