RealFourier

Comment and keyword shading is a reading aid only. It is not a verification marker; the evidence is the build record on the Build page.

1import Mathlib.Data.Real.Archimedean2import Mathlib.Data.Fintype.BigOperators3import Mathlib.Algebra.BigOperators.Fin4import Mathlib.Tactic.Linarith5import Mathlib.Tactic.Positivity6import Mathlib.Tactic.FieldSimp7import Mathlib.Tactic.NormNum8import Mathlib.Tactic.Ring9import Fourier10import RealNoise1112/- Phase 8, part B at ℝ: the Fourier results of Fourier.lean instantiated at Mathlib's real13   numbers, with an explicit equivalence between the list cube `bitvecs n` and Mathlib's14   finite type Fin n → Bool (cube points and character indices), and the transfer of15   finite sums to Mathlib's ∑.  Written by Claude (10 October 2026).  Lean 4.26.0 with16   Mathlib v4.26.0 (commit 2df2f01).1718   In the Fin form: x, S : Fin n → Bool, χ_S(x) = (−1)^{Σ_i [S_i ∧ x_i]},19   f̂(S) = 2^{−n} Σ_x f(x) χ_S(x), f(x) = Σ_S f̂(S) χ_S(x) for EVERY f, orthonormality,20   uniqueness, Parseval, tails and the parity spectrum.  B2/B3 for Nim are restated at ℝ in21   the list form used by the earlier modules (the cube there is bitvecs (B·N) resp.22   bitvecs (2·B·N)). -/2324namespace NimAudit25namespace RealFourier2627open Fourier Noise28open Bridge (bitvecs mem_bitvecs_length mem_bitvecs_of_length ones maskU)2930attribute [local instance] Lean.Grind.Semiring.natCast3132/-! ## The equivalence between bitvecs n and Fin n → Bool -/3334/-- Cube point / mask as a list. -/35def toL {n : ℕ} (v : Fin n → Bool) : List Bool := List.ofFn v3637theorem toL_mem {n : ℕ} (v : Fin n → Bool) : toL v ∈ bitvecs n := mem_bitvecs_of_length (by simp [toL])3839theorem toL_injective (n : ℕ) : Function.Injective (@toL n) := fun _ _ h => List.ofFn_injective h4041/-- Every list of length n is toL of a function (surjectivity onto the cube). -/42theorem toL_surj {n : ℕ} {x : List Bool} (hx : x ∈ bitvecs n) : ∃ v : Fin n → Bool, toL v = x := by43  have hl := mem_bitvecs_length hx44  subst hl45  exact ⟨fun i => x[i.1], List.ofFn_getElem x⟩4647/-- The cube as a Finset is the image of Fin n → Bool. -/48theorem image_toL (n : ℕ) : Finset.univ.image (@toL n) = (bitvecs n).toFinset := by49  ext x50  simp only [Finset.mem_image, Finset.mem_univ, true_and, List.mem_toFinset]51  constructor52  · rintro ⟨v, rfl⟩; exact toL_mem v53  · exact toL_surj5455/-- SUM TRANSFER: Σ over the list cube = Mathlib's Σ over Fin n → Bool. -/56theorem gs_eq_fintype_sum (n : ℕ) (g : List Bool → ℝ) : gs (bitvecs n) g = ∑ v : Fin n → Bool, g (toL v) := by57  rw [RealNoise.gs_real, ← List.sum_toFinset _ (cube_nodup n), ← image_toL,58    Finset.sum_image (fun a _ b _ h => toL_injective n h)]5960/-! ## Fin-form Fourier analysis over ℝ -/6162/-- χ_S(x) for S, x : Fin n → Bool. -/63noncomputable def chiF {n : ℕ} (S x : Fin n → Bool) : ℝ := chi (toL S) (toL x)6465/-- Number of coordinates selected by S at which x is 1. -/66theorem selCount_toL : ∀ {n : ℕ} (S x : Fin n → Bool),67    selCount (toL S) (toL x) = ∑ i, if S i && x i then 1 else 068  | 0, S, x => by simp [toL, selCount]69  | n + 1, S, x => by70    simp only [toL, List.ofFn_succ, selCount]71    rw [Fin.sum_univ_succ]72    congr 173    exact selCount_toL (fun i => S i.succ) (fun i => x i.succ)7475/-- 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]7879/-- |S| = number of i with S i. -/80theorem ones_toL : ∀ {n : ℕ} (S : Fin n → Bool), ones (toL S) = ∑ i, if S i then 1 else 081  | 0, S => by simp [toL, ones]82  | n + 1, S => by83    rw [Fin.sum_univ_succ, ← ones_toL (fun i => S i.succ)]84    simp only [toL, List.ofFn_succ, ones, List.filter_cons]85    cases S 0 <;> simp <;> omega8687/-- 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 x9091/-- 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 09495theorem lift_toL {n : ℕ} (F : (Fin n → Bool) → ℝ) (v : Fin n → Bool) : lift F (toL v) = F v := by96  unfold lift toL97  rw [dif_pos (by simp)]98  congr 1; funext i; simp99100theorem fhat_eq_coef {n : ℕ} (F : (Fin n → Bool) → ℝ) (S : Fin n → Bool) : fhat F S = coef n (lift F) (toL S) := by101  unfold fhat coef ip102  rw [gs_eq_fintype_sum, mul_comm]103  congr 1104  apply Finset.sum_congr rfl; intro v _105  rw [lift_toL]; rfl106107/-- 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]; rfl115116/-- 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]; rfl127128/-- 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]139140/-- 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]151152/-- n = 0: one point, one character, f̂(S) = f(x) for the unique S and x. -/153theorem dim_zero_fin (F : (Fin 0 → Bool) → ℝ) (x S : Fin 0 → Bool) : F x = fhat F S * chiF S x := by154  rw [inversion_fin F x, Fintype.sum_unique]155  congr 1 <;> congr 1 <;> exact Subsingleton.elim _ _156157/-- 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 0160161theorem 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]166167/-- PARITY IS A PURE CHARACTER (Fin form): f̂_{χ_S}(T) = [T = S], and its tail is 1 below168    |S| and 0 from |S| on. -/169theorem parity_fin {n : ℕ} (S : Fin n → Bool) :170    (∀ T, fhat (chiF S) T = if T = S then 1 else 0) ∧171    ∀ k, tailF (chiF S) k = if k < ∑ i, (if S i then 1 else 0) then 1 else 0 := by172  have hc : ∀ x ∈ bitvecs n, lift (chiF S) x = chi (R := ℝ) (toL S) x := by173    intro x hx; obtain ⟨v, rfl⟩ := toL_surj hx; rw [lift_toL]; rfl174  refine ⟨fun T => ?_, fun k => ?_⟩175  · rw [fhat_eq_coef, coef_congr hc, coef_chi (toL_mem S) (toL_mem T)]176    by_cases h : T = S177    · simp [h]178    · rw [if_neg h, if_neg (fun e => h (toL_injective n e))]179  · rw [tailF_eq, tail_congr hc, tail_chi (toL_mem S), ones_toL]180181/-! ## B2 and B3 at ℝ (list form, as in the Nim modules) -/182183theorem nimBit_spectrum_real {B N j : ℕ} (hj : j < B) :184    (∀ T ∈ bitvecs (B * N), coef (B * N) (nimBitSign (R := ℝ) B N j) T = if T = maskU B N (2 ^ j) then 1 else 0) ∧185    ones (maskU B N (2 ^ j)) = N ∧ ExactDeg (B * N) (nimBitSign (R := ℝ) B N j) N ∧186    ∀ k, tail (B * N) (nimBitSign (R := ℝ) B N j) k = if k < N then 1 else 0 :=187  nimBit_spectrum hj188189theorem delta_spectrum_real {B j : ℕ} (hj : j < B) :190    (∀ w ∈ bitvecs (B * 2), (deltaSign B j w : ℝ) = chi (maskU B 2 (2 ^ j)) w) ∧191    ones (maskU B 2 (2 ^ j)) = 2 ∧ ExactDeg (B * 2) (deltaSign (R := ℝ) B j) 2 :=192  delta_spectrum hj193194theorem bandLimited_corr_real {n : ℕ} {f : List Bool → ℝ} {k : ℕ} {ε : ℝ} (hb : BandLimited n f k ε)195    {S : List Bool} (hS : S ∈ bitvecs n) (hk : k < ones S) : ip n f (chi S) ^ 2 ≤ ε :=196  bandLimited_corr hb hS hk197198theorem dC_not_character_real {B N q : ℕ} (hN : 2 ≤ N) (hq : q < B) :199    ¬ ∃ (S : List Bool) (c : ℝ), c * c = 1 ∧ ∀ z ∈ bitvecs (2 * (B * N)), dSign B N q z = c * chi S z :=200  dC_not_character hN hq201202theorem dC_two_coefs_real {B N q : ℕ} (hN : 2 ≤ N) (hq : q < B) :203    ∃ S ∈ bitvecs (2 * (B * N)), ∃ T ∈ bitvecs (2 * (B * N)), S ≠ T ∧204      coef (2 * (B * N)) (dSign (R := ℝ) B N q) S ≠ 0 ∧ coef (2 * (B * N)) (dSign (R := ℝ) B N q) T ≠ 0 :=205  dC_two_coefs hN hq206207theorem dSign_enc_real {B N q : ℕ} {Q Q' : List ℕ} (hQ : Q.length = N) (hQ' : Q'.length = N)208    (hw : Game.Width B Q) (hw' : Game.Width B Q') (h1 : LocalRestore.OneChange Q Q') :209    (dSign B N q (enc B N Q Q') : ℝ) = sg ((nimSum Q ^^^ nimSum Q').testBit q) :=210  dSign_enc hQ hQ' hw hw' h1211212theorem dSign_known_heap_real {B N q i : ℕ} (hq : q < B) (hi : i < N) {Q : List ℕ} (hQ : Q.length = N) (y : ℕ) :213    (dSign B N q (enc B N Q (Q.set i y)) : ℝ) =214      chi (twoMask (2 * (B * N)) (B * i + (B - 1 - q)) (B * N + (B * i + (B - 1 - q)))) (enc B N Q (Q.set i y)) :=215  dSign_known_heap hq hi hQ y216217theorem dC_one_exactDeg_real {B q : ℕ} (hq : q < B) : ExactDeg (2 * (B * 1)) (dSign (R := ℝ) B 1 q) 2 :=218  dC_one_exactDeg hq219220theorem gMask_delta_real {B N q : ℕ} (hq : q < B) {Q Q' : List ℕ} (hQ : Q.length = N) (hQ' : Q'.length = N)221    (hw : Game.Width B Q) (hw' : Game.Width B Q') :222    (chi (gMask B N q) (enc B N Q Q') : ℝ) = sg ((nimSum Q ^^^ nimSum Q').testBit q) :=223  gMask_delta hq hQ hQ' hw hw'224225theorem char_unique_real {B N q : ℕ} (hq : q < B) {S : List Bool} (hS : S ∈ bitvecs (2 * (B * N)))226    (h : ∀ Q Q', Q.length = N → Q'.length = N → Game.Width B Q → Game.Width B Q' → LocalRestore.OneChange Q Q' →227      (chi S (enc B N Q Q') : ℝ) = sg ((nimSum Q ^^^ nimSum Q').testBit q)) :228    S = gMask B N q :=229  char_unique hq hS h230231theorem char_unique_signed_real {B N q : ℕ} (hq : q < B) {S : List Bool} (hS : S ∈ bitvecs (2 * (B * N)))232    {c : ℝ} (h : ∀ Q Q', Q.length = N → Q'.length = N → Game.Width B Q → Game.Width B Q' → LocalRestore.OneChange Q Q' →233      c * chi S (enc B N Q Q') = sg ((nimSum Q ^^^ nimSum Q').testBit q)) :234    c = 1 ∧ S = gMask B N q :=235  char_unique_signed hq hS h236237theorem no_low_degree_extension_real {B N q : ℕ} (hq : q < B) {S : List Bool} (hS : S ∈ bitvecs (2 * (B * N)))238    (hdeg : ones S < 2 * N)239    (h : ∀ Q Q', Q.length = N → Q'.length = N → Game.Width B Q → Game.Width B Q' → LocalRestore.OneChange Q Q' →240      (chi S (enc B N Q Q') : ℝ) = sg ((nimSum Q ^^^ nimSum Q').testBit q)) : False :=241  no_low_degree_extension hq hS hdeg h242243/-! ## Axiom checks -/244#print axioms toL_mem245#print axioms toL_injective246#print axioms toL_surj247#print axioms image_toL248#print axioms gs_eq_fintype_sum249#print axioms selCount_toL250#print axioms chiF_formula251#print axioms ones_toL252#print axioms lift_toL253#print axioms fhat_eq_coef254#print axioms inversion_fin255#print axioms orthonormal_fin256#print axioms uniqueness_fin257#print axioms parseval_fin258#print axioms dim_zero_fin259#print axioms tailF_eq260#print axioms parity_fin261#print axioms nimBit_spectrum_real262#print axioms delta_spectrum_real263#print axioms bandLimited_corr_real264#print axioms dC_not_character_real265#print axioms dC_two_coefs_real266#print axioms dSign_enc_real267#print axioms dSign_known_heap_real268#print axioms dC_one_exactDeg_real269#print axioms gMask_delta_real270#print axioms char_unique_real271#print axioms char_unique_signed_real272#print axioms no_low_degree_extension_real273274end RealFourier275end NimAudit