Noise stability and noise sensitivity

Flipping each bit of a string x independently with probability (1 - ρ) / 2 gives a random string y that is ρ-correlated with x. The noise operator T_ρ (BitString.noiseOp) averages a real function over this noise, T_ρ f x = 𝔼_y f y. It damps the Fourier coefficient of S by ρ ^ |S| (BitString.fourierCoeff_noiseOp), so it has Fourier expansion ∑_S ρ ^ |S| f̂(S) χ_S (BitString.noiseOp_eq_sum), the noise operators form a semigroup, T_ρ T_σ = T_{ρ σ} (BitString.noiseOp_noiseOp), and each is self-adjoint (BitString.expect_mul_noiseOp_comm).

The noise stability Stab_ρ[f] = 𝔼_x f x T_ρ f x (BitString.noiseStability) is the correlation of f at two ρ-correlated strings. It is ∑_S ρ ^ |S| f̂(S) ^ 2 (BitString.noiseStability_eq_sum), so on 0 ≤ ρ ≤ 1 it increases with ρ from the squared mean (𝔼 f) ^ 2 to the second moment 𝔼 f ^ 2.

The noise sensitivity NS_δ[f] of a Boolean function (BitString.noiseSensitivity) is the probability that f x ≠ f y when y flips each bit of a uniform x independently with probability δ. Reading f as the function F = (-1) ^ f with values ±1, it is NS_δ[f] = 1 / 2 - 1 / 2 Stab_{1 - 2 δ}[F] (BitString.noiseSensitivity_eq_noiseStability), hence NS_δ[f] = ∑_S (1 - (1 - 2 δ) ^ |S|) / 2 F̂(S) ^ 2 (BitString.noiseSensitivity_eq_sum) and NS_δ[f] ≤ δ I[F], at most δ times the total influence (BitString.noiseSensitivity_le_mul_totalInfluence) O'Donnell, Section 2.4.

The noised string is x + P, the coordinatewise exclusive or of x with a random mask P of BitString.bernoulliAverage, bit strings adding in Mathlib's Boolean ring structure on Bool. The coordinates of the mask are independent: the average of a product of functions of the separate coordinates factorizes (BitString.bernoulliAverage_prod), so the character of S averages to (1 - 2 p) ^ |S| over a mask of rate p (BitString.bernoulliAverage_chi).

Main definitions

• Cslib.BitString.noiseOp, Cslib.BitString.noiseOpₗ: the noise operator T_ρ, and the same as a linear map.
• Cslib.BitString.noiseStability: the noise stability of a real function.
• Cslib.BitString.noiseSensitivity: the noise sensitivity of a Boolean function.

Main results

• Cslib.BitString.noiseOp_eq_sum, Cslib.BitString.fourierCoeff_noiseOp: the Fourier expansion of T_ρ f O'Donnell, Proposition 2.47.
• Cslib.BitString.noiseOp_noiseOp: the noise operators form a semigroup.
• Cslib.BitString.noiseOp_comp_arrowCongr, Cslib.BitString.noiseOp_of_isEmpty: the noise operator commutes with renaming the coordinates and is the identity on the cube over no coordinates.
• Cslib.BitString.expect_mul_noiseOp_comm: the noise operator is self-adjoint.
• Cslib.BitString.noiseStability_eq_sum: the Fourier formula for the noise stability O'Donnell, Theorem 2.49.
• Cslib.BitString.sq_expect_le_noiseStability, Cslib.BitString.noiseStability_le_expect_sq, Cslib.BitString.noiseStability_mono: the noise stability lies between the squared mean and the second moment, increasingly in ρ.
• Cslib.BitString.noiseSensitivity_eq_noiseStability, Cslib.BitString.noiseSensitivity_eq_sum: the noise sensitivity through the noise stability and its Fourier formula O'Donnell, Definition 2.43 and Theorem 2.49.
• Cslib.BitString.noiseSensitivity_le_mul_totalInfluence: the noise sensitivity at δ is at most δ times the total influence.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.BitString.bernoulliAverage_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (S : Finset ι) : bernoulliAverage p (chi ℝ S) = (1 - 2 * p) ^ S.card

The character of S averages to (1 - 2 p) ^ |S| over a random mask of rate p: each of its coordinates is selected, negating the sign, with probability p.

The noise operator

noncomputable def Cslib.BitString.noiseOp {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f : (ι → Bool) → ℝ) (x : ι → Bool) : ℝ

The noise operator T_ρ: the average of f at a string ρ-correlated with x, which flips each bit of x independently with probability (1 - ρ) / 2. It is an average over a probability distribution when -1 ≤ ρ ≤ 1.

theorem Cslib.BitString.noiseOp_eq_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f : (ι → Bool) → ℝ) (x : ι → Bool) : noiseOp ρ f x = ∑ S : Finset ι, ρ ^ S.card * fourierCoeff f S * chi ℝ S x

The Fourier expansion of T_ρ f: the noise operator damps the coefficient of S by ρ ^ |S| O'Donnell, Proposition 2.47.

