6.5. Highlight: Fooling F₂-polynomials
Definition 6.46. Let
\varphi:\mathbb F_2^n\to\mathbb R_{\ge0} be a probability density and let
\mathcal C be a class of functions
\mathbb F_2^n\to\mathbb R. The density \varphi
\epsilon-fools \mathcal C if
\left|
\mathbb E_{\boldsymbol y\sim\varphi}[f(\boldsymbol y)]
-\mathbb E_{\boldsymbol x\sim\mathbb F_2^n}[f(\boldsymbol x)]
\right|\le\epsilon
for every f\in\mathcal C.
Lean code for Definition6.5.1●1 definition
Associated Lean declarations
-
FABL.ProbabilityDensity.Fools[complete]
-
FABL.ProbabilityDensity.Fools[complete]
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/Fooling.leancomplete
def FABL.ProbabilityDensity.Fools {n : ℕ} (φ : FABL.ProbabilityDensity n) (C : Set (FABL.F₂Cube n → ℝ)) (ε : ℝ) : Prop
def FABL.ProbabilityDensity.Fools {n : ℕ} (φ : FABL.ProbabilityDensity n) (C : Set (FABL.F₂Cube n → ℝ)) (ε : ℝ) : Prop
O'Donnell, Definition 6.46: a density `ε`-fools a function class when each density-weighted expectation is within `ε` of the corresponding uniform expectation.
Example 6.47. Let n be even, let
\operatorname{IP}_n:\mathbb F_2^n\to\{0,1\} be the
inner-product-mod-2 function, and let \varphi be the density of the
uniform distribution on its support. The function
\operatorname{IP}_n has \mathbb F_2-degree 2, and \varphi is
roughly 2^{-n/2}-biased, but
\mathbb E_{\boldsymbol x\sim\mathbb F_2^n}
[\operatorname{IP}_n(\boldsymbol x)]
=\frac{1-2^{-n/2}}2,
\qquad
\mathbb E_{\boldsymbol y\sim\varphi}
[\operatorname{IP}_n(\boldsymbol y)]
=1.
Thus a small-biased density need not fool even all
\mathbb F_2-degree-2 functions.
Lean code for Lemma6.5.2●3 theorems
Associated Lean declarations
-
theoremdefined in FABL/Chapter06/Pseudorandomness/InnerProductSupportDensity.leancomplete
theorem FABL.expect_booleanRealEmbedding_innerProductModTwoBit (m : ℕ) : (Finset.univ.expect fun z => FABL.booleanRealEmbedding FABL.innerProductModTwoBit z) = (1 - (2 ^ m)⁻¹) / 2
theorem FABL.expect_booleanRealEmbedding_innerProductModTwoBit (m : ℕ) : (Finset.univ.expect fun z => FABL.booleanRealEmbedding FABL.innerProductModTwoBit z) = (1 - (2 ^ m)⁻¹) / 2
The exact uniform probability that inner product modulo two equals one.
-
theoremdefined in FABL/Chapter06/Pseudorandomness/InnerProductSupportDensity.leancomplete
theorem FABL.innerProductModTwoSupportDensity_expectation (m : ℕ) (hm : 0 < m) : (FABL.innerProductModTwoSupportDensity m hm).expectation (FABL.booleanRealEmbedding FABL.innerProductModTwoBit) = 1
theorem FABL.innerProductModTwoSupportDensity_expectation (m : ℕ) (hm : 0 < m) : (FABL.innerProductModTwoSupportDensity m hm).expectation (FABL.booleanRealEmbedding FABL.innerProductModTwoBit) = 1
Under the support density, inner product modulo two has expectation one.
-
theoremdefined in FABL/Chapter06/Pseudorandomness/InnerProductSupportDensity.leancomplete
theorem FABL.innerProductModTwoSupportDensity_expectation_gap (m : ℕ) (hm : 0 < m) : |(FABL.innerProductModTwoSupportDensity m hm).expectation (FABL.booleanRealEmbedding FABL.innerProductModTwoBit) - Finset.univ.expect fun z => FABL.booleanRealEmbedding FABL.innerProductModTwoBit z| = (1 + (2 ^ m)⁻¹) / 2
theorem FABL.innerProductModTwoSupportDensity_expectation_gap (m : ℕ) (hm : 0 < m) : |(FABL.innerProductModTwoSupportDensity m hm).expectation (FABL.booleanRealEmbedding FABL.innerProductModTwoBit) - Finset.univ.expect fun z => FABL.booleanRealEmbedding FABL.innerProductModTwoBit z| = (1 + (2 ^ m)⁻¹) / 2
Example 6.47: the support density and the uniform cube have the stated exact gap.
Luby--Veličković--Wigderson bound. There is a generator whose output
distribution \epsilon-fools every n-bit Boolean function of
\mathbb F_2-degree at most d and whose seed uses
\exp\!\left(
O\!\left(\sqrt{d\log(n/d)+\log(1/\epsilon)}\right)
\right)
independent random bits.
The book quotes this external result for historical comparison and does not prove it.
Bogdanov--Viola bounds. Boolean functions of \mathbb F_2-degree at most
2 can be \epsilon-fooled using O(\log(n/\epsilon)) independent
random bits. Those of degree at most 3 can be \epsilon-fooled using
O(\log n)+\exp(\operatorname{poly}(1/\epsilon))
independent random bits.
The book quotes these external bounds without proof.
Lovett's convolution bound. Let
\varphi:\mathbb F_2^n\to\mathbb R_{\ge0} be an
\epsilon-biased density. For every
f:\mathbb F_2^n\to\{-1,1\} with
\deg_{\mathbb F_2}(f)\le d,
\left|
\mathbb E_{\boldsymbol y^{(1)},\ldots,\boldsymbol y^{(2^d)}
\mathrel{\sim}\varphi}
\!\left[
f\!\left(\boldsymbol y^{(1)}+\cdots+\boldsymbol y^{(2^d)}\right)
\right]
-\mathbb E_{\boldsymbol x\sim\mathbb F_2^n}[f(\boldsymbol x)]
\right|
\le O\!\left(\epsilon^{\,1/4^d}\right).
Equivalently, the 2^d-fold convolution
\varphi^{*2^d} fools the class of
\mathbb F_2-degree-at-most-d Boolean functions, using
2^{O(d)}\log(n/\epsilon) random bits with a standard small-bias
construction.
The book quotes this external theorem without proof.
-
FABL.f₂PolynomialSignClass[complete] -
FABL.isTranslationClosed_f₂PolynomialSignClass[complete] -
FABL.ProbabilityDensity.IsBiased.violaTheorem[complete]
Viola's Theorem. Let
\varphi:\mathbb F_2^n\to\mathbb R_{\ge0} be an
\epsilon-biased probability density, where 0\le\epsilon\le1, and let
d\in\mathbb N_{>0}. Define
\epsilon_d=9\epsilon^{\,1/2^{d-1}}.
Then the d-fold convolution \varphi^{*d}
\epsilon_d-fools all
f:\mathbb F_2^n\to\{-1,1\} with
\deg_{\mathbb F_2}(f)\le d; explicitly,
\left|
\mathbb E_{\boldsymbol y^{(1)},\ldots,\boldsymbol y^{(d)}
\mathrel{\sim}\varphi}
\!\left[
f\!\left(\boldsymbol y^{(1)}+\cdots+\boldsymbol y^{(d)}\right)
\right]
-\mathbb E_{\boldsymbol x\sim\mathbb F_2^n}[f(\boldsymbol x)]
\right|
\le 9\epsilon^{\,1/2^{d-1}}.
Lean code for Theorem6.5.6●3 declarations
Associated Lean declarations
-
FABL.f₂PolynomialSignClass[complete]
-
FABL.isTranslationClosed_f₂PolynomialSignClass[complete]
-
FABL.ProbabilityDensity.IsBiased.violaTheorem[complete]
-
FABL.f₂PolynomialSignClass[complete] -
FABL.isTranslationClosed_f₂PolynomialSignClass[complete] -
FABL.ProbabilityDensity.IsBiased.violaTheorem[complete]
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/Viola.leancomplete
def FABL.f₂PolynomialSignClass (n d : ℕ) : Set (FABL.F₂Cube n → ℝ)
def FABL.f₂PolynomialSignClass (n d : ℕ) : Set (FABL.F₂Cube n → ℝ)
The real sign encodings of binary Boolean functions of algebraic degree at most `d`.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/Viola.leancomplete
theorem FABL.isTranslationClosed_f₂PolynomialSignClass (n d : ℕ) : FABL.IsTranslationClosed (FABL.f₂PolynomialSignClass n d)
theorem FABL.isTranslationClosed_f₂PolynomialSignClass (n d : ℕ) : FABL.IsTranslationClosed (FABL.f₂PolynomialSignClass n d)
The class of degree-at-most-`d` binary polynomial sign encodings is translation-closed.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/Viola.leancomplete
theorem FABL.ProbabilityDensity.IsBiased.violaTheorem {n : ℕ} {φ : FABL.ProbabilityDensity n} {ε : ℝ} (hφ : φ.IsBiased ε) (hε : 0 ≤ ε) (hε_one : ε ≤ 1) (d : ℕ) (hd : 1 ≤ d) : (φ.convolutionPower d).Fools (FABL.f₂PolynomialSignClass n d) (FABL.violaError ε d)
theorem FABL.ProbabilityDensity.IsBiased.violaTheorem {n : ℕ} {φ : FABL.ProbabilityDensity n} {ε : ℝ} (hφ : φ.IsBiased ε) (hε : 0 ≤ ε) (hε_one : ε ≤ 1) (d : ℕ) (hd : 1 ≤ d) : (φ.convolutionPower d).Fools (FABL.f₂PolynomialSignClass n d) (FABL.violaError ε d)
Viola's Theorem: the `d`-fold convolution of an `ε`-biased density fools every degree-at-most-`d` binary polynomial sign encoding with error `9 ε^(1 / 2^(d-1))`. The positive-degree hypothesis makes the book's exponent convention explicit; the induction base is `d = 1`.
-
FABL.violaBaseBias[complete] -
FABL.violaBaseBias_pos[complete] -
FABL.violaBaseBias_le_half[complete] -
FABL.violaError_baseBias[complete] -
FABL.violaSmallBiasSeedBits[complete] -
FABL.violaSmallBiasSampler[complete] -
FABL.card_violaSmallBiasSamplerSeedSpace[complete] -
FABL.violaSeedLogBound[complete] -
FABL.logb_smallBiasSupportEnvelope_eq[complete] -
FABL.violaSmallBiasSeedBits_le_of_card[complete] -
FABL.exists_violaSmallBiasDistribution[complete]
Random-bit consequence of Viola's Theorem. For
d\in\mathbb N_{>0} and 0<\epsilon\le1, there is an explicit
distribution that \epsilon-fools every
f:\mathbb F_2^n\to\{-1,1\} of
\mathbb F_2-degree at most d and can be sampled using
O(d\log n)+O\!\left(d\,2^d\log(1/\epsilon)\right)
independent random bits. This follows by applying Viola's Theorem to the
small-biased construction of Theorem 6.30 with its bias parameter chosen to
make 9\epsilon_0^{\,1/2^{d-1}}\le\epsilon.
Lean code for Corollary6.5.7●11 declarations
Associated Lean declarations
-
FABL.violaBaseBias[complete]
-
FABL.violaBaseBias_pos[complete]
-
FABL.violaBaseBias_le_half[complete]
-
FABL.violaError_baseBias[complete]
-
FABL.violaSmallBiasSeedBits[complete]
-
FABL.violaSmallBiasSampler[complete]
-
FABL.card_violaSmallBiasSamplerSeedSpace[complete]
-
FABL.violaSeedLogBound[complete]
-
FABL.logb_smallBiasSupportEnvelope_eq[complete]
-
FABL.violaSmallBiasSeedBits_le_of_card[complete]
-
FABL.exists_violaSmallBiasDistribution[complete]
-
FABL.violaBaseBias[complete] -
FABL.violaBaseBias_pos[complete] -
FABL.violaBaseBias_le_half[complete] -
FABL.violaError_baseBias[complete] -
FABL.violaSmallBiasSeedBits[complete] -
FABL.violaSmallBiasSampler[complete] -
FABL.card_violaSmallBiasSamplerSeedSpace[complete] -
FABL.violaSeedLogBound[complete] -
FABL.logb_smallBiasSupportEnvelope_eq[complete] -
FABL.violaSmallBiasSeedBits_le_of_card[complete] -
FABL.exists_violaSmallBiasDistribution[complete]
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
def FABL.violaBaseBias (ε : ℝ) (d : ℕ) : ℝ
def FABL.violaBaseBias (ε : ℝ) (d : ℕ) : ℝ
The bias supplied to Theorem 6.30 before applying Viola's theorem.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
theorem FABL.violaBaseBias_pos {ε : ℝ} (hε : 0 < ε) (d : ℕ) : 0 < FABL.violaBaseBias ε d
theorem FABL.violaBaseBias_pos {ε : ℝ} (hε : 0 < ε) (d : ℕ) : 0 < FABL.violaBaseBias ε d
A positive target error gives a positive base bias.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
theorem FABL.violaBaseBias_le_half {ε : ℝ} (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (d : ℕ) : FABL.violaBaseBias ε d ≤ 2⁻¹
theorem FABL.violaBaseBias_le_half {ε : ℝ} (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (d : ℕ) : FABL.violaBaseBias ε d ≤ 2⁻¹
In the book's error range, the selected base bias is at most one half.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
theorem FABL.violaError_baseBias {ε : ℝ} (hε : 0 < ε) (d : ℕ) (_hd : 1 ≤ d) : FABL.violaError (FABL.violaBaseBias ε d) d = ε
theorem FABL.violaError_baseBias {ε : ℝ} (hε : 0 < ε) (d : ℕ) (_hd : 1 ≤ d) : FABL.violaError (FABL.violaBaseBias ε d) d = ε
The choice of base bias makes Viola's error exactly the requested error.
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
def FABL.violaSmallBiasSeedBits (d ℓ : ℕ) : ℕ
def FABL.violaSmallBiasSeedBits (d ℓ : ℕ) : ℕ
Exact independent seed-bit count: two `ℓ`-bit field elements for each of the `d` convolution summands.
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
def FABL.violaSmallBiasSampler (n d : ℕ) {ℓ : ℕ} (hℓ : ℓ ≠ 0) (seeds : Fin d → FABL.BinaryExtensionField ℓ × FABL.BinaryExtensionField ℓ) : FABL.F₂Cube n
def FABL.violaSmallBiasSampler (n d : ℕ) {ℓ : ℕ} (hℓ : ℓ ≠ 0) (seeds : Fin d → FABL.BinaryExtensionField ℓ × FABL.BinaryExtensionField ℓ) : FABL.F₂Cube n
The explicit sampler adds `d` independently seeded outputs of the Theorem 6.30 generator.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
theorem FABL.card_violaSmallBiasSamplerSeedSpace (d : ℕ) {ℓ : ℕ} (hℓ : ℓ ≠ 0) : Fintype.card (Fin d → FABL.BinaryExtensionField ℓ × FABL.BinaryExtensionField ℓ) = 2 ^ FABL.violaSmallBiasSeedBits d ℓ
theorem FABL.card_violaSmallBiasSamplerSeedSpace (d : ℕ) {ℓ : ℕ} (hℓ : ℓ ≠ 0) : Fintype.card (Fin d → FABL.BinaryExtensionField ℓ × FABL.BinaryExtensionField ℓ) = 2 ^ FABL.violaSmallBiasSeedBits d ℓ
The sampler's finite seed space has exactly `2^(2dℓ)` elements.
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
def FABL.violaSeedLogBound (n d : ℕ) (ε : ℝ) : ℝ
def FABL.violaSeedLogBound (n d : ℕ) (ε : ℝ) : ℝ
The real logarithmic expression underlying the book's two random-bit terms.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
theorem FABL.logb_smallBiasSupportEnvelope_eq {n d : ℕ} {ε : ℝ} (hn : 0 < n) (hε : 0 < ε) : Real.logb 2 (16 * (↑n / FABL.violaBaseBias ε d) ^ 2) = 4 + 2 * (Real.logb 2 ↑n + 2 ^ (d - 1) * Real.logb 2 (9 / ε))
theorem FABL.logb_smallBiasSupportEnvelope_eq {n d : ℕ} {ε : ℝ} (hn : 0 < n) (hε : 0 < ε) : Real.logb 2 (16 * (↑n / FABL.violaBaseBias ε d) ^ 2) = 4 + 2 * (Real.logb 2 ↑n + 2 ^ (d - 1) * Real.logb 2 (9 / ε))
The support-size logarithm of the selected base construction has the advertised `log n + 2^(d-1) log(1/ε)` form.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
theorem FABL.violaSmallBiasSeedBits_le_of_card {n d ℓ : ℕ} {ε : ℝ} (hn : 0 < n) (hε : 0 < ε) (hℓ : ℓ ≠ 0) (hcard : ↑(FABL.smallBiasGeneratorMultiset n hℓ).card ≤ 16 * (↑n / FABL.violaBaseBias ε d) ^ 2) : ↑(FABL.violaSmallBiasSeedBits d ℓ) ≤ FABL.violaSeedLogBound n d ε
theorem FABL.violaSmallBiasSeedBits_le_of_card {n d ℓ : ℕ} {ε : ℝ} (hn : 0 < n) (hε : 0 < ε) (hℓ : ℓ ≠ 0) (hcard : ↑(FABL.smallBiasGeneratorMultiset n hℓ).card ≤ 16 * (↑n / FABL.violaBaseBias ε d) ^ 2) : ↑(FABL.violaSmallBiasSeedBits d ℓ) ≤ FABL.violaSeedLogBound n d ε
A support bound for the Theorem 6.30 construction yields the corresponding exact random-bit bound for `d` independent seed pairs.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaSeedLength.leancomplete
theorem FABL.exists_violaSmallBiasDistribution (n d : ℕ) (hn : 0 < n) (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hε_one : ε ≤ 1) : ∃ ℓ, ∃ (hℓ : ℓ ≠ 0), ((FABL.smallBiasGeneratorDensity n hℓ).convolutionPower d).Fools (FABL.f₂PolynomialSignClass n d) ε ∧ ↑(FABL.violaSmallBiasSeedBits d ℓ) ≤ FABL.violaSeedLogBound n d ε
theorem FABL.exists_violaSmallBiasDistribution (n d : ℕ) (hn : 0 < n) (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hε_one : ε ≤ 1) : ∃ ℓ, ∃ (hℓ : ℓ ≠ 0), ((FABL.smallBiasGeneratorDensity n hℓ).convolutionPower d).Fools (FABL.f₂PolynomialSignClass n d) ε ∧ ↑(FABL.violaSmallBiasSeedBits d ℓ) ≤ FABL.violaSeedLogBound n d ε
Random-bit consequence of Viola's theorem. The witness is the explicit finite-field density from Theorem 6.30, convolved `d` times.
Definition 6.48. For
f:\mathbb F_2^n\to\mathbb F_2 and
y\in\mathbb F_2^n, the directional derivative of f in direction
y is the function
\Delta_yf:\mathbb F_2^n\to\mathbb F_2 defined by
\Delta_yf(x)=f(x+y)-f(x)=f(x+y)+f(x).
The two displayed expressions agree because the codomain is
\mathbb F_2.
Lean code for Definition6.5.8●1 definition
Associated Lean declarations
-
FABL.booleanDerivative[complete]
-
FABL.booleanDerivative[complete]
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/DirectionalDerivatives.leancomplete
def FABL.booleanDerivative {n : ℕ} (f : FABL.F₂BooleanFunction n) (y : FABL.F₂Cube n) : FABL.F₂BooleanFunction n
def FABL.booleanDerivative {n : ℕ} (f : FABL.F₂BooleanFunction n) (y : FABL.F₂Cube n) : FABL.F₂BooleanFunction n
The binary directional derivative in direction `y`.
Fact 6.49. For every
f:\mathbb F_2^n\to\mathbb F_2 and
y\in\mathbb F_2^n,
\deg_{\mathbb F_2}(\Delta_yf)
\le \deg_{\mathbb F_2}(f)-1.
For a constant function the right side is interpreted in the natural
truncated-degree convention.
Lean code for Lemma6.5.9●1 theorem
Associated Lean declarations
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/DirectionalDerivatives.leancomplete
theorem FABL.functionAlgebraicDegree_booleanDerivative_le {n : ℕ} (f : FABL.F₂BooleanFunction n) (y : FABL.F₂Cube n) : FABL.functionAlgebraicDegree (FABL.booleanDerivative f y) ≤ FABL.functionAlgebraicDegree f - 1
theorem FABL.functionAlgebraicDegree_booleanDerivative_le {n : ℕ} (f : FABL.F₂BooleanFunction n) (y : FABL.F₂Cube n) : FABL.functionAlgebraicDegree (FABL.booleanDerivative f y) ≤ FABL.functionAlgebraicDegree f - 1
Fact 6.49: every binary directional derivative lowers algebraic degree by one.
Proposition 6.50. Let
f:\mathbb F_2^n\to\mathbb F_2 satisfy
\deg_{\mathbb F_2}(f)=d, fix y,y'\in\mathbb F_2^n, and define
g(x)=f(x+y)-f(x+y').
Then
\deg_{\mathbb F_2}(g)\le d-1.
Lean code for Proposition6.5.10●1 theorem
Associated Lean declarations
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/DirectionalDerivatives.leancomplete
theorem FABL.functionAlgebraicDegree_add_translates_le {n : ℕ} (f : FABL.F₂BooleanFunction n) (d : ℕ) (hdegree : FABL.functionAlgebraicDegree f = d) (y y' : FABL.F₂Cube n) : (FABL.functionAlgebraicDegree fun x => f (x + y) + f (x + y')) ≤ d - 1
theorem FABL.functionAlgebraicDegree_add_translates_le {n : ℕ} (f : FABL.F₂BooleanFunction n) (d : ℕ) (hdegree : FABL.functionAlgebraicDegree f = d) (y y' : FABL.F₂Cube n) : (FABL.functionAlgebraicDegree fun x => f (x + y) + f (x + y')) ≤ d - 1
Proposition 6.50: the difference of two translates of a degree-`d` binary polynomial has degree at most `d - 1`.
-
FABL.IsTranslationClosed[complete] -
FABL.ProbabilityDensity.expectation_convolution[complete] -
FABL.ProbabilityDensity.Fools.convolution_right[complete]
Exercise 6.29. Let \mathcal C be a class of functions
\mathbb F_2^n\to\mathbb R closed under translation: if
f\in\mathcal C and z\in\mathbb F_2^n, then the function
f^{+z}(x)=f(x+z)
also belongs to \mathcal C. If a probability density \psi
\epsilon-fools \mathcal C, then for every probability density
\varphi, the convolution \psi*\varphi also
\epsilon-fools \mathcal C.
Lean code for Lemma6.5.11●3 declarations
Associated Lean declarations
-
FABL.IsTranslationClosed[complete]
-
FABL.ProbabilityDensity.expectation_convolution[complete]
-
FABL.ProbabilityDensity.Fools.convolution_right[complete]
-
FABL.IsTranslationClosed[complete] -
FABL.ProbabilityDensity.expectation_convolution[complete] -
FABL.ProbabilityDensity.Fools.convolution_right[complete]
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/Fooling.leancomplete
def FABL.IsTranslationClosed {n : ℕ} (C : Set (FABL.F₂Cube n → ℝ)) : Prop
def FABL.IsTranslationClosed {n : ℕ} (C : Set (FABL.F₂Cube n → ℝ)) : Prop
A class of real-valued binary-cube functions is closed under every additive translation.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/Fooling.leancomplete
theorem FABL.ProbabilityDensity.expectation_convolution {n : ℕ} (ψ φ : FABL.ProbabilityDensity n) (f : FABL.F₂Cube n → ℝ) : (ψ.convolution φ).expectation f = Finset.univ.expect fun z => φ.toFun z * ψ.expectation fun y => f (y + z)
theorem FABL.ProbabilityDensity.expectation_convolution {n : ℕ} (ψ φ : FABL.ProbabilityDensity n) (f : FABL.F₂Cube n → ℝ) : (ψ.convolution φ).expectation f = Finset.univ.expect fun z => φ.toFun z * ψ.expectation fun y => f (y + z)
Expectation against a convolution is the iterated expectation of the translated test function.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/Fooling.leancomplete
theorem FABL.ProbabilityDensity.Fools.convolution_right {n : ℕ} {C : Set (FABL.F₂Cube n → ℝ)} {ε : ℝ} {ψ : FABL.ProbabilityDensity n} (hψ : ψ.Fools C ε) (hC : FABL.IsTranslationClosed C) (φ : FABL.ProbabilityDensity n) : (ψ.convolution φ).Fools C ε
theorem FABL.ProbabilityDensity.Fools.convolution_right {n : ℕ} {C : Set (FABL.F₂Cube n → ℝ)} {ε : ℝ} {ψ : FABL.ProbabilityDensity n} (hψ : ψ.Fools C ε) (hC : FABL.IsTranslationClosed C) (φ : FABL.ProbabilityDensity n) : (ψ.convolution φ).Fools C ε
O'Donnell, Exercise 6.29: right convolution by an arbitrary density preserves fooling of a translation-closed class.
Directional-gap inequality used in Viola's proof. Let
\psi:\mathbb F_2^n\to\mathbb R_{\ge0} be a probability density and let
F:\mathbb F_2^n\to\{-1,1\}. Define the multiplicative directional
derivative
D_yF(x)=F(x+y)F(x).
Then
\begin{aligned}
|\mathbb E[F]|\,
\left|
\mathbb E_{z\sim\psi}[F(z)]-\mathbb E[F]
\right|
&\le
\mathbb E_{y\sim\mathbb F_2^n}
\left[
\left|
\mathbb E_{z\sim\psi}[D_yF(z)]
-\mathbb E_{x\sim\mathbb F_2^n}[D_yF(x)]
\right|
\right].
\end{aligned}
If F(x)=(-1)^{f(x)} for an
\mathbb F_2-polynomial f, then
D_yF(x)=(-1)^{\Delta_yf(x)}.
Lean code for Lemma6.5.12●2 declarations
Associated Lean declarations
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaAuxiliary.leancomplete
def FABL.multiplicativeDerivative {n : ℕ} (F : FABL.F₂Cube n → ℝ) (y : FABL.F₂Cube n) : FABL.F₂Cube n → ℝ
def FABL.multiplicativeDerivative {n : ℕ} (F : FABL.F₂Cube n → ℝ) (y : FABL.F₂Cube n) : FABL.F₂Cube n → ℝ
The multiplicative directional derivative of a real-valued function on the binary cube.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaAuxiliary.leancomplete
theorem FABL.abs_mean_mul_density_gap_le_expect_abs_multiplicativeDerivative_gap {n : ℕ} (ψ : FABL.ProbabilityDensity n) (F : FABL.F₂Cube n → ℝ) (_hF : FABL.IsSignValued F) : |Finset.univ.expect fun x => F x| * |ψ.expectation F - Finset.univ.expect fun x => F x| ≤ Finset.univ.expect fun y => |ψ.expectation (FABL.multiplicativeDerivative F y) - Finset.univ.expect fun x => FABL.multiplicativeDerivative F y x|
theorem FABL.abs_mean_mul_density_gap_le_expect_abs_multiplicativeDerivative_gap {n : ℕ} (ψ : FABL.ProbabilityDensity n) (F : FABL.F₂Cube n → ℝ) (_hF : FABL.IsSignValued F) : |Finset.univ.expect fun x => F x| * |ψ.expectation F - Finset.univ.expect fun x => F x| ≤ Finset.univ.expect fun y => |ψ.expectation (FABL.multiplicativeDerivative F y) - Finset.univ.expect fun x => FABL.multiplicativeDerivative F y x|
The directional-gap inequality used in Case 1 of Viola's proof.
Convolution second moment used in Viola's proof. For every probability
density \varphi:\mathbb F_2^n\to\mathbb R_{\ge0} and every
F:\mathbb F_2^n\to\mathbb R,
\begin{aligned}
&\mathbb E_{y,y'\mathrel{\sim}\varphi}
\mathbb E_{x\sim\mathbb F_2^n}
[F(x+y)F(x+y')]\\
&\qquad =
\mathbb E_{x\sim\mathbb F_2^n}[(\varphi*F)(x)^2]
=\sum_{\gamma\in\widehat{\mathbb F_2^n}}
\widehat\varphi(\gamma)^2\widehat F(\gamma)^2.
\end{aligned}
Consequently, if \varphi is \epsilon-biased and
F:\mathbb F_2^n\to\{-1,1\}, then
\mathbb E[(\varphi*F)^2]
\le \mathbb E[F]^2+\epsilon^2.
Lean code for Lemma6.5.13●3 theorems
Associated Lean declarations
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaAuxiliary.leancomplete
theorem FABL.expectation_pair_correlation_eq_expect_convolution_sq {n : ℕ} (φ : FABL.ProbabilityDensity n) (F : FABL.F₂Cube n → ℝ) : (φ.expectation fun y => φ.expectation fun y' => Finset.univ.expect fun x => F (x + y) * F (x + y')) = Finset.univ.expect fun x => FABL.convolution φ.toFun F x ^ 2
theorem FABL.expectation_pair_correlation_eq_expect_convolution_sq {n : ℕ} (φ : FABL.ProbabilityDensity n) (F : FABL.F₂Cube n → ℝ) : (φ.expectation fun y => φ.expectation fun y' => Finset.univ.expect fun x => F (x + y) * F (x + y')) = Finset.univ.expect fun x => FABL.convolution φ.toFun F x ^ 2
The pair-correlation average under two independent density samples is the second moment of the density/function convolution.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaAuxiliary.leancomplete
theorem FABL.expect_convolution_sq_eq_sum_sq_vectorFourierCoeff {n : ℕ} (φ : FABL.ProbabilityDensity n) (F : FABL.F₂Cube n → ℝ) : (Finset.univ.expect fun x => FABL.convolution φ.toFun F x ^ 2) = ∑ γ, FABL.vectorFourierCoeff φ.toFun γ ^ 2 * FABL.vectorFourierCoeff F γ ^ 2
theorem FABL.expect_convolution_sq_eq_sum_sq_vectorFourierCoeff {n : ℕ} (φ : FABL.ProbabilityDensity n) (F : FABL.F₂Cube n → ℝ) : (Finset.univ.expect fun x => FABL.convolution φ.toFun F x ^ 2) = ∑ γ, FABL.vectorFourierCoeff φ.toFun γ ^ 2 * FABL.vectorFourierCoeff F γ ^ 2
Parseval and the convolution theorem identify the convolution second moment with the pointwise product of the two Fourier square spectra.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaAuxiliary.leancomplete
theorem FABL.expect_convolution_sq_le_sq_mean_add_sq {n : ℕ} {φ : FABL.ProbabilityDensity n} {F : FABL.F₂Cube n → ℝ} {ε : ℝ} (hφ : φ.IsBiased ε) (hF : FABL.IsSignValued F) : (Finset.univ.expect fun x => FABL.convolution φ.toFun F x ^ 2) ≤ (Finset.univ.expect fun x => F x) ^ 2 + ε ^ 2
theorem FABL.expect_convolution_sq_le_sq_mean_add_sq {n : ℕ} {φ : FABL.ProbabilityDensity n} {F : FABL.F₂Cube n → ℝ} {ε : ℝ} (hφ : φ.IsBiased ε) (hF : FABL.IsSignValued F) : (Finset.univ.expect fun x => FABL.convolution φ.toFun F x ^ 2) ≤ (Finset.univ.expect fun x => F x) ^ 2 + ε ^ 2
The small-bias and sign-valued consequence of the convolution second-moment identity.
-
FABL.violaError[complete] -
FABL.violaError_succ[complete] -
FABL.sqrt_violaError[complete] -
FABL.sq_le_violaError[complete]
Error recurrence used in Viola's proof. Let 0\le\epsilon\le1 and, for
d\ge1, set
\epsilon_d=9\epsilon^{\,1/2^{d-1}}.
Then
\epsilon_{d+1}=3\sqrt{\epsilon_d},
\qquad
\sqrt{\epsilon_d}=\frac13\epsilon_{d+1},
\qquad
\epsilon^2\le\epsilon_d.
Lean code for Lemma6.5.14●4 declarations
Associated Lean declarations
-
FABL.violaError[complete]
-
FABL.violaError_succ[complete]
-
FABL.sqrt_violaError[complete]
-
FABL.sq_le_violaError[complete]
-
FABL.violaError[complete] -
FABL.violaError_succ[complete] -
FABL.sqrt_violaError[complete] -
FABL.sq_le_violaError[complete]
-
defdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaAuxiliary.leancomplete
def FABL.violaError (ε : ℝ) (d : ℕ) : ℝ
def FABL.violaError (ε : ℝ) (d : ℕ) : ℝ
The error parameter in Viola's theorem: `ε_d = 9 ε^(1 / 2^(d-1))`, intended for `d ≥ 1`.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaAuxiliary.leancomplete
theorem FABL.violaError_succ {ε : ℝ} (hε : 0 ≤ ε) (_hε_one : ε ≤ 1) {d : ℕ} (hd : 1 ≤ d) : FABL.violaError ε (d + 1) = 3 * √(FABL.violaError ε d)
theorem FABL.violaError_succ {ε : ℝ} (hε : 0 ≤ ε) (_hε_one : ε ≤ 1) {d : ℕ} (hd : 1 ≤ d) : FABL.violaError ε (d + 1) = 3 * √(FABL.violaError ε d)
The successive Viola error parameters satisfy `ε_(d+1) = 3 √ε_d`.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaAuxiliary.leancomplete
theorem FABL.sqrt_violaError {ε : ℝ} (hε : 0 ≤ ε) (hε_one : ε ≤ 1) {d : ℕ} (hd : 1 ≤ d) : √(FABL.violaError ε d) = 1 / 3 * FABL.violaError ε (d + 1)
theorem FABL.sqrt_violaError {ε : ℝ} (hε : 0 ≤ ε) (hε_one : ε ≤ 1) {d : ℕ} (hd : 1 ≤ d) : √(FABL.violaError ε d) = 1 / 3 * FABL.violaError ε (d + 1)
Equivalently, `√ε_d = ε_(d+1) / 3`.
-
theoremdefined in FABL/Chapter06/FoolingF₂Polynomials/ViolaAuxiliary.leancomplete
theorem FABL.sq_le_violaError {ε : ℝ} (hε : 0 ≤ ε) (hε_one : ε ≤ 1) {d : ℕ} (_hd : 1 ≤ d) : ε ^ 2 ≤ FABL.violaError ε d
theorem FABL.sq_le_violaError {ε : ℝ} (hε : 0 ≤ ε) (hε_one : ε ≤ 1) {d : ℕ} (_hd : 1 ≤ d) : ε ^ 2 ≤ FABL.violaError ε d
For `0 ≤ ε ≤ 1`, the original squared bias is at most every Viola error parameter.
Counting lower bound for convolution generators. The book records the
external historical result that, for each d\in\mathbb N_{>0}, there are
small-bias parameters and dimensions for which a d-fold convolution of
small-biased densities fails to fool some Boolean function of
\mathbb F_2-degree d+1.
The book cites the counting argument establishing this sharp degree boundary without stating its full quantified parameter theorem, and does not prove it. This node records the historical claim only and supplies no assumption to the production library.
Lovett--Tzur explicit counterexample. For every
d\in\mathbb N_{>0} and \ell\ge2d+1, there are an explicit
(\ell/2^n)-biased density \varphi on
\mathbb F_2^{(\ell+1)n} and an explicit Boolean function
f:\mathbb F_2^{(\ell+1)n}\to\{-1,1\},
\qquad
\deg_{\mathbb F_2}(f)=d+1,
such that
\left|
\mathbb E_{w\sim\varphi^{*d}}[f(w)]-\mathbb E[f]
\right|
\ge1-\frac{2d}{2^n}.
The book quotes this external construction without proof.
Open problem (the error exponent in Viola's Theorem). It is unknown whether
the error dependence
\epsilon^{\,1/2^{d-1}} in Viola's Theorem can be improved, even for
d=2. An improvement as modest as replacing it by
\epsilon^{\,1/1.99^d} for degrees as large as \log n would imply
progress on the correlation-bounds-for-polynomials problem.