Fourier bookkeeping on the four-dimensional torus

This file fixes the normalization conventions on the formal torus carrier. It provides character algebra, orthogonality for both the probability Haar measure and the paper's Lebesgue-normalized measure, the coefficient convention used in paper equation (3.23), and the complete product-torus L² Fourier/Plancherel interface.

Character algebra

@[simp]

theorem Anderson4D.charT4_add (k l : Z4) (x : T4) : charT4 (k + l) x = charT4 k x * charT4 l x

@[simp]

theorem Anderson4D.charT4_neg (k : Z4) (x : T4) : charT4 (-k) x = (starRingEnd ℂ) (charT4 k x)

@[simp]

theorem Anderson4D.conj_charT4 (k : Z4) (x : T4) : (starRingEnd ℂ) (charT4 k x) = charT4 (-k) x

@[simp]

theorem Anderson4D.conj_charT4_neg (k : Z4) (x : T4) : (starRingEnd ℂ) (charT4 (-k) x) = charT4 k x

theorem Anderson4D.norm_charT4 (k : Z4) (x : T4) : ‖charT4 k x‖ = 1

theorem Anderson4D.abs_charT4 (k : Z4) (x : T4) : ‖charT4 k x‖₊ = 1

theorem Anderson4D.continuous_charT4 (k : Z4) : Continuous (charT4 k)

theorem Anderson4D.integrable_charT4_mul_conj (k l : Z4) : MeasureTheory.Integrable (fun (x : T4) => charT4 k x * (starRingEnd ℂ) (charT4 l x)) haarT4

Orthogonality

theorem Anderson4D.integral_fourier (k : ℤ) : ∫ (x : AddCircle (2 * Real.pi)), (fourier k) x ∂AddCircle.haarAddCircle = if k = 0 then 1 else 0

The mean of a one-dimensional Fourier character under probability Haar measure.

theorem Anderson4D.fourier_orthogonality (n m : ℤ) : ∫ (x : AddCircle (2 * Real.pi)), (fourier n) x * (starRingEnd ℂ) ((fourier m) x) ∂AddCircle.haarAddCircle = if n = m then 1 else 0

One-dimensional Fourier orthogonality under probability Haar measure.

theorem Anderson4D.charT4_orthogonality (k l : Z4) : ∫ (x : T4), charT4 k x * (starRingEnd ℂ) (charT4 l x) ∂haarT4 = if k = l then 1 else 0

Product-character orthogonality under the probability Haar measure.

theorem Anderson4D.charT4_orthogonality_paper (k l : Z4) : ∫ (x : T4), charT4 k x * (starRingEnd ℂ) (charT4 l x) ∂paperMeasure = if k = l then ↑((2 * Real.pi) ^ dim) else 0

Product-character orthogonality under the paper's measure. This is the explicit (2π)⁴ normalization ledger entry.

Coefficient conventions

noncomputable def Anderson4D.torusFourierCoeff (f : T4 → ℂ) (k : Z4) : ℂ

Standard probability-Haar Fourier coefficient. The conjugated character gives the usual negative-exponential convention.

Equations

• Anderson4D.torusFourierCoeff f k = ∫ (x : Anderson4D.T4), (starRingEnd ℂ) (Anderson4D.charT4 k x) * f x ∂Anderson4D.haarT4

noncomputable def Anderson4D.paperFourierCoeff (f : T4 → ℂ) (k : Z4) : ℂ

The paper's one-variable positive-exponential coefficient, without a normalizing (2π)⁻⁴ factor.

Equations

• Anderson4D.paperFourierCoeff f k = ∫ (x : Anderson4D.T4), Anderson4D.charT4 k x * f x ∂Anderson4D.paperMeasure

noncomputable def Anderson4D.paperKernelCoeff (K : T4 → T4 → ℂ) (α β : Z4) : ℂ

Paper equation (3.23), for an arbitrary complex kernel.

Equations

• Anderson4D.paperKernelCoeff K α β = ∫ (x : Anderson4D.T4), ∫ (y : Anderson4D.T4), Anderson4D.charT4 α x * Anderson4D.charT4 β y * K x y ∂Anderson4D.paperMeasure ∂Anderson4D.paperMeasure