theorem Cslib.BitString.fourierCoeff_noiseOp {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f : (ι → Bool) → ℝ) (S : Finset ι) : fourierCoeff (noiseOp ρ f) S = ρ ^ S.card * fourierCoeff f S

The noise operator damps the Fourier coefficient of S by ρ ^ |S| O'Donnell, Proposition 2.47.

theorem Cslib.BitString.noiseOp_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (S : Finset ι) (x : ι → Bool) : noiseOp ρ (chi ℝ S) x = ρ ^ S.card * chi ℝ S x

The characters are eigenfunctions of the noise operator.

@[simp]

theorem Cslib.BitString.noiseOp_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : noiseOp 1 f = f

At ρ = 1 no bit is flipped, so the noise operator is the identity.

theorem Cslib.BitString.noiseOp_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (x : ι → Bool) : noiseOp 0 f x = Finset.univ.expect fun (y : ι → Bool) => f y

At ρ = 0 the noised string is uniform, so the noise operator returns the mean.

@[simp]

theorem Cslib.BitString.noiseOp_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ c : ℝ) (x : ι → Bool) : noiseOp ρ (fun (x : ι → Bool) => c) x = c

The noise operator fixes the constants.

theorem Cslib.BitString.noiseOp_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f g : (ι → Bool) → ℝ) (x : ι → Bool) : noiseOp ρ (fun (y : ι → Bool) => f y + g y) x = noiseOp ρ f x + noiseOp ρ g x

The noise operator is additive.

theorem Cslib.BitString.noiseOp_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f g : (ι → Bool) → ℝ) (x : ι → Bool) : noiseOp ρ (fun (y : ι → Bool) => f y - g y) x = noiseOp ρ f x - noiseOp ρ g x

The noise operator commutes with subtraction.

theorem Cslib.BitString.noiseOp_const_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ c : ℝ) (f : (ι → Bool) → ℝ) (x : ι → Bool) : noiseOp ρ (fun (y : ι → Bool) => c * f y) x = c * noiseOp ρ f x

The noise operator commutes with scaling.

noncomputable def Cslib.BitString.noiseOpₗ {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) : ((ι → Bool) → ℝ) →ₗ[ℝ] (ι → Bool) → ℝ

The noise operator T_ρ, as a linear map.

@[simp]

theorem Cslib.BitString.noiseOpₗ_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f : (ι → Bool) → ℝ) : (noiseOpₗ ρ) f = noiseOp ρ f

The linear map noiseOpₗ ρ applies the noise operator T_ρ.

theorem Cslib.BitString.noiseOp_noiseOp {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ σ : ℝ) (f : (ι → Bool) → ℝ) : noiseOp ρ (noiseOp σ f) = noiseOp (ρ * σ) f

The noise operators form a semigroup: T_ρ T_σ = T_{ρ σ}.

theorem Cslib.BitString.noiseOp_comp_arrowCongr {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : Type u_2} [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (ρ : ℝ) (g : (κ → Bool) → ℝ) (x : ι → Bool) : noiseOp ρ (fun (y : ι → Bool) => g fun (j : κ) => y (e.symm j)) x = noiseOp ρ g fun (j : κ) => x (e.symm j)

The noise operator commutes with renaming the coordinates.

theorem Cslib.BitString.noiseOp_of_isEmpty {ι : Type u_1} [Fintype ι] [DecidableEq ι] [IsEmpty ι] (ρ : ℝ) (g : (ι → Bool) → ℝ) (x : ι → Bool) : noiseOp ρ g x = g x

On the cube over no coordinates, a single point, the noise operator is the identity.

theorem Cslib.BitString.expect_mul_noiseOp_eq_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f g : (ι → Bool) → ℝ) : (Finset.univ.expect fun (x : ι → Bool) => f x * noiseOp ρ g x) = ∑ S : Finset ι, ρ ^ S.card * (fourierCoeff f S * fourierCoeff g S)

The correlation of f with T_ρ g is the sum of the products of the Fourier coefficients damped by ρ ^ |S|.

theorem Cslib.BitString.expect_mul_noiseOp_comm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f g : (ι → Bool) → ℝ) : (Finset.univ.expect fun (x : ι → Bool) => f x * noiseOp ρ g x) = Finset.univ.expect fun (x : ι → Bool) => noiseOp ρ f x * g x

The noise operator is self-adjoint: 𝔼 f T_ρ g = 𝔼 (T_ρ f) g.

Noise stability

noncomputable def Cslib.BitString.noiseStability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f : (ι → Bool) → ℝ) : ℝ

The noise stability Stab_ρ[f] of f at ρ: the correlation 𝔼 f x f y of f at a uniform string x and a string y that is ρ-correlated with x.

theorem Cslib.BitString.noiseStability_eq_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f : (ι → Bool) → ℝ) : noiseStability ρ f = ∑ S : Finset ι, ρ ^ S.card * fourierCoeff f S ^ 2

