Section 6.4, paragraph 1Walsh–Hadamard characters are orthonormal; every f equals its Fourier expansion

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

A useful complementary lens is Fourier analysis on the Boolean hypercube. Let $f:\bits^{n}\to\mathbb{R}$ and define the Walsh–Hadamard characters $\chi_S(x) \;=\; (-1)^{\sum_{i\in S} x_i}, \qquad S\subseteq[n].$ The set $\{\chi_S\}_{S\subseteq[n]}$ is an orthonormal basis with respect to the uniform distribution on $\bits^n$ . The Fourier coefficients are $\hat f(S)\;=\;\mathbb{E}_{x\sim U(\bits^n)}\bigl[f(x)\chi_S(x)\bigr], \qquad\text{and}\qquad f(x)=\sum_{S\subseteq[n]}\hat f(S)\chi_S(x).$ We refer to $|S|$ as the Fourier degree (or “frequency”) of the coefficient $\hat f(S)$ .

Generated from paper_jmlr.tex, lines 936–948.

2 Explain this

Characters. For a set $S$ of input coordinates, $\chi_S(x)=(-1)^{\sum_{i\in S}x_i}$ is $+1$ or $-1$ according to the parity of the inputs in $S$ .

Basis. The $2^n$ characters are orthonormal under the uniform distribution, and every real function $f$ on $\{0,1\}^n$ is a unique combination $f=\sum_S\hat f(S)\chi_S$ with coefficients $\hat f(S)=\mathbb E[f\chi_S]$ .

Example. On two bits, AND (as a 0/1 function) is $\tfrac14-\tfrac14\chi_{{1}}-\tfrac14\chi_{{2}}+\tfrac14 \chi_{{1,2}}$.

The size $|S|$ is the degree or frequency of the coefficient. Parity of all inputs is the single highest-degree character.

3 How this is formalised

Checked over Mathlib's real numbers, for functions on Mathlib's finite cube Fin n → Bool:

RealFourier.chiF_formula: $\chi_S(x)=(-1)^{\sum_{i\in S}x_i}$ (RealFourier.chiF);
RealFourier.orthonormal_fin: orthonormality;
RealFourier.inversion_fin: every $F$ equals the sum of its Fourier series (coefficients RealFourier.fhat with the uniform normalisation);
RealFourier.uniqueness_fin: the expansion is unique;
RealFourier.parseval_fin: Parseval's identity.

All statements include $n=0$ . The same results are proved for any linearly ordered field in the list form used by the other modules (Fourier).

Coverage record
Paper anchor	`sec:spectral-view-p1` (website anchor; the manuscript has no label here)
Displayed as	Section 6.4, paragraph 1
Claim	Walsh–Hadamard characters are orthonormal; every f equals its Fourier expansion
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 936–948; SHA-256 of the normalised block source `9234e1d1315bf727…`
Lean declarations	`NimAudit.RealFourier.chiF_formula` (RealFourier, lines 75–77, file `e0e69edd199d…`) `NimAudit.RealFourier.orthonormal_fin` (RealFourier, lines 116–126, file `e0e69edd199d…`) `NimAudit.RealFourier.inversion_fin` (RealFourier, lines 107–114, file `e0e69edd199d…`) `NimAudit.RealFourier.uniqueness_fin` (RealFourier, lines 128–138, file `e0e69edd199d…`) `NimAudit.RealFourier.parseval_fin` (RealFourier, lines 140–150, file `e0e69edd199d…`)
Audited correspondence rows	`def:fourier-tail`
Explanations	`explain/c-fourier-basis`, `formal/c-fourier-basis`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `RealFourier.chiF_formula`

Module RealFourier (lean/phase8/RealFourier.lean, lines 75–77) · file SHA-256 e0e69edd199d8650… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

THE PAPER'S FORMULA: χ_S(x) = (−1)^{Σ_{i∈S} x_i}.

Statement as elaborated and printed by Lean 4.26.0

∀ {n : ℕ} (S x : Fin n → Bool),
  NimAudit.RealFourier.chiF S x = (-1) ^ ∑ i, if (S i && x i) = true then 1 else 0

Exact source text, lines 75–77

75/-- THE PAPER'S FORMULA: χ_S(x) = (−1)^{Σ_{i∈S} x_i}. -/76theorem chiF_formula {n : ℕ} (S x : Fin n → Bool) : chiF S x = (-1) ^ (∑ i, if S i && x i then 1 else 0) := by77  unfold chiF; rw [chi_pow, selCount_toL]

Project declarations in the statement: RealFourier.chiF

Project declarations used by the proof or definition body

Fourier.chi, Fourier.chi_pow, Fourier.selCount, RealFourier.chiF, RealFourier.selCount_toL, RealFourier.toL

theorem `RealFourier.orthonormal_fin`