noncomputable def Anderson4D.normalizedKernelCoeff (K : T4 → T4 → ℂ) (α β : Z4) : ℂ

Probability-Haar counterpart of paperKernelCoeff, useful for normalization arguments.

Equations

• Anderson4D.normalizedKernelCoeff K α β = ∫ (x : Anderson4D.T4), ∫ (y : Anderson4D.T4), Anderson4D.charT4 α x * Anderson4D.charT4 β y * K x y ∂Anderson4D.haarT4 ∂Anderson4D.haarT4

theorem Anderson4D.torusFourierCoeff_char (k l : Z4) : torusFourierCoeff (charT4 l) k = if k = l then 1 else 0

Fourier coefficients of the character basis at probability-Haar normalization.

theorem Anderson4D.paperFourierCoeff_char (k l : Z4) : paperFourierCoeff (charT4 l) k = if l = -k then ↑((2 * Real.pi) ^ dim) else 0

Under the paper's positive-exponential convention, the coefficient of e_l is supported at frequency -l and has mass (2π)⁴.

theorem Anderson4D.paperFourierCoeff_eq_volume_mul_torusFourierCoeff_neg (f : T4 → ℂ) (k : Z4) : paperFourierCoeff f k = ↑((2 * Real.pi) ^ dim) * torusFourierCoeff f (-k)

Complete one-variable normalization/sign dictionary: the paper's unnormalized positive-exponential coefficient is (2π)⁴ times the probability-Haar coefficient at the opposite frequency.

Finite Fourier polynomials

noncomputable def Anderson4D.torusTrigPoly (s : Finset Z4) (a : Z4 → ℂ) (x : T4) : ℂ

A finite Fourier polynomial on 𝕋⁴.

Equations

• Anderson4D.torusTrigPoly s a x = ∑ k ∈ s, a k * Anderson4D.charT4 k x

theorem Anderson4D.torusFourierCoeff_trigPoly (s : Finset Z4) (a : Z4 → ℂ) (k : Z4) : torusFourierCoeff (torusTrigPoly s a) k = if k ∈ s then a k else 0

Fourier coefficient extraction for a finite trigonometric polynomial.

theorem Anderson4D.torusTrigPoly_parseval (s : Finset Z4) (a : Z4 → ℂ) : ∫ (x : T4), torusTrigPoly s a x * (starRingEnd ℂ) (torusTrigPoly s a x) ∂haarT4 = ∑ k ∈ s, a k * (starRingEnd ℂ) (a k)

Finite-dimensional Parseval identity. This is the algebraic core of the product-torus Plancherel interface and already suffices for every finite Fourier truncation.

Product-torus L² Fourier theory

noncomputable def Anderson4D.charT4Continuous (k : Z4) : C(T4, ℂ)

A Fourier character regarded as a continuous function.

Equations

• Anderson4D.charT4Continuous k = { toFun := Anderson4D.charT4 k, continuous_toFun := ⋯ }

@[simp]

theorem Anderson4D.charT4Continuous_apply (k : Z4) (x : T4) : (charT4Continuous k) x = charT4 k x

@[simp]

theorem Anderson4D.charT4Continuous_zero : charT4Continuous 0 = 1

@[simp]

theorem Anderson4D.charT4Continuous_add (k l : Z4) : charT4Continuous (k + l) = charT4Continuous k * charT4Continuous l

@[simp]

theorem Anderson4D.star_charT4Continuous (k : Z4) : star (charT4Continuous k) = charT4Continuous (-k)

noncomputable def Anderson4D.torusFourierSubalgebra : StarSubalgebra ℂ C(T4, ℂ)

The star subalgebra generated by the Fourier characters.

Equations

