Boolean valued functions

This file introduces a typeclass BooleanValued for Boolean functions only taking values ±1 and proves some basic properties specific to Boolean-valued functions.

Main results

• eq_character_of_fourier_weight_one_eq_one, used in the proof of Arrow's theorem
• almost_character -- a theorem on BLR linearity testing

class LeanPool.LeanBooleanfun.BooleanFun.BooleanValued {n : ℕ} (f : BooleanFunc n) : Prop

BooleanValued f bundles a proof that f takes values ±1.

• one_or_neg_one (x : Fin n → Fin 2) : f x = 1 ∨ f x = -1

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.eq_one_or_eq_neg_one {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] (x : Fin n → Fin 2) : f x = 1 ∨ f x = -1

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.norm_sq_eq_one {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] : ‖f‖ ^ 2 = 1

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.fourier_eq_one {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] : ∑ S : Finset (Fin n), |fourierTransform f S| ^ 2 = 1

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.eq_neg_one_of_ne_one {n : ℕ} {f : BooleanFunc n} {x : Fin n → Fin 2} [hbv : BooleanValued f] (h' : f x ≠ 1) : f x = -1

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.eq_one_of_ne_neg_one {n : ℕ} {f : BooleanFunc n} {x : Fin n → Fin 2} [hbv : BooleanValued f] (h' : f x ≠ -1) : f x = 1

instance LeanPool.LeanBooleanfun.BooleanFun.BV.neg_boolean_valued {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] : BooleanValued (-f)

instance LeanPool.LeanBooleanfun.BooleanFun.BV.instBooleanValuedWalshCharacter {n : ℕ} (S : Finset (Fin n)) : BooleanValued (walshCharacter S)

Walsh characters are Boolean valued

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.eq_character_of_eq_sum_degree_one {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] (hn : n > 0) (hf : ∀ (x : Fin n → Fin 2), f x = ∑ i : Fin n, fourierTransform f {i} * (-1) ^ ↑(x i)) : ∃ S ∈ {S : Finset (Fin n) | S.card = 1}, ∃ (c : ℝ), f = c • walshCharacter S

A Boolean valued function that is a linear combination of degree one characters must be constant times a degree one character. Most involved step towards eq_character_of_fourier_weight_one_eq_one.

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.eq_character_of_fourier_weight_one_eq_one' {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] (hn : n > 0) (hf : fourierWeight 1 f = 1) : ∃ S ∈ {S : Finset (Fin n) | S.card = 1}, ∃ (c : ℝ), f = c • walshCharacter S

A Boolean valued function with degree one Fourier weight equal to one must be ±1 times a degree one character.

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.eq_character_of_fourier_weight_one_eq_one {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] (hn : n > 0) (hf : fourierWeight 1 f = 1) : ∃ (i : Fin n) (c : ℝ), f = c • walshCharacter {i}

A Boolean valued function with degree one Fourier weight equal to one must be ±1 times a degree one character. This is [odonnell2014], Exercise 1.19(a).

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.BV.distance {n : ℕ} (f g : BooleanFunc n) : ℝ

The Hamming distance of two Boolean-valued functions is equal to the proportion of inputs where they are not equal. The definition does not require f g be Boolean-valued, but it will only be used in this context.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.BV.distance f g = LeanPool.LeanBooleanfun.BooleanFun.expectation fun (x : Fin n → Fin 2) => LeanPool.LeanBooleanfun.BooleanFun.oneOn (f x ≠ g x)

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.oneOn_eq_of_one_or_neg_one {x y : ℝ} (hx : x = 1 ∨ x = -1) (hy : y = 1 ∨ y = -1) : oneOn (x = y) = 1 / 2 * (1 + x * y)

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.oneOn_ne_of_one_or_neg_one {x y : ℝ} (hx : x = 1 ∨ x = -1) (hy : y = 1 ∨ y = -1) : oneOn (x ≠ y) = 1 / 2 * (1 - x * y)

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.distance_eq {n : ℕ} {f g : BooleanFunc n} [hbv : BooleanValued f] [hbvg : BooleanValued g] : distance f g = expectation fun (x : Fin n → Fin 2) => 1 / 2 * (1 - f x * g x)

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.inner_eq_distance {n : ℕ} {f g : BooleanFunc n} [hbv : BooleanValued f] [hbvg : BooleanValued g] : inner ℝ f g = 1 - 2 * distance f g

We introduce the BLR "linearity" test [Blum, Luby, Rubinfeld][blr1990] following O'Donnell [odonnell2014], Sec. 1.6.

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.BV.acceptanceProbabilityBLR {n : ℕ} (f : BooleanFunc n) : ℝ

The BLR test accepts f on independently and uniformly chosen x y if (f x) * (f y) = f (x + y). The acceptance probability is the proportion of inputs x y on which the test accepts.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.acceptanceProbabilityBLR_eq {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] : acceptanceProbabilityBLR f = expectation fun (x : Fin n → Fin 2) => expectation fun (y : Fin n → Fin 2) => 1 / 2 * (1 + f x * f y * f (x + y))

theorem LeanPool.LeanBooleanfun.BooleanFun.BV.almost_character {n : ℕ} {f : BooleanFunc n} [hbv : BooleanValued f] {ε : ℝ} (h : acceptanceProbabilityBLR f ≥ 1 - ε) : ∃ (S : Finset (Fin n)), distance f (walshCharacter S) ≤ ε

The BLR test can detect that a Boolean valued function is close to being a character. See [odonnell2014], Theorem 1.30.