Module RealFourier (lean/phase8/RealFourier.lean, lines 116–126) · file SHA-256 e0e69edd199d8650… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

ORTHONORMALITY (Fin form).

Statement as elaborated and printed by Lean 4.26.0

∀ {n : ℕ} (S T : Fin n → Bool),
  (2 ^ n)⁻¹ * ∑ x, NimAudit.RealFourier.chiF S x * NimAudit.RealFourier.chiF T x =
    if S = T then 1 else 0

Exact source text, lines 116–126

116/-- ORTHONORMALITY (Fin form). -/117theorem orthonormal_fin {n : ℕ} (S T : Fin n → Bool) :118    (2 ^ n)⁻¹ * ∑ x, chiF S x * chiF T x = if S = T then 1 else 0 := by119  have h := orthonormal (R := ℝ) (toL_mem S) (toL_mem T)120  unfold ip at h121  rw [gs_eq_fintype_sum, mul_comm] at h122  rw [show (if S = T then (1 : ℝ) else 0) = if toL S = toL T then 1 else 0 by123    by_cases hST : S = T124    · simp [hST]125    · rw [if_neg hST, if_neg (fun e => hST (toL_injective n e))]]126  rw [← h]; rfl

Project declarations in the statement: RealFourier.chiF

Project declarations used by the proof or definition body

Bridge.bitvecs, Fourier.chi, Fourier.ip, Fourier.orthonormal, Noise.gs, RealFourier.chiF, RealFourier.gs_eq_fintype_sum, RealFourier.toL, RealFourier.toL_injective, RealFourier.toL_mem

theorem `RealFourier.inversion_fin`

Module RealFourier (lean/phase8/RealFourier.lean, lines 107–114) · file SHA-256 e0e69edd199d8650… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

B1 AT ℝ (Fin form). FOURIER INVERSION for every F : (Fin n → Bool) → ℝ.

Statement as elaborated and printed by Lean 4.26.0

∀ {n : ℕ} (F : (Fin n → Bool) → ℝ) (x : Fin n → Bool),
  F x = ∑ S, NimAudit.RealFourier.fhat F S * NimAudit.RealFourier.chiF S x

Exact source text, lines 107–114

107/-- B1 AT ℝ (Fin form). FOURIER INVERSION for every F : (Fin n → Bool) → ℝ. -/108theorem inversion_fin {n : ℕ} (F : (Fin n → Bool) → ℝ) (x : Fin n → Bool) :109    F x = ∑ S, fhat F S * chiF S x := by110  have h := inversion (R := ℝ) n (lift F) (toL_mem x)111  rw [lift_toL, gs_eq_fintype_sum] at h112  rw [← h]113  apply Finset.sum_congr rfl; intro S _114  rw [fhat_eq_coef]; rfl

Project declarations in the statement: RealFourier.chiF, RealFourier.fhat

Project declarations used by the proof or definition body

Bridge.bitvecs, Fourier.chi, Fourier.coef, Fourier.inversion, Noise.gs, RealFourier.chiF, RealFourier.fhat, RealFourier.fhat_eq_coef, RealFourier.gs_eq_fintype_sum, RealFourier.lift, RealFourier.lift_toL, RealFourier.toL, RealFourier.toL_mem

theorem `RealFourier.uniqueness_fin`

Module RealFourier (lean/phase8/RealFourier.lean, lines 128–138) · file SHA-256 e0e69edd199d8650… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

UNIQUENESS (Fin form).

Statement as elaborated and printed by Lean 4.26.0

∀ {n : ℕ} (F c : (Fin n → Bool) → ℝ),
  (∀ (x : Fin n → Bool), F x = ∑ S, c S * NimAudit.RealFourier.chiF S x) →
    ∀ (S : Fin n → Bool), NimAudit.RealFourier.fhat F S = c S

Exact source text, lines 128–138

128/-- UNIQUENESS (Fin form). -/129theorem uniqueness_fin {n : ℕ} (F : (Fin n → Bool) → ℝ) (c : (Fin n → Bool) → ℝ)130    (h : ∀ x, F x = ∑ S, c S * chiF S x) : ∀ S, fhat F S = c S := by131  intro S132  rw [fhat_eq_coef]133  have hc := uniqueness (R := ℝ) n (lift F) (lift c) (fun x hx => by134    obtain ⟨v, rfl⟩ := toL_surj hx135    rw [lift_toL, h v, gs_eq_fintype_sum]136    apply Finset.sum_congr rfl; intro T _137    rw [lift_toL]; rfl) (toL S) (toL_mem S)138  rw [hc, lift_toL]

Project declarations in the statement: RealFourier.chiF, RealFourier.fhat

Project declarations used by the proof or definition body