• Anderson4D.torusFourierSubalgebra = { toSubalgebra := Algebra.adjoin ℂ (Set.range Anderson4D.charT4Continuous), star_mem' := @Anderson4D.torusFourierSubalgebra._proof_8 }

theorem Anderson4D.torusFourierSubalgebra_coe : Subalgebra.toSubmodule torusFourierSubalgebra.toSubalgebra = Submodule.span ℂ (Set.range charT4Continuous)

The algebra generated by the Fourier characters is already their complex linear span.

theorem Anderson4D.charT4Continuous_single (x : T4) (i : Fin dim) : (charT4Continuous (Pi.single i 1)) x = (fourier 1) (x i)

A character supported in a single coordinate reads that coordinate through the standard circle embedding.

theorem Anderson4D.torusFourierSubalgebra_separatesPoints : torusFourierSubalgebra.SeparatesPoints

Fourier characters separate points of T4.

theorem Anderson4D.torusFourierSubalgebra_closure_eq_top : torusFourierSubalgebra.topologicalClosure = ⊤

The character-generated star subalgebra is uniformly dense in the continuous functions on T4.

theorem Anderson4D.span_charT4Continuous_closure_eq_top : (Submodule.span ℂ (Set.range charT4Continuous)).topologicalClosure = ⊤

The complex linear span of the Fourier characters is uniformly dense in the continuous functions on T4.

@[reducible, inline]

noncomputable abbrev Anderson4D.charT4Lp (p : ENNReal) [Fact (1 ≤ p)] (k : Z4) : ↥(MeasureTheory.Lp ℂ p haarT4)

A Fourier character as an element of Lᵖ(T4, haarT4).

Equations

• Anderson4D.charT4Lp p k = (ContinuousMap.toLp p Anderson4D.haarT4 ℂ) (Anderson4D.charT4Continuous k)

theorem Anderson4D.coeFn_charT4Lp (p : ENNReal) [Fact (1 ≤ p)] (k : Z4) : ↑↑(charT4Lp p k) =ᵐ[haarT4] charT4 k

The Lᵖ representative of a character agrees almost everywhere with the pointwise character.

theorem Anderson4D.span_charT4Lp_closure_eq_top {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) : (Submodule.span ℂ (Set.range (charT4Lp p))).topologicalClosure = ⊤

For finite p, the Fourier characters have dense span in Lᵖ(T4, haarT4).

theorem Anderson4D.orthonormal_charT4 : Orthonormal ℂ (charT4Lp 2)

The Fourier characters form an orthonormal family in L²(T4, haarT4).

noncomputable def Anderson4D.torusFourierBasis : HilbertBasis Z4 ℂ ↥(MeasureTheory.Lp ℂ 2 haarT4)

The product Fourier characters as a Hilbert basis of L²(T4, haarT4).

Equations

• Anderson4D.torusFourierBasis = HilbertBasis.mk Anderson4D.orthonormal_charT4 Anderson4D.torusFourierBasis._proof_5

@[simp]

theorem Anderson4D.coe_torusFourierBasis : ⇑torusFourierBasis = charT4Lp 2

theorem Anderson4D.torusFourierBasis_repr (f : ↥(MeasureTheory.Lp ℂ 2 haarT4)) (k : Z4) : ↑(torusFourierBasis.repr f) k = torusFourierCoeff (↑↑f) k

The abstract Hilbert-basis coordinate is the integral Fourier coefficient fixed above.

theorem Anderson4D.norm_torusFourierCoeff_le (f : ↥(MeasureTheory.Lp ℂ 2 haarT4)) (k : Z4) : ‖torusFourierCoeff (↑↑f) k‖ ≤ ‖f‖

Each Fourier coefficient is bounded by the L² norm.

theorem Anderson4D.hasSum_torusFourier_series_L2 (f : ↥(MeasureTheory.Lp ℂ 2 haarT4)) : HasSum (fun (k : Z4) => torusFourierCoeff (↑↑f) k • charT4Lp 2 k) f

Every L² function is the L² sum of its product-torus Fourier series. This HasSum statement, rather than a raw tsum, records the required convergence.

theorem Anderson4D.hasSum_conj_mul_torusFourierCoeff (f g : ↥(MeasureTheory.Lp ℂ 2 haarT4)) : HasSum (fun (k : Z4) => (starRingEnd ℂ) (torusFourierCoeff (↑↑f) k) * torusFourierCoeff (↑↑g) k) (∫ (x : T4), (starRingEnd ℂ) (↑↑f x) * ↑↑g x ∂haarT4)

Parseval's identity for inner products on the product torus.

theorem Anderson4D.hasSum_sq_torusFourierCoeff (f : ↥(MeasureTheory.Lp ℂ 2 haarT4)) : HasSum (fun (k : Z4) => ‖torusFourierCoeff (↑↑f) k‖ ^ 2) (∫ (x : T4), ‖↑↑f x‖ ^ 2 ∂haarT4)

Parseval's identity for squared norms on the product torus.

theorem Anderson4D.tsum_sq_torusFourierCoeff (f : ↥(MeasureTheory.Lp ℂ 2 haarT4)) : ∑' (k : Z4), ‖torusFourierCoeff (↑↑f) k‖ ^ 2 = ∫ (x : T4), ‖↑↑f x‖ ^ 2 ∂haarT4

tsum form of Plancherel, derived from the convergent HasSum statement.

theorem Anderson4D.torusFourierCoeff_l2_ext {f g : ↥(MeasureTheory.Lp ℂ 2 haarT4)} (h : ∀ (k : Z4), torusFourierCoeff (↑↑f) k = torusFourierCoeff (↑↑g) k) : f = g

Fourier coefficients determine an L² function.

theorem Anderson4D.torusFourierCoeff_toLp (f : T4 → ℂ) (hf : MeasureTheory.MemLp f 2 haarT4) (k : Z4) : torusFourierCoeff (↑↑(MeasureTheory.MemLp.toLp f hf)) k = torusFourierCoeff f k

Passing an L² function to the quotient does not change its Fourier coefficients.

Bounded and finite multiplier interfaces

@[reducible, inline]

noncomputable abbrev Anderson4D.TorusL2Sequence : AddSubgroup (PreLp fun (x : Z4) => ℂ)

The ℓ²(Z4) coefficient space used by the Fourier basis.

Equations

• Anderson4D.TorusL2Sequence = lp (fun (x : Anderson4D.Z4) => ℂ) 2

noncomputable def Anderson4D.torusDiagonalCLM (symbol : Z4 → ℂ) (C : ℝ) (hC : 0 ≤ C) (hsymbol : ∀ (k : Z4), ‖symbol k‖ ≤ C) : ↥TorusL2Sequence →L[ℂ] ↥TorusL2Sequence

Coordinatewise multiplication by a uniformly bounded symbol on ℓ²(Z4).

Equations

• Anderson4D.torusDiagonalCLM symbol C hC hsymbol = lp.mapCLM 2 (fun (k : Anderson4D.Z4) => symbol k • ContinuousLinearMap.id ℂ ℂ) hC ⋯

@[simp]

theorem Anderson4D.torusDiagonalCLM_apply (symbol : Z4 → ℂ) (C : ℝ) (hC : 0 ≤ C) (hsymbol : ∀ (k : Z4), ‖symbol k‖ ≤ C) (a : ↥TorusL2Sequence) (k : Z4) : ↑((torusDiagonalCLM symbol C hC hsymbol) a) k = symbol k * ↑a k

theorem Anderson4D.torusDiagonalCLM_norm_le (symbol : Z4 → ℂ) (C : ℝ) (hC : 0 ≤ C) (hsymbol : ∀ (k : Z4), ‖symbol k‖ ≤ C) : ‖torusDiagonalCLM symbol C hC hsymbol‖ ≤ C

Operator-norm control for the diagonal action on coefficients.

noncomputable def Anderson4D.torusL2MultiplierCLM (symbol : Z4 → ℂ) (C : ℝ) (hC : 0 ≤ C) (hsymbol : ∀ (k : Z4), ‖symbol k‖ ≤ C) : ↥(MeasureTheory.Lp ℂ 2 haarT4) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 haarT4)

