Documentation

Complexity.Foundations.BooleanAnalysis.BucketWeight

Fourier weight on the sets with a given part in a set of coordinates #

For a set J of coordinates and a set S, the bucket weight of S in J is the Fourier weight of F on the sets U with U ∩ J = S (BitString.bucketWeight). O'Donnell writes it W^{S | J̄} [F] = ∑_{T ⊆ J̄} F̂(S ∪ T)² for S ⊆ J, where J̄ is the complement of J O'Donnell, Definition 3.39. The buckets of a fixed J partition the sets of coordinates, so the bucket weights of distinct sets S add up to at most the total weight (BitString.sum_bucketWeight_le), and the bucket of U ∩ J holds at least the weight of U (BitString.sq_fourierCoeff_le_bucketWeight). For J the set of all coordinates the buckets are single sets (BitString.bucketWeight_univ).

The bucket weight is the expected squared coefficient of the restriction of F fixing the coordinates outside J at random (BitString.expect_fourierCoeff_piecewise_sq), hence the expectation of F (x, z) χ_S(x) F (y, z) χ_S(y) for independent uniform x, y, z, where (x, z) takes the coordinates in J from x and the others from z (BitString.bucketWeight_eq_expect_sample) O'Donnell, Proposition 3.40. With query access to a Boolean function this lets one estimate any bucket weight by sampling: the basis of the Goldreich–Levin and Kushilevitz–Mansour algorithms [GL89] [KM93].

Main definitions #

Main results #

References #

source
noncomputable def Cslib.BitString.bucketWeight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → ℝ) (J S : Finset ι) :
ℝ

The bucket weight of S in J: the Fourier weight of F on the sets U of coordinates with U ∩ J = S, written W^{S | J̄} [F] by O'Donnell, where J̄ is the complement of J.

Instances For
    source
    theorem Cslib.BitString.bucketWeight_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → ℝ) (J S : Finset ι) :
    0 ≤ bucketWeight F J S

    Every bucket weight is nonnegative.

    source
    @[simp]
    theorem Cslib.BitString.bucketWeight_univ {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → ℝ) (S : Finset ι) :
    bucketWeight F Finset.univ S = fourierCoeff F S ^ 2

    For J the set of all coordinates, the bucket of S is S alone.

    source
    theorem Cslib.BitString.sq_fourierCoeff_le_bucketWeight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → ℝ) (J U : Finset ι) :
    fourierCoeff F U ^ 2 ≤ bucketWeight F J (U ∩ J)

    The bucket of U ∩ J holds at least the weight of U.

    source
    theorem Cslib.BitString.sum_bucketWeight_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → ℝ) (J : Finset ι) (𝒮 : Finset (Finset ι)) :
    ∑ S ∈ 𝒮, bucketWeight F J S ≤ ∑ U : Finset ι, fourierCoeff F U ^ 2

    The buckets of J partition the sets of coordinates: the bucket weights of distinct sets add up to at most the total Fourier weight.

    source
    theorem Cslib.BitString.bucketWeight_eq_expect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → ℝ) (J S : Finset ι) :
    bucketWeight F J S = Finset.univ.expect fun (z : ι → Bool) => fourierCoeff (fun (x : ι → Bool) => F (J.piecewise x z)) S ^ 2

    The bucket weight is the expected squared coefficient of a random restriction.

    source
    theorem Cslib.BitString.bucketWeight_eq_expect_sample {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → ℝ) (J S : Finset ι) :
    bucketWeight F J S = Finset.univ.expect fun (p : (ι → Bool) × (ι → Bool) × (ι → Bool)) => F (J.piecewise p.1 p.2.2) * chi ℝ S p.1 * (F (J.piecewise p.2.1 p.2.2) * chi ℝ S p.2.1)

    Estimating a bucket weight by sampling O'Donnell, Proposition 3.40: the bucket weight of S in J is the expectation of F (x, z) χ_S(x) F (y, z) χ_S(y) for independent uniform x, y, z, where (x, z) takes the coordinates in J from x and the others from z.