The Hamming distance in the Fourier basis

Read Boolean functions f g : (ι → Bool) → Bool as the functions F = (-1) ^ f and G = (-1) ^ g with values ±1. Where f and g agree, F - G vanishes, and where they differ (F - G) ^ 2 = 4, so the relative Hamming distance is a quarter of the mean of (F - G) ^ 2 (BitString.expect_sq_signVal_sub_signVal). By Parseval's identity it is a quarter of the squared Euclidean distance between the Fourier coefficients, d_H(f, g) / 2 ^ n = 1 / 4 ∑_S (F̂(S) - Ĝ(S)) ^ 2 (BitString.hammingDist_div_eq_sum_fourierCoeff_sub_sq) O'Donnell, Section 1.4.

Smoothing both functions by the noise operator T_ρ before comparing them gives the noise distance D_ρ(f, g) = 1 / 4 𝔼 (T_ρ F - T_ρ G) ^ 2 (BitString.noiseDist). The noise operator damps the coefficient on S by ρ ^ |S|, so D_ρ(f, g) = 1 / 4 ∑_S ρ ^ (2 |S|) (F̂(S) - Ĝ(S)) ^ 2 (BitString.noiseDist_eq_sum), the noise stability of F - G at ρ ^ 2 up to the factor 1 / 4 (BitString.noiseDist_eq_noiseStability). At ρ = 1 it is the relative Hamming distance (BitString.noiseDist_one), and it shrinks as |ρ| decreases (BitString.noiseDist_mono), so on |ρ| ≤ 1 noise contracts the relative Hamming distance (BitString.noiseDist_le_hammingDist_div). High-degree disagreements are damped most: two distinct parities on sets of size k are at relative Hamming distance 1 / 2, but at noise distance ρ ^ (2 k) / 2 (BitString.noiseDist_parityOn).

The damped coefficients ρ ^ |S| F̂(S) / 2 are a point of the Euclidean space indexed by the sets of coordinates (BitString.noiseEmbedding), and √D_ρ is the Euclidean distance between the points of f and g (BitString.dist_noiseEmbedding). Hence √D_ρ satisfies the triangle inequality (BitString.sqrt_noiseDist_triangle), and for ρ ≠ 0 it separates Boolean functions (BitString.noiseDist_eq_zero_iff), since a function is determined by its Fourier coefficients. So √D_ρ is a metric on Boolean functions for every ρ ≠ 0 (BitString.noiseMetricSpace); for ρ = 1 this is the square root of the relative Hamming distance, which is therefore a Euclidean metric. The noise distance is an average over a probability distribution only for |ρ| ≤ 1, but the algebraic statements hold for every real ρ.

Main definitions

• Cslib.BitString.noiseDist: the noise distance D_ρ between Boolean functions.
• Cslib.BitString.noiseEmbedding: the damped Fourier coefficients, as a point of Euclidean space.
• Cslib.BitString.noiseMetricSpace: the metric √D_ρ, for ρ ≠ 0.

Main results

• Cslib.BitString.hammingDist_div_eq_sum_fourierCoeff_sub_sq: the relative Hamming distance is a quarter of the squared distance between the Fourier coefficients.
• Cslib.BitString.noiseDist_eq_sum, Cslib.BitString.noiseDist_eq_noiseStability: the Fourier formula for the noise distance.
• Cslib.BitString.noiseDist_one, Cslib.BitString.noiseDist_mono, Cslib.BitString.noiseDist_le_hammingDist_div: noise contracts the relative Hamming distance.
• Cslib.BitString.noiseDist_parityOn: the noise distance between two distinct parities.
• Cslib.BitString.dist_noiseEmbedding, Cslib.BitString.sqrt_noiseDist_triangle, Cslib.BitString.noiseDist_eq_zero_iff: √D_ρ is a Euclidean metric.

References

• R. O'Donnell, Analysis of Boolean Functions

The Hamming distance and the Fourier coefficients

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

The mean squared difference of two Boolean functions read as signs is four times their relative Hamming distance.

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

The relative Hamming distance in the Fourier basis: it is a quarter of the squared Euclidean distance between the Fourier coefficients of the two functions read as signs, d_H(f, g) / 2 ^ n = 1 / 4 ∑_S (F̂(S) - Ĝ(S)) ^ 2, by Parseval's identity for F - G O'Donnell, Section 1.4.

The noise distance

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

The noise distance D_ρ(f, g) between two Boolean functions: a quarter of the mean squared difference of T_ρ F and T_ρ G, for F and G the functions read as signs and T_ρ the noise operator. For |ρ| ≤ 1 it compares f and g after averaging each over the strings ρ-correlated with the input.

theorem Cslib.BitString.noiseDist_eq_noiseStability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f g : (ι → Bool) → Bool) : noiseDist ρ f g = (noiseStability (ρ ^ 2) fun (x : ι → Bool) => signVal (f x) - signVal (g x)) / 4