The bounded L² Fourier multiplier obtained by conjugating the coefficient-space diagonal map by the product-torus Fourier basis.

Equations

• Anderson4D.torusL2MultiplierCLM symbol C hC hsymbol = ↑↑Anderson4D.torusFourierBasis.repr.symm ∘SL Anderson4D.torusDiagonalCLM symbol C hC hsymbol ∘SL ↑↑Anderson4D.torusFourierBasis.repr

@[simp]

theorem Anderson4D.torusFourierCoeff_l2MultiplierCLM (symbol : Z4 → ℂ) (C : ℝ) (hC : 0 ≤ C) (hsymbol : ∀ (k : Z4), ‖symbol k‖ ≤ C) (f : ↥(MeasureTheory.Lp ℂ 2 haarT4)) (k : Z4) : torusFourierCoeff (↑↑((torusL2MultiplierCLM symbol C hC hsymbol) f)) k = symbol k * torusFourierCoeff (↑↑f) k

The bounded multiplier has exactly the prescribed Fourier coefficients.

theorem Anderson4D.torusL2MultiplierCLM_apply_norm_le (symbol : Z4 → ℂ) (C : ℝ) (hC : 0 ≤ C) (hsymbol : ∀ (k : Z4), ‖symbol k‖ ≤ C) (f : ↥(MeasureTheory.Lp ℂ 2 haarT4)) : ‖(torusL2MultiplierCLM symbol C hC hsymbol) f‖ ≤ C * ‖f‖