The Fourier formula for the noise stability: Stab_ρ[f] = ∑_S ρ ^ |S| f̂(S) ^ 2 O'Donnell, Theorem 2.49.

theorem Cslib.BitString.mul_noiseStability_derivative {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (i : ι) (f : (ι → Bool) → ℝ) : ρ * noiseStability ρ (derivative i f) = ∑ S : Finset ι with i ∈ S, ρ ^ S.card * fourierCoeff f S ^ 2

The noise stability of a derivative: ρ Stab_ρ[Dᵢ f] weighs the squared coefficient of f on each set containing i by ρ to the size of the set.

theorem Cslib.BitString.noiseStability_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : noiseStability 1 f = Finset.univ.expect fun (x : ι → Bool) => f x ^ 2

At ρ = 1 the noise stability is the second moment.

theorem Cslib.BitString.noiseStability_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : noiseStability 0 f = (Finset.univ.expect fun (x : ι → Bool) => f x) ^ 2

At ρ = 0 the noise stability is the squared mean.

theorem Cslib.BitString.noiseStability_mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ σ : ℝ} (hρ : 0 ≤ ρ) (hρσ : ρ ≤ σ) (f : (ι → Bool) → ℝ) : noiseStability ρ f ≤ noiseStability σ f

On 0 ≤ ρ, the noise stability increases with ρ.

theorem Cslib.BitString.sq_expect_le_noiseStability {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ : ℝ} (hρ : 0 ≤ ρ) (f : (ι → Bool) → ℝ) : (Finset.univ.expect fun (x : ι → Bool) => f x) ^ 2 ≤ noiseStability ρ f

On 0 ≤ ρ, the noise stability is at least the squared mean.

theorem Cslib.BitString.noiseStability_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ : ℝ} (hρ : 0 ≤ ρ) (f : (ι → Bool) → ℝ) : 0 ≤ noiseStability ρ f

On 0 ≤ ρ, the noise stability is nonnegative.

theorem Cslib.BitString.noiseStability_le_expect_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ : ℝ} (hρ : |ρ| ≤ 1) (f : (ι → Bool) → ℝ) : noiseStability ρ f ≤ Finset.univ.expect fun (x : ι → Bool) => f x ^ 2

On |ρ| ≤ 1, the noise stability is at most the second moment.

Noise sensitivity

noncomputable def Cslib.BitString.noiseSensitivity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (δ : ℝ) (f : (ι → Bool) → Bool) : ℝ

The noise sensitivity NS_δ[f] of a Boolean function f at δ: the probability that f x ≠ f y for a uniform string x and the string y that flips each bit of x independently with probability δ.

theorem Cslib.BitString.noiseSensitivity_eq_noiseStability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (δ : ℝ) (f : (ι → Bool) → Bool) : noiseSensitivity δ f = 1 / 2 - 1 / 2 * noiseStability (1 - 2 * δ) fun (x : ι → Bool) => signVal (f x)

The noise sensitivity through the noise stability: NS_δ[f] = 1 / 2 - 1 / 2 Stab_{1 - 2 δ}[F], for F the function f with values ±1.

theorem Cslib.BitString.noiseSensitivity_eq_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (δ : ℝ) (f : (ι → Bool) → Bool) : noiseSensitivity δ f = ∑ S : Finset ι, (1 - (1 - 2 * δ) ^ S.card) / 2 * fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S ^ 2

The Fourier formula for the noise sensitivity: NS_δ[f] = ∑_S (1 - (1 - 2 δ) ^ |S|) / 2 F̂(S) ^ 2, for F the function f with values ±1 O'Donnell, Theorem 2.49.

@[simp]

theorem Cslib.BitString.noiseSensitivity_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) : noiseSensitivity 0 f = 0

With no noise, f never changes.

theorem Cslib.BitString.noiseSensitivity_mem_Icc {ι : Type u_1} [Fintype ι] [DecidableEq ι] {δ : ℝ} (hδ : 0 ≤ δ) (hδ' : δ ≤ 1) (f : (ι → Bool) → Bool) : noiseSensitivity δ f ∈ Set.Icc 0 1

On 0 ≤ δ ≤ 1, the noise sensitivity is a probability.

theorem Cslib.BitString.noiseSensitivity_mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] {δ δ' : ℝ} (hδδ' : δ ≤ δ') (hδ' : δ' ≤ 1 / 2) (f : (ι → Bool) → Bool) : noiseSensitivity δ f ≤ noiseSensitivity δ' f

On δ ≤ 1 / 2, the noise sensitivity increases with δ.

theorem Cslib.BitString.noiseSensitivity_le_mul_totalInfluence {ι : Type u_1} [Fintype ι] [DecidableEq ι] {δ : ℝ} (hδ : δ ≤ 1) (f : (ι → Bool) → Bool) : noiseSensitivity δ f ≤ δ * totalInfluence fun (x : ι → Bool) => signVal (f x)

The noise sensitivity is at most δ times the total influence: NS_δ[f] ≤ δ I[F] for δ ≤ 1, for F the function f with values ±1 O'Donnell, Exercise 2.42.