The Fourier expansion on the cube and the meaning of HasDegreeLE

The characters chi S are an orthogonal basis of the functions on the cube. Consequences:

• every f has HasDegreeLE f (Fintype.card ι) (hasDegreeLE_card);
• the coefficients in HasDegreeLE are unique (fourier_unique);
• HasDegreeLE f d ↔ all Fourier coefficients above level d vanish (hasDegreeLE_iff_fourier);
• HasDegreeLE (chi S) d ↔ S.card ≤ d (hasDegreeLE_chi_iff), so HasDegreeLE separates every degree level and is not accidentally trivial.

noncomputable def AaronsonAmbainis.Bridge.sg (b : Bool) : ℝ

Sign of a bit: false ↦ 1, true ↦ -1.

Equations

• AaronsonAmbainis.Bridge.sg b = AaronsonAmbainis.Row.sgn b

theorem AaronsonAmbainis.Bridge.sg_mul_self (b : Bool) : sg b * sg b = 1

theorem AaronsonAmbainis.Bridge.sg_not (b : Bool) : (sg !b) = -sg b

theorem AaronsonAmbainis.Bridge.sg_mul_of_ne {a b : Bool} (h : a ≠ b) : sg a * sg b = -1

theorem AaronsonAmbainis.Bridge.chi_eq_prod_sg {ι : Type u_1} (S : Finset ι) (x : Cube ι) : chi S x = ∏ i ∈ S, sg (x i)

theorem AaronsonAmbainis.Bridge.chi_eq_prod_univ {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (x : Cube ι) : chi S x = ∏ i : ι, if i ∈ S then sg (x i) else 1

theorem AaronsonAmbainis.Bridge.chi_mul_chi {ι : Type u_1} [DecidableEq ι] [Finite ι] (S T : Finset ι) (x : Cube ι) : chi S x * chi T x = chi (symmDiff S T) x

χ_S χ_T = χ_{S Δ T}.

theorem AaronsonAmbainis.Bridge.chi_flip_mem {ι : Type u_1} [DecidableEq ι] {U : Finset ι} {j : ι} (hj : j ∈ U) (x : Cube ι) : chi U (flipSet x {j}) = -chi U x

Flipping a coordinate in U negates χ_U.

theorem AaronsonAmbainis.Bridge.sum_chi_mul_chi {ι : Type u_1} [Fintype ι] (x y : Cube ι) : ∑ S : Finset ι, chi S x * chi S y = if x = y then 2 ^ Fintype.card ι else 0

Orthogonality, summing over the characters.

theorem AaronsonAmbainis.Bridge.sum_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : Finset ι) : ∑ x : Cube ι, chi U x = if U = ∅ then 2 ^ Fintype.card ι else 0

∑_x χ_U(x) = 2^n [U = ∅].

theorem AaronsonAmbainis.Bridge.sum_chi_mul_chi_cube {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S T : Finset ι) : ∑ x : Cube ι, chi S x * chi T x = if S = T then 2 ^ Fintype.card ι else 0

Orthogonality, summing over the cube.

noncomputable def AaronsonAmbainis.Bridge.fourier {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (S : Finset ι) : ℝ

The Fourier coefficient of f at S.

Equations

• AaronsonAmbainis.Bridge.fourier f S = (∑ y : AaronsonAmbainis.Cube ι, f y * AaronsonAmbainis.chi S y) / 2 ^ Fintype.card ι

theorem AaronsonAmbainis.Bridge.fourier_inversion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (x : Cube ι) : ∑ S : Finset ι, fourier f S * chi S x = f x

Fourier inversion.

theorem AaronsonAmbainis.Bridge.hasDegreeLE_card {ι : Type u_1} [Fintype ι] (f : Cube ι → ℝ) : HasDegreeLE f (Fintype.card ι)

Every function on the cube has degree at most the number of coordinates.

theorem AaronsonAmbainis.Bridge.fourier_unique {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Cube ι → ℝ} {c : Finset ι → ℝ} (hf : ∀ (x : Cube ι), f x = ∑ S : Finset ι, c S * chi S x) (T : Finset ι) : c T = fourier f T

The coefficients of a character expansion are unique: they are the Fourier coefficients.

theorem AaronsonAmbainis.Bridge.hasDegreeLE_iff_fourier {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : Cube ι → ℝ} {d : ℕ} : HasDegreeLE f d ↔ ∀ (S : Finset ι), d < S.card → fourier f S = 0

HasDegreeLE f d says exactly that the Fourier coefficients above level d vanish.

theorem AaronsonAmbainis.Bridge.fourier_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S T : Finset ι) : fourier (chi S) T = if S = T then 1 else 0

theorem AaronsonAmbainis.Bridge.hasDegreeLE_chi_iff {ι : Type u_1} [Fintype ι] (S : Finset ι) (d : ℕ) : HasDegreeLE (chi S) d ↔ S.card ≤ d

A character χ_S has degree at most d exactly when |S| ≤ d.

theorem AaronsonAmbainis.Bridge.parity_not_hasDegreeLE {ι : Type u_1} [Fintype ι] {d : ℕ} (hd : d < Fintype.card ι) : ¬HasDegreeLE (chi Finset.univ) d

The full parity does not have degree < n: HasDegreeLE is not trivially true.