Analysis on Boolean functions

This file contains some basic definitions and theorems for analysis of real-valued Boolean functions mainly following Ryan O'Donnell's book [odonnell2014]. The Hamming cube is represented by the function type Fin n → Fin 2, so that a BooleanFunc n is a (Fin n → Fin 2) → ℝ.

Thanks to Mathlib, it is relatively straightforward to get started with Fourier analysis:

• Typeclass inference automatically equips BooleanFunc n with the appropriate ℝ-vector space structure.
• We define inner product space structure via InnerProductSpace.Core and show that the walshCharacters form an orthonormal basis.
• Then Plancherel's theorem follows from Mathlib's OrthogonalFamily.inner_sum.

Even if there was a general framework for Fourier transforms on LCA groups in Mathlib, it may be preferrable to use this ad-hoc definition due to slightly different notational conventions in the context of Boolean functions, and the simplicity of working with finite sums.

Main results

• walsh_fourier expresses a Boolean function in terms of its Walsh-Fourier transform
• variance_le_totalInfluence is a version of the classical L² Poincaré inequality
• fourier_convolution is the convolution theorem for the Walsh-Fourier transform

Notation

• 𝐄 denotes expectation with respect to uniform probability measure
• χ S denotes the Walsh character associated with an S : Finset (Fin n)
• 𝓕 denotes the Walsh-Fourier transform fourierTransform
• ⟨⬝, ⬝⟩ denotes the inner product defined as expectation of product
• ‖⬝‖ denotes the (normalized) L² norm
• ⋆ denotes convolution

@[reducible, inline]

abbrev LeanPool.LeanBooleanfun.BooleanFun.BooleanFunc (n : ℕ) : Type

A Boolean function maps an n-tuple of bits (of type Fin n → Fin 2) to a real number.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.BooleanFunc n = ((Fin n → Fin 2) → ℝ)

theorem LeanPool.LeanBooleanfun.BooleanFun.add_self_eq_zero {n : ℕ} (a : Fin n → Fin 2) : a + a = 0

theorem LeanPool.LeanBooleanfun.BooleanFun.sum_translate {n : ℕ} {f : BooleanFunc n} (a : Fin n → Fin 2) : ∑ x : Fin n → Fin 2, f x = ∑ x : Fin n → Fin 2, f (x + a)

Translation invariance

noncomputable def LeanPool.LeanBooleanfun.BooleanFun.expectation {n : ℕ} : BooleanFunc n →ₗ[ℝ] ℝ

The expectation of a Boolean function is its average value with respect to the uniform probability measure on Fin n → Fin 2.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.expectation = { toFun := fun (f : LeanPool.LeanBooleanfun.BooleanFun.BooleanFunc n) => (1 / 2) ^ n * ∑ i : Fin n → Fin 2, f i, map_add' := ⋯, map_smul' := ⋯ }

def LeanPool.LeanBooleanfun.BooleanFun.«term𝐄» : Lean.ParserDescr

Expectation of a Boolean function

Equations

• LeanPool.LeanBooleanfun.BooleanFun.«term𝐄» = Lean.ParserDescr.node `LeanPool.LeanBooleanfun.BooleanFun.«term𝐄» 1024 (Lean.ParserDescr.symbol "𝐄")

@[reducible, inline]

abbrev LeanPool.LeanBooleanfun.BooleanFun.walshCharacter {n : ℕ} (S : Finset (Fin n)) : BooleanFunc n

Definition of Walsh character

Equations

• LeanPool.LeanBooleanfun.BooleanFun.walshCharacter S x = ∏ i ∈ S, (-1) ^ ↑(x i)

def LeanPool.LeanBooleanfun.BooleanFun.termχ : Lean.ParserDescr

Walsh character

Equations

• LeanPool.LeanBooleanfun.BooleanFun.termχ = Lean.ParserDescr.node `LeanPool.LeanBooleanfun.BooleanFun.termχ 1024 (Lean.ParserDescr.symbol "χ")

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_def {n : ℕ} {x : Fin n → Fin 2} {S : Finset (Fin n)} : walshCharacter S x = ∏ i ∈ S, (-1) ^ ↑(x i)

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_ne_zero {n : ℕ} {x : Fin n → Fin 2} {S : Finset (Fin n)} : walshCharacter S x ≠ 0

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_eq_neg_one_pow_sum {n : ℕ} {x : Fin n → Fin 2} {S : Finset (Fin n)} : walshCharacter S x = (-1) ^ ∑ i ∈ S, ↑(x i)

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_add {n : ℕ} {x y : Fin n → Fin 2} {S : Finset (Fin n)} : walshCharacter S (x + y) = walshCharacter S x * walshCharacter S y