The noise distance is a quarter of the noise stability of F - G at ρ ^ 2.

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

The Fourier formula for the noise distance: D_ρ(f, g) = 1 / 4 ∑_S ρ ^ (2 |S|) (F̂(S) - Ĝ(S)) ^ 2.

theorem Cslib.BitString.noiseDist_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → Bool) : noiseDist 1 f g = ↑(hammingDist f g) / 2 ^ Fintype.card ι

Without noise, the noise distance is the relative Hamming distance.

theorem Cslib.BitString.noiseDist_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → Bool) : noiseDist 0 f g = ((Finset.univ.expect fun (x : ι → Bool) => signVal (f x)) - Finset.univ.expect fun (x : ι → Bool) => signVal (g x)) ^ 2 / 4

With full noise, the noise distance compares only the means.

theorem Cslib.BitString.noiseDist_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f g : (ι → Bool) → Bool) : 0 ≤ noiseDist ρ f g

The noise distance is nonnegative.

theorem Cslib.BitString.noiseDist_comm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f g : (ι → Bool) → Bool) : noiseDist ρ f g = noiseDist ρ g f

The noise distance is symmetric.

@[simp]

theorem Cslib.BitString.noiseDist_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f : (ι → Bool) → Bool) : noiseDist ρ f f = 0

A Boolean function is at noise distance zero from itself.

theorem Cslib.BitString.noiseDist_mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ σ : ℝ} (h : |ρ| ≤ |σ|) (f g : (ι → Bool) → Bool) : noiseDist ρ f g ≤ noiseDist σ f g

The noise distance grows with |ρ|.

theorem Cslib.BitString.noiseDist_le_hammingDist_div {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ : ℝ} (h : |ρ| ≤ 1) (f g : (ι → Bool) → Bool) : noiseDist ρ f g ≤ ↑(hammingDist f g) / 2 ^ Fintype.card ι

Noise contracts the relative Hamming distance: for |ρ| ≤ 1, the noise distance is at most the relative Hamming distance.

theorem Cslib.BitString.noiseDist_parityOn {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) {S T : Finset ι} (h : S ≠ T) : noiseDist ρ (parityOn S) (parityOn T) = (ρ ^ (2 * S.card) + ρ ^ (2 * T.card)) / 4

Two distinct parities on sets S and T are at noise distance (ρ ^ (2 |S|) + ρ ^ (2 |T|)) / 4: all their Fourier weight sits on S and T.

The Euclidean embedding

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

The point of a Boolean function in the Euclidean space indexed by the sets of coordinates: its Fourier coefficients, read as signs, damped by ρ ^ |S| and halved.

theorem Cslib.BitString.noiseDist_eq_dist_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f g : (ι → Bool) → Bool) : noiseDist ρ f g = dist (noiseEmbedding ρ f) (noiseEmbedding ρ g) ^ 2

The noise distance is the squared Euclidean distance between the embedded functions.

theorem Cslib.BitString.dist_noiseEmbedding {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f g : (ι → Bool) → Bool) : dist (noiseEmbedding ρ f) (noiseEmbedding ρ g) = √(noiseDist ρ f g)

The square root of the noise distance is a Euclidean distance.

theorem Cslib.BitString.sqrt_noiseDist_triangle {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : ℝ) (f g h : (ι → Bool) → Bool) : √(noiseDist ρ f h) ≤ √(noiseDist ρ f g) + √(noiseDist ρ g h)

The triangle inequality for the square root of the noise distance.

theorem Cslib.BitString.noiseEmbedding_injective {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ : ℝ} (hρ : ρ ≠ 0) : Function.Injective (noiseEmbedding ρ)

For ρ ≠ 0 the embedding is injective: the damping is invertible, a function is determined by its Fourier coefficients, and a Boolean function by its signs.

theorem Cslib.BitString.noiseDist_eq_zero_iff {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ : ℝ} (hρ : ρ ≠ 0) {f g : (ι → Bool) → Bool} : noiseDist ρ f g = 0 ↔ f = g

For ρ ≠ 0, the noise distance separates Boolean functions.

@[reducible, inline]

noncomputable abbrev Cslib.BitString.noiseMetricSpace {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ : ℝ} (hρ : ρ ≠ 0) : MetricSpace ((ι → Bool) → Bool)

The square root of the noise distance is a metric on Boolean functions, for ρ ≠ 0: the metric induced by the Euclidean embedding. For ρ = 1 it is the square root of the relative Hamming distance. This is a definition, not an instance, since it depends on ρ.

theorem Cslib.BitString.noiseMetricSpace_dist {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ρ : ℝ} (hρ : ρ ≠ 0) (f g : (ι → Bool) → Bool) : dist f g = √(noiseDist ρ f g)

The distance in noiseMetricSpace is the square root √D_ρ of the noise distance.