Pointwise norm bound for the bounded Fourier multiplier.

theorem Anderson4D.torusL2MultiplierCLM_norm_le (symbol : Z4 → ℂ) (C : ℝ) (hC : 0 ≤ C) (hsymbol : ∀ (k : Z4), ‖symbol k‖ ≤ C) : ‖torusL2MultiplierCLM symbol C hC hsymbol‖ ≤ C

Operator-norm bound for the bounded Fourier multiplier.

noncomputable def Anderson4D.torusFiniteSynthesis (s : Finset Z4) (a : Z4 → ℂ) : ↥(MeasureTheory.Lp ℂ 2 haarT4)

Synthesis of finitely many Fourier modes in L².

Equations

• Anderson4D.torusFiniteSynthesis s a = ∑ k ∈ s, a k • Anderson4D.charT4Lp 2 k

theorem Anderson4D.torusFourierCoeff_finiteSynthesis (s : Finset Z4) (a : Z4 → ℂ) (k : Z4) : torusFourierCoeff (↑↑(torusFiniteSynthesis s a)) k = if k ∈ s then a k else 0

Coefficient extraction for finite L² synthesis.

noncomputable def Anderson4D.torusFiniteMultiplier (symbol : Z4 → ℂ) (s : Finset Z4) (a : Z4 → ℂ) : ↥(MeasureTheory.Lp ℂ 2 haarT4)

Multiplication by a symbol on a finite set of Fourier modes.

Equations

• Anderson4D.torusFiniteMultiplier symbol s a = Anderson4D.torusFiniteSynthesis s fun (k : Anderson4D.Z4) => symbol k * a k

theorem Anderson4D.torusFourierCoeff_finiteMultiplier (symbol : Z4 → ℂ) (s : Finset Z4) (a : Z4 → ℂ) (k : Z4) : torusFourierCoeff (↑↑(torusFiniteMultiplier symbol s a)) k = if k ∈ s then symbol k * a k else 0

The defining coefficient formula for the finite Fourier multiplier.

def Anderson4D.IsTorusL2Multiplier (symbol : Z4 → ℂ) (f g : ↥(MeasureTheory.Lp ℂ 2 haarT4)) : Prop

A graph-style Fourier multiplier specification. It applies equally to bounded and unbounded symbols and therefore does not assert nonexistent global domains.

Equations

• Anderson4D.IsTorusL2Multiplier symbol f g = ∀ (k : Anderson4D.Z4), Anderson4D.torusFourierCoeff (↑↑g) k = symbol k * Anderson4D.torusFourierCoeff (↑↑f) k

theorem Anderson4D.isTorusL2Multiplier_l2MultiplierCLM (symbol : Z4 → ℂ) (C : ℝ) (hC : 0 ≤ C) (hsymbol : ∀ (k : Z4), ‖symbol k‖ ≤ C) (f : ↥(MeasureTheory.Lp ℂ 2 haarT4)) : IsTorusL2Multiplier symbol f ((torusL2MultiplierCLM symbol C hC hsymbol) f)

The constructed bounded multiplier satisfies the domain-independent multiplier specification.

