Definition 6.1The degree->k Fourier tail and (k,ε)-spectral band-limitation

The tail above degree $k$ is the total squared Fourier weight on sets larger than $k$. A function is $(k,\varepsilon)$-band-limited if that weight is at most $\varepsilon$: almost all of its "energy" is at low frequency. For a $\pm1$-valued function the total weight is $1$, so the tail is the fraction of energy above degree $k$.

Fourier.tail is $\mathrm{Tail}_{>k}(f)=\sum_{|S|>k}\hat f(S)^2$ and Fourier.BandLimited is "tail at most $\varepsilon$". RealFourier.tailF_eq connects the Mathlib-cube version RealFourier.tailF to the list-cube definition used elsewhere.

Principal declarations

∀ {n : ℕ} (F : (Fin n → Bool) → ℝ) (k : ℕ),
  NimAudit.RealFourier.tailF F k = NimAudit.Fourier.tail n (NimAudit.RealFourier.lift F) k

161theorem tailF_eq {n : ℕ} (F : (Fin n → Bool) → ℝ) (k : ℕ) : tailF F k = tail n (lift F) k := by162  unfold tailF tail163  rw [gs_eq_fintype_sum]164  apply Finset.sum_congr rfl; intro S _165  rw [ones_toL, fhat_eq_coef]

{R : Type} → [Grind.Field R] → ℕ → (List Bool → R) → ℕ → R

380/-- Degree-> k Fourier tail Tail_{>k}(f) = Σ_{|S| > k} f̂(S)². -/381def tail (n : Nat) (f : List Bool → R) (k : Nat) : R :=382  gs (bitvecs n) (fun S => if k < ones S then coef n f S ^ 2 else 0)

{R : Type} → [Grind.Field R] → [LE R] → ℕ → (List Bool → R) → ℕ → R → Prop

384/-- (k, ε)-spectrally band-limited. -/385def BandLimited (n : Nat) (f : List Bool → R) (k : Nat) (ε : R) : Prop := tail n f k ≤ ε

Definitions these statements use

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

157/-- Degree-> k tail (Fin form). -/158noncomputable def tailF {n : ℕ} (F : (Fin n → Bool) → ℝ) (k : ℕ) : ℝ :=159  ∑ S : Fin n → Bool, if k < ∑ i, (if S i then 1 else 0) then fhat F S ^ 2 else 0

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

91/-- Lift of a function on Fin n → Bool to lists (0 off the cube). -/92noncomputable def lift {n : ℕ} (F : (Fin n → Bool) → ℝ) (x : List Bool) : ℝ :=93  if h : x.length = n then F (fun i => x[i.1]'(by omega)) else 0

Full modules

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).