Walsh characters are characters.

@[reducible, inline]

abbrev LeanPool.LeanBooleanfun.BooleanFun.BooleanFunc' (n : ℕ) : Type

Dual space of Boolean functions as the type of real-valued functions on Finset (Fin n).

Equations

• LeanPool.LeanBooleanfun.BooleanFun.BooleanFunc' n = (Finset (Fin n) → ℝ)

noncomputable def LeanPool.LeanBooleanfun.BooleanFun.fourierTransform {n : ℕ} : BooleanFunc n →ₗ[ℝ] BooleanFunc' n

The Walsh-Fourier transform of a Boolean function f is defined on sets of coordinates S : Finset (Fin n) as expectation of the Walsh character χ S times f.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.LeanBooleanfun.BooleanFun.term𝓕 : Lean.ParserDescr

Walsh-Fourier transform on Boolean functions

Equations

• LeanPool.LeanBooleanfun.BooleanFun.term𝓕 = Lean.ParserDescr.node `LeanPool.LeanBooleanfun.BooleanFun.term𝓕 1024 (Lean.ParserDescr.symbol "𝓕")

theorem LeanPool.LeanBooleanfun.BooleanFun.expectation_eq_fourier {n : ℕ} {f : BooleanFunc n} : expectation f = fourierTransform f ∅

theorem LeanPool.LeanBooleanfun.BooleanFun.expectation_prod_self_nonneg {n : ℕ} {f : BooleanFunc n} : 0 ≤ expectation (f * f)

@[implicit_reducible]

noncomputable instance LeanPool.LeanBooleanfun.BooleanFun.instCoreReal {n : ℕ} : InnerProductSpace.Core ℝ (BooleanFunc n)

Boolean functions form an inner product space.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible, instance 10000]

noncomputable instance LeanPool.LeanBooleanfun.BooleanFun.instNormedAddCommGroupReal {n : ℕ} : NormedAddCommGroup (BooleanFunc n)

Equations

• LeanPool.LeanBooleanfun.BooleanFun.instNormedAddCommGroupReal = InnerProductSpace.Core.toNormedAddCommGroup

@[implicit_reducible, instance 10000]

noncomputable instance LeanPool.LeanBooleanfun.BooleanFun.instSeminormedReal {n : ℕ} : SeminormedAddCommGroup (BooleanFunc n)

Equations

• LeanPool.LeanBooleanfun.BooleanFun.instSeminormedReal = NormedAddCommGroup.toSeminormedAddCommGroup

@[implicit_reducible, instance 10000]

noncomputable instance LeanPool.LeanBooleanfun.BooleanFun.instNormReal {n : ℕ} : Norm (BooleanFunc n)

Equations

• LeanPool.LeanBooleanfun.BooleanFun.instNormReal = LeanPool.LeanBooleanfun.BooleanFun.instSeminormedReal.toNorm

@[implicit_reducible, instance 10000]

noncomputable instance LeanPool.LeanBooleanfun.BooleanFun.instInnerProductSpaceReal {n : ℕ} : InnerProductSpace ℝ (BooleanFunc n)

Equations

• LeanPool.LeanBooleanfun.BooleanFun.instInnerProductSpaceReal = InnerProductSpace.ofCore inferInstance

theorem LeanPool.LeanBooleanfun.BooleanFun.cauchy_schwarz {n : ℕ} {f g : BooleanFunc n} : |inner ℝ f g| ≤ ‖f‖ * ‖g‖

Cauchy-Schwarz inequality on Boolean functions

@[simp]

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_sq_eq_one {n : ℕ} {S : Finset (Fin n)} : walshCharacter S ^ 2 = 1

@[simp]

theorem LeanPool.LeanBooleanfun.BooleanFun.expectation_one {n : ℕ} : expectation 1 = 1

theorem LeanPool.LeanBooleanfun.BooleanFun.norm_sq_eq_inner {n : ℕ} {f : BooleanFunc n} : ‖f‖ ^ 2 = inner ℝ f f

@[simp]

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_norm_one {n : ℕ} (S : Finset (Fin n)) : ‖walshCharacter S‖ = 1

Walsh characters are L² normalized.

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_inner_self_eq_one {n : ℕ} {S : Finset (Fin n)} : inner ℝ (walshCharacter S) (walshCharacter S) = 1

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_mul_eq {n : ℕ} {S S' : Finset (Fin n)} : walshCharacter S * walshCharacter S' = walshCharacter (symmDiff S S')

theorem LeanPool.LeanBooleanfun.BooleanFun.inner_eq_expectation {n : ℕ} {f g : BooleanFunc n} : inner ℝ f g = expectation (f * g)

theorem LeanPool.LeanBooleanfun.BooleanFun.fourier_eq_inner {n : ℕ} {f : BooleanFunc n} {S : Finset (Fin n)} : fourierTransform f S = inner ℝ (walshCharacter S) f

def LeanPool.LeanBooleanfun.BooleanFun.flipAt {n : ℕ} (i₀ : Fin n) (x : Fin n → Fin 2) : Fin n → Fin 2

Flip the i₀th bit of x.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.flipAt i₀ x i = if i = i₀ then 1 - x i else x i

@[simp]

theorem LeanPool.LeanBooleanfun.BooleanFun.flipAt_flipped {n : ℕ} {i₀ : Fin n} {x : Fin n → Fin 2} : flipAt i₀ x i₀ = 1 - x i₀

The i₀th bit of x is flipped.

theorem LeanPool.LeanBooleanfun.BooleanFun.flipAt_unflipped {n : ℕ} {i i₀ : Fin n} {x : Fin n → Fin 2} (h : i ≠ i₀) : flipAt i₀ x i = x i

Bits that are not the i₀th bits remain unchanged.

@[simp]

theorem LeanPool.LeanBooleanfun.BooleanFun.flipAt_flipAt_eq {n : ℕ} {i₀ : Fin n} {x : Fin n → Fin 2} : flipAt i₀ (flipAt i₀ x) = x

Flipping a bit twice results in no change.

theorem LeanPool.LeanBooleanfun.BooleanFun.flipAt_involutive {n : ℕ} {i₀ : Fin n} : Function.Involutive (flipAt i₀)

Flipping a bit is an involution on Fin n → Fin 2.

theorem LeanPool.LeanBooleanfun.BooleanFun.flipAt_bijective {n : ℕ} {i₀ : Fin n} : Function.Bijective (flipAt i₀)

Flipping a bit is a bijection on Fin n → Fin 2.

@[simp]

theorem LeanPool.LeanBooleanfun.BooleanFun.expectation_walsh_eq_zero {n : ℕ} {S : Finset (Fin n)} (hS : S.Nonempty) : expectation (walshCharacter S) = 0

Expectation of χ S is zero if S is nonempty

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_orthogonal {n : ℕ} {S S' : Finset (Fin n)} (h : S ≠ S') : inner ℝ (walshCharacter S) (walshCharacter S') = 0

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_inner_eq {n : ℕ} {S S' : Finset (Fin n)} : inner ℝ (walshCharacter S) (walshCharacter S') = oneOn (S = S')

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_orthonormal {n : ℕ} : Orthonormal ℝ walshCharacter

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.walshBasis {n : ℕ} : Module.Basis (Finset (Fin n)) ℝ (BooleanFunc n)

Basis of Walsh characters on BooleanFunc n.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.walshBasis = basisOfOrthonormalOfCardEqFinrank ⋯ ⋯

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.walshOrthonormalBasis {n : ℕ} : OrthonormalBasis (Finset (Fin n)) ℝ (BooleanFunc n)

Orthonormal basis of Walsh characters on BooleanFunc n.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.walshOrthonormalBasis = (basisOfOrthonormalOfCardEqFinrank ⋯ ⋯).toOrthonormalBasis ⋯

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_fourier {n : ℕ} (f : BooleanFunc n) : f = ∑ S : Finset (Fin n), fourierTransform f S • walshCharacter S

Walsh-Fourier expansion : Every Boolean function is equal to a linear combination of Walsh characters.

theorem LeanPool.LeanBooleanfun.BooleanFun.fourier_walsh {n : ℕ} {S S' : Finset (Fin n)} : fourierTransform (walshCharacter S) S' = oneOn (S' = S)

theorem LeanPool.LeanBooleanfun.BooleanFun.inner_eq_sum_fourier {n : ℕ} {f g : BooleanFunc n} : inner ℝ f g = ∑ S : Finset (Fin n), fourierTransform f S * fourierTransform g S

Plancherel/Parseval theorem for Boolean functions.

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_plancherel {n : ℕ} {f : BooleanFunc n} : ‖f‖ ^ 2 = ∑ S : Finset (Fin n), |fourierTransform f S| ^ 2

Plancherel/Parseval theorem for Boolean functions.

@[reducible, inline]

abbrev LeanPool.LeanBooleanfun.BooleanFun.setAt {n : ℕ} (i₀ : Fin n) (v : Fin 2) (x : Fin n → Fin 2) : Fin n → Fin 2

Set the i₀th bit of x to v.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.setAt i₀ v x i = if i = i₀ then v else x i

@[simp]

theorem LeanPool.LeanBooleanfun.BooleanFun.setAt_it {n : ℕ} (i₀ : Fin n) (v : Fin 2) (x : Fin n → Fin 2) : setAt i₀ v x i₀ = v

The i₀th bit of setAt i₀ v x has value v.

theorem LeanPool.LeanBooleanfun.BooleanFun.setAt_other {n : ℕ} (i₀ : Fin n) (v : Fin 2) (x : Fin n → Fin 2) (i : Fin n) (h : i₀ ≠ i) : setAt i₀ v x i = x i

Bits other than the i₀th bit are unaffected by setAt.

noncomputable def LeanPool.LeanBooleanfun.BooleanFun.dderiv {n : ℕ} (i : Fin n) : BooleanFunc n →ₗ[ℝ] BooleanFunc n

Discrete partial "derivative" of a Boolean function with respect to the ith coordinate. See Def. 2.16 in [odonnell2014].

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.LeanBooleanfun.BooleanFun.walsh_setAt_eq_ite {n : ℕ} {x : Fin n → Fin 2} {i : Fin n} {S : Finset (Fin n)} {v : Fin 2} : walshCharacter S (setAt i v x) = if i ∈ S then (-1) ^ ↑v * walshCharacter (S \ {i}) x else walshCharacter S x

theorem LeanPool.LeanBooleanfun.BooleanFun.dderiv_walsh {n : ℕ} (i : Fin n) (S : Finset (Fin n)) : (dderiv i) (walshCharacter S) = if i ∈ S then walshCharacter (S \ {i}) else 0

theorem LeanPool.LeanBooleanfun.BooleanFun.dderiv_eq_sum_fourier {n : ℕ} (i : Fin n) (f : BooleanFunc n) : (dderiv i) f = ∑ S : Finset (Fin n) with i ∈ S, fourierTransform f S • walshCharacter (S \ {i})

noncomputable def LeanPool.LeanBooleanfun.BooleanFun.laplace {n : ℕ} (i : Fin n) : BooleanFunc n →ₗ[ℝ] BooleanFunc n

The ith coordinate Laplacian operator as in Def. 2.25 [odonnell2014].

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.LeanBooleanfun.BooleanFun.setAt_eq_id {n : ℕ} {x : Fin n → Fin 2} {i : Fin n} {v : Fin 2} (h : x i = v) : setAt i v x = x

theorem LeanPool.LeanBooleanfun.BooleanFun.setAt_eq_flipAt {n : ℕ} {x : Fin n → Fin 2} {i : Fin n} {v : Fin 2} (h : x i ≠ v) : setAt i v x = flipAt i x

theorem LeanPool.LeanBooleanfun.BooleanFun.laplace_eq_dderiv {n : ℕ} (i : Fin n) (f : BooleanFunc n) (x : Fin n → Fin 2) : (laplace i) f x = (-1) ^ ↑(x i) * (dderiv i) f x

theorem LeanPool.LeanBooleanfun.BooleanFun.laplace_walsh {n : ℕ} (i : Fin n) (S : Finset (Fin n)) : (laplace i) (walshCharacter S) = if i ∈ S then walshCharacter S else 0

theorem LeanPool.LeanBooleanfun.BooleanFun.laplace_eq_sum_fourier {n : ℕ} (i : Fin n) (f : BooleanFunc n) : (laplace i) f = ∑ S : Finset (Fin n) with i ∈ S, fourierTransform f S • walshCharacter S

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.influence {n : ℕ} (f : BooleanFunc n) (i : Fin n) : ℝ

The ith influence of a Boolean function is defined as the expectation of the ith Laplacian squared.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.influence f i = LeanPool.LeanBooleanfun.BooleanFun.expectation ((LeanPool.LeanBooleanfun.BooleanFun.laplace i) f ^ 2)

theorem LeanPool.LeanBooleanfun.BooleanFun.influence_eq_sum_fourier {n : ℕ} (f : BooleanFunc n) (i : Fin n) : influence f i = ∑ S : Finset (Fin n) with i ∈ S, fourierTransform f S ^ 2

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.totalInfluence {n : ℕ} (f : BooleanFunc n) : ℝ

The total influence of a Boolean function is defined as the sum of the ith influences.

Equations

• LeanPool.LeanBooleanfun.BooleanFun.totalInfluence f = ∑ i : Fin n, LeanPool.LeanBooleanfun.BooleanFun.influence f i

theorem LeanPool.LeanBooleanfun.BooleanFun.totalInfluence_eq_sum_fourier {n : ℕ} (f : BooleanFunc n) : totalInfluence f = ∑ S : Finset (Fin n), ↑S.card * fourierTransform f S ^ 2

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.covariance {n : ℕ} (f g : BooleanFunc n) : ℝ

Covariance of two Boolean functions

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.variance {n : ℕ} (f : BooleanFunc n) : ℝ

Variance of a Boolean function defined via covariance

Equations

• LeanPool.LeanBooleanfun.BooleanFun.variance f = LeanPool.LeanBooleanfun.BooleanFun.covariance f f

theorem LeanPool.LeanBooleanfun.BooleanFun.covariance_eq_sum_fourier {n : ℕ} (f g : BooleanFunc n) : covariance f g = ∑ S : Finset (Fin n) with S.Nonempty, fourierTransform f S * fourierTransform g S

theorem LeanPool.LeanBooleanfun.BooleanFun.variance_eq_sum_fourier {n : ℕ} (f : BooleanFunc n) : variance f = ∑ S : Finset (Fin n) with S.Nonempty, fourierTransform f S ^ 2

theorem LeanPool.LeanBooleanfun.BooleanFun.variance_le_totalInfluence {n : ℕ} (f : BooleanFunc n) : variance f ≤ totalInfluence f

L² Poincaré inequality : variance of a Boolean function is ≤ total Influence. See [odonnell2014], Sec. 2.3.

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.fourierWeight {n : ℕ} (k : ℕ) (f : BooleanFunc n) : ℝ

The kth Fourier weight is the sum of squares of degree k Fourier coefficients

Equations

• LeanPool.LeanBooleanfun.BooleanFun.fourierWeight k f = ∑ S : Finset (Fin n) with S.card = k, |LeanPool.LeanBooleanfun.BooleanFun.fourierTransform f S| ^ 2

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.fourierWeightOne {n : ℕ} (f : BooleanFunc n) : ℝ

Alternative expression for degree one Fourier weight in terms in terms of sum over coordinates

Equations

• LeanPool.LeanBooleanfun.BooleanFun.fourierWeightOne f = ∑ i : Fin n, |LeanPool.LeanBooleanfun.BooleanFun.fourierTransform f {i}| ^ 2

theorem LeanPool.LeanBooleanfun.BooleanFun.fourier_weight_one {n : ℕ} {f : BooleanFunc n} : fourierWeight 1 f = fourierWeightOne f

theorem LeanPool.LeanBooleanfun.BooleanFun.fourier_eq_zero_iff_fourier_weight_eq {n k : ℕ} {f : BooleanFunc n} : (∀ (S : Finset (Fin n)), S.card ≠ k → fourierTransform f S = 0) ↔ fourierWeight k f = ‖f‖ ^ 2

theorem LeanPool.LeanBooleanfun.BooleanFun.eq_sum_fourier_of_fourier_weight {n k : ℕ} {f : BooleanFunc n} (h : fourierWeight k f = ‖f‖ ^ 2) : f = ∑ S : Finset (Fin n) with S.card = k, fourierTransform f S • walshCharacter S

theorem LeanPool.LeanBooleanfun.BooleanFun.eq_sum_degree_one_of_fourier_weight_one {n : ℕ} {f : BooleanFunc n} (h : fourierWeight 1 f = ‖f‖ ^ 2) (x : Fin n → Fin 2) : f x = ∑ i : Fin n, fourierTransform f {i} * (-1) ^ ↑(x i)

theorem LeanPool.LeanBooleanfun.BooleanFun.eq_sum_degree_one_of_fourier_eq_zero {n : ℕ} {f : BooleanFunc n} (h : ∀ (S : Finset (Fin n)), S.card ≠ 1 → fourierTransform f S = 0) (x : Fin n → Fin 2) : f x = ∑ i : Fin n, fourierTransform f {i} * (-1) ^ ↑(x i)

noncomputable def LeanPool.LeanBooleanfun.BooleanFun.multiplier {n : ℕ} (m : ℕ → ℝ) : BooleanFunc n →ₗ[ℝ] BooleanFunc n

Walsh-Fourier multiplier as an ℝ-linear operator on Boolean functions

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.LeanBooleanfun.BooleanFun.multiplier_walsh {n : ℕ} {m : ℕ → ℝ} {S : Finset (Fin n)} : (multiplier m) (walshCharacter S) = m S.card • walshCharacter S

Walsh characters are eigenfunctions of multipliers.

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.noiseOperator {n : ℕ} (ρ : ℝ) : BooleanFunc n →ₗ[ℝ] BooleanFunc n

The noise operator defined via Fourier expansion. See Prop. 2.47 in [odonnell2014].

Equations

• LeanPool.LeanBooleanfun.BooleanFun.noiseOperator ρ = LeanPool.LeanBooleanfun.BooleanFun.multiplier fun (x : ℕ) => ρ ^ x

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.noiseStability {n : ℕ} (ρ : ℝ) (f : BooleanFunc n) : ℝ

Noise stability

Equations

• LeanPool.LeanBooleanfun.BooleanFun.noiseStability ρ f = inner ℝ f ((LeanPool.LeanBooleanfun.BooleanFun.noiseOperator ρ) f)

theorem LeanPool.LeanBooleanfun.BooleanFun.noise_stability_eq_sum_fourier {n : ℕ} {f : BooleanFunc n} {ρ : ℝ} : noiseStability ρ f = ∑ S : Finset (Fin n), ρ ^ S.card * |fourierTransform f S| ^ 2

@[reducible, inline]

noncomputable abbrev LeanPool.LeanBooleanfun.BooleanFun.convolution {n : ℕ} (f g : BooleanFunc n) : BooleanFunc n

Discrete convolution of Boolean functions

Equations

• (f⋆g) x = LeanPool.LeanBooleanfun.BooleanFun.expectation fun (y : Fin n → Fin 2) => f y * g (x + y)

def LeanPool.LeanBooleanfun.BooleanFun.«term_⋆_» : Lean.TrailingParserDescr

Discrete convolution of Boolean functions

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.LeanBooleanfun.BooleanFun.fourier_convolution {n : ℕ} {f g : BooleanFunc n} : fourierTransform (f⋆g) = fourierTransform f * fourierTransform g

Convolution theorem : the Walsh-Fourier transform turns convolution into pointwise product.