theorem Anderson4D.IsTorusL2Multiplier.unique {symbol : Z4 → ℂ} {f g h : ↥(MeasureTheory.Lp ℂ 2 haarT4)} (hg : IsTorusL2Multiplier symbol f g) (hh : IsTorusL2Multiplier symbol f h) : g = h

A multiplier output, when it exists, is unique in L².

theorem Anderson4D.isTorusL2Multiplier_one (f : ↥(MeasureTheory.Lp ℂ 2 haarT4)) : IsTorusL2Multiplier (fun (x : Z4) => 1) f f

The identity symbol acts as the identity.

theorem Anderson4D.IsTorusL2Multiplier.comp {symbol₁ symbol₂ : Z4 → ℂ} {f g h : ↥(MeasureTheory.Lp ℂ 2 haarT4)} (h₁ : IsTorusL2Multiplier symbol₁ f g) (h₂ : IsTorusL2Multiplier symbol₂ g h) : IsTorusL2Multiplier (fun (k : Z4) => symbol₂ k * symbol₁ k) f h

Multiplier specifications compose by pointwise multiplication of their symbols.

theorem Anderson4D.isTorusL2Multiplier_finite (symbol : Z4 → ℂ) (s : Finset Z4) (a : Z4 → ℂ) : IsTorusL2Multiplier symbol (torusFiniteSynthesis s a) (torusFiniteMultiplier symbol s a)

Finite synthesis realizes the multiplier specification without any summability assumption.

theorem Anderson4D.paperKernelCoeff_eq_volume_sq_smul_normalized (K : T4 → T4 → ℂ) (α β : Z4) : paperKernelCoeff K α β = ((2 * Real.pi) ^ dim) ^ 2 • normalizedKernelCoeff K α β

General two-variable normalization ledger: each integration against the paper measure contributes one factor (2π)⁴.

theorem Anderson4D.normalizedKernelCoeff_eq_iterated_torusFourierCoeff (K : T4 → T4 → ℂ) (α β : Z4) : normalizedKernelCoeff K α β = torusFourierCoeff (fun (x : T4) => torusFourierCoeff (K x) (-β)) (-α)

Positive-exponential normalized kernel coefficients are iterated standard coefficients at the opposite frequencies.

theorem Anderson4D.normalizedKernelCoeff_rankOne (f g : T4 → ℂ) (α β : Z4) : normalizedKernelCoeff (fun (x y : T4) => f x * g y) α β = (∫ (x : T4), charT4 α x * f x ∂haarT4) * ∫ (y : T4), charT4 β y * g y ∂haarT4

A rank-one normalized kernel coefficient factors into two one-variable integrals. No Fubini theorem is needed.

theorem Anderson4D.paperKernelCoeff_rankOne (f g : T4 → ℂ) (α β : Z4) : paperKernelCoeff (fun (x y : T4) => f x * g y) α β = paperFourierCoeff f α * paperFourierCoeff g β

A rank-one paper-normalized kernel coefficient factors into the two unnormalized one-variable coefficients.

theorem Anderson4D.paperKernelCoeff_rankOne_eq_normalized (f g : T4 → ℂ) (α β : Z4) : paperKernelCoeff (fun (x y : T4) => f x * g y) α β = ((2 * Real.pi) ^ dim) ^ 2 • normalizedKernelCoeff (fun (x y : T4) => f x * g y) α β

The paper and normalized rank-one coefficients differ by two copies of the measure factor (2π)⁴.

Operator-sign ledger

noncomputable def Anderson4D.rankOneOperatorPairing (f g : T4 → ℂ) (α β : Z4) : ℂ

The rank-one operator pairing with e_{-α} in the conjugate-linear slot, written at probability-Haar normalization.

Equations

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

theorem Anderson4D.rankOneOperatorPairing_eq_normalizedKernelCoeff (f g : T4 → ℂ) (α β : Z4) : rankOneOperatorPairing f g α β = normalizedKernelCoeff (fun (x y : T4) => f x * g y) α β

Sign check for equation (3.23): e_{-α} in the operator's conjugate-linear slot produces the paper's positive e_α convention.