Bridge.bitvecs, Fourier.chi, Fourier.coef, Fourier.uniqueness, Noise.gs, RealFourier.chiF, RealFourier.fhat, RealFourier.fhat_eq_coef, RealFourier.gs_eq_fintype_sum, RealFourier.lift, RealFourier.lift_toL, RealFourier.toL, RealFourier.toL_mem, RealFourier.toL_surj

theorem `RealFourier.parseval_fin`

Module RealFourier (lean/phase8/RealFourier.lean, lines 140–150) · file SHA-256 e0e69edd199d8650… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

PARSEVAL (Fin form).

Statement as elaborated and printed by Lean 4.26.0

∀ {n : ℕ} (F G : (Fin n → Bool) → ℝ),
  (2 ^ n)⁻¹ * ∑ x, F x * G x = ∑ S, NimAudit.RealFourier.fhat F S * NimAudit.RealFourier.fhat G S

Exact source text, lines 140–150

140/-- PARSEVAL (Fin form). -/141theorem parseval_fin {n : ℕ} (F G : (Fin n → Bool) → ℝ) :142    (2 ^ n)⁻¹ * ∑ x, F x * G x = ∑ S, fhat F S * fhat G S := by143  have h := parseval (R := ℝ) n (lift F) (lift G)144  unfold ip at h145  rw [gs_eq_fintype_sum, gs_eq_fintype_sum, mul_comm] at h146  have e1 : ∑ x, F x * G x = ∑ x : Fin n → Bool, lift F (toL x) * lift G (toL x) := by147    apply Finset.sum_congr rfl; intro v _; rw [lift_toL, lift_toL]148  rw [e1, h]149  apply Finset.sum_congr rfl; intro S _150  rw [fhat_eq_coef, fhat_eq_coef]

Project declarations in the statement: RealFourier.fhat

Project declarations used by the proof or definition body

Bridge.bitvecs, Fourier.coef, Fourier.ip, Fourier.parseval, Noise.gs, RealFourier.fhat, RealFourier.fhat_eq_coef, RealFourier.gs_eq_fintype_sum, RealFourier.lift, RealFourier.lift_toL, RealFourier.toL

Definitions these statements use

def `RealFourier.chiF`

Module RealFourier (lean/phase8/RealFourier.lean, lines 62–63) · file SHA-256 e0e69edd199d8650…

χ_S(x) for S, x : Fin n → Bool.

Statement as elaborated and printed by Lean 4.26.0

{n : ℕ} → (Fin n → Bool) → (Fin n → Bool) → ℝ

Exact source text, lines 62–63

62/-- χ_S(x) for S, x : Fin n → Bool. -/63noncomputable def chiF {n : ℕ} (S x : Fin n → Bool) : ℝ := chi (toL S) (toL x)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Fourier.chi, RealFourier.toL

def `RealFourier.fhat`

Module RealFourier (lean/phase8/RealFourier.lean, lines 87–89) · file SHA-256 e0e69edd199d8650…

Fourier coefficient on Fin n → Bool, with the uniform normalisation.

Statement as elaborated and printed by Lean 4.26.0

{n : ℕ} → ((Fin n → Bool) → ℝ) → (Fin n → Bool) → ℝ

Exact source text, lines 87–89

87/-- Fourier coefficient on Fin n → Bool, with the uniform normalisation. -/88noncomputable def fhat {n : ℕ} (F : (Fin n → Bool) → ℝ) (S : Fin n → Bool) : ℝ :=89  (2 ^ n)⁻¹ * ∑ x, F x * chiF S x

Project declarations in the statement: none

Project declarations used by the proof or definition body

RealFourier.chiF

Full modules

Module	File	Lines	Imports
RealFourier	`lean/phase8/RealFourier.lean`	275	`Mathlib.Data.Real.Archimedean`, `Mathlib.Data.Fintype.BigOperators`, `Mathlib.Algebra.BigOperators.Fin`, `Mathlib.Tactic.Linarith`, `Mathlib.Tactic.Positivity`, `Mathlib.Tactic.FieldSimp`, `Mathlib.Tactic.NormNum`, `Mathlib.Tactic.Ring`, Fourier, RealNoise

Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).

Section 6.4, paragraph 1Walsh–Hadamard characters are orthonormal; every f equals its Fourier expansion

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem RealFourier.chiF_formula

theorem RealFourier.orthonormal_fin

theorem RealFourier.inversion_fin

theorem RealFourier.uniqueness_fin

theorem RealFourier.parseval_fin

Definitions these statements use

def RealFourier.chiF

def RealFourier.fhat

Full modules

theorem `RealFourier.chiF_formula`

theorem `RealFourier.orthonormal_fin`

theorem `RealFourier.inversion_fin`

theorem `RealFourier.uniqueness_fin`

theorem `RealFourier.parseval_fin`

def `RealFourier.chiF`

def `RealFourier.fhat`