Rounding a real approximation to its sign

A real function g on the cube rounds to the Boolean function that is true, the sign -1, exactly where g is negative (BitString.signRound). If g approximates a Boolean function f, read as signs, in mean square, then the rounding is close to f: the fraction of the points where they differ is at most 𝔼_x (f x - g x)² (BitString.hammingDist_signRound_div_le_expect_sq_sub), since a point where the signs differ contributes at least one to the mean square O'Donnell, Section 3.4.

By Parseval's identity, the mean-square distance from a function F to a combination ∑_{S ∈ T} c_S χ_S of the characters of a family T of sets is the squared error of the weights on T plus the Fourier weight of F off T (BitString.expect_sq_sub_sum_mul_chi). So estimating the Fourier coefficients of f on a family carrying almost all of its weight, and rounding, approximates f (BitString.hammingDist_signRound_sum_mul_chi_div_le): the principle of the low-degree algorithm of Linial, Mansour and Nisan [LMN93].

Main definitions

• Cslib.BitString.signRound: a real function on the cube rounded to its sign.

Main results

• Cslib.BitString.hammingDist_signRound_le_sum_sq_sub, Cslib.BitString.hammingDist_signRound_div_le_expect_sq_sub: rounding a mean-square approximation of a Boolean function to its sign approximates the function.
• Cslib.BitString.expect_sq_sub_sum_mul_chi: the mean-square distance to a combination of characters, by Parseval's identity.
• Cslib.BitString.hammingDist_signRound_sum_mul_chi_div_le: rounding approximate Fourier coefficients on a family of sets.

References

• R. O'Donnell, Analysis of Boolean Functions
• N. Linial, Y. Mansour, N. Nisan, Constant depth circuits, Fourier transform, and learnability

noncomputable def Cslib.BitString.signRound {ι : Type u_1} (g : (ι → Bool) → ℝ) (x : ι → Bool) : Bool

A real function on the cube rounded to its sign: true, the sign -1, where it is negative, and false, the sign 1, elsewhere.

@[simp]

theorem Cslib.BitString.signRound_apply {ι : Type u_1} (g : (ι → Bool) → ℝ) (x : ι → Bool) : signRound g x = decide (g x < 0)

The sign rounding of g at x is true exactly when g x < 0.

theorem Cslib.BitString.hammingDist_signRound_le_sum_sq_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (g : (ι → Bool) → ℝ) : ↑(hammingDist (signRound g) f) ≤ ∑ x : ι → Bool, (signVal (f x) - g x) ^ 2

Rounding to the sign: the rounding of g differs from f on at most ∑_x (f x - g x)² points, reading f as signs.

theorem Cslib.BitString.hammingDist_signRound_div_le_expect_sq_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (g : (ι → Bool) → ℝ) : ↑(hammingDist (signRound g) f) / 2 ^ Fintype.card ι ≤ Finset.univ.expect fun (x : ι → Bool) => (signVal (f x) - g x) ^ 2

Rounding to the sign O'Donnell, Section 3.4: the rounding of g differs from f on at most a fraction 𝔼_x (f x - g x)² of the points, reading f as signs.

theorem Cslib.BitString.expect_sq_sub_sum_mul_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → ℝ) (T : Finset (Finset ι)) (c : Finset ι → ℝ) : (Finset.univ.expect fun (x : ι → Bool) => (F x - ∑ S ∈ T, c S * chi ℝ S x) ^ 2) = ∑ S ∈ T, (fourierCoeff F S - c S) ^ 2 + ∑ S ∈ Tᶜ, fourierCoeff F S ^ 2

The mean-square distance from F to the combination ∑_{S ∈ T} c_S χ_S of characters is the squared error of the weights on T plus the Fourier weight of F off T.

theorem Cslib.BitString.hammingDist_signRound_sum_mul_chi_div_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (T : Finset (Finset ι)) (c : Finset ι → ℝ) : ↑(hammingDist (signRound fun (x : ι → Bool) => ∑ S ∈ T, c S * chi ℝ S x) f) / 2 ^ Fintype.card ι ≤ ∑ S ∈ T, (fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S - c S) ^ 2 + ∑ S ∈ Tᶜ, fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S ^ 2

Learning from approximate Fourier coefficients O'Donnell, Section 3.4: rounding the combination ∑_{S ∈ T} c_S χ_S of characters to its sign misclassifies at most a fraction ∑_{S ∈ T} (f̂(S) - c_S)² + ∑_{S ∉ T} f̂(S)² of the points, where f̂ are the Fourier coefficients of f read as signs.