B-3: Finite trigonometric polynomials and positivity.

We model a finite trigonometric polynomial via complex exponentials with integer frequencies k ∈ [-N, N], scaled by log a. The evaluation is complex-valued; when used as a kernel for the quadratic form, we take the real part.

structure Frourio.TrigPoly (a : ℝ) : Type

• N : ℕ
• c : ℤ → ℂ

noncomputable def Frourio.TrigPoly.eval {a : ℝ} (F : TrigPoly a) (τ : ℝ) : ℂ

Equations

• F.eval τ = ∑ k ∈ Finset.Icc (-↑F.N) ↑F.N, F.c k * Complex.exp (Complex.I * (↑k * ↑(Real.log a) * ↑τ))

noncomputable def Frourio.TrigPoly.kernelR {a : ℝ} (F : TrigPoly a) : ℝ → ℝ

Real-valued kernel obtained as the real part of the complex trigonometric polynomial.

Equations

• F.kernelR τ = (F.eval τ).re

theorem Frourio.TrigPoly.Q_pos_of_ae_nonneg {a : ℝ} (F : TrigPoly a) (h : ∀ᵐ (τ : ℝ), 0 ≤ F.kernelR τ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : 0 ≤ Qℝ F.kernelR g

Positivity wrapper: if the real part is a.e. nonnegative, then the quadratic form built from it is nonnegative.

B-4: Finite lattice residue identity (design-level statement).

We introduce the exponential modes and state a finite-dimensional identity as a Prop to be proven in later phases when we put the problem on an appropriate compact domain or introduce weight/cutoffs that make the modes belong to L².

noncomputable def Frourio.LatticeResidue.eK (_a : ℝ) (_k : ℤ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Exponential mode e_k(τ) = exp(i k (log a) τ) as a design placeholder in L². In later phases this will be replaced by a genuine Lp element on a periodic domain or with suitable weights.

Equations

• Frourio.LatticeResidue.eK _a _k = 0

def Frourio.LatticeResidue.symmIdx (N : ℕ) : Finset ℤ

Symmetric integer index set {-N, …, N}.

Equations

• Frourio.LatticeResidue.symmIdx N = Finset.Icc (-↑N) ↑N

def Frourio.LatticeResidue.lattice_residue_finite {a : ℝ} (F : TrigPoly a) : Prop

Finite lattice residue identity (signature). For a trigonometric polynomial F with coefficients c_k on the symmetric index set, the quadratic form with kernel Re (eval F) equals a finite sum of modal energies weighted by Re c_k. The right-hand side uses placeholder eK a k modes in L².

This is a design-level Prop to be established in later phases.

Equations

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

structure Frourio.LatticeResidue.LatticeResidueHypotheses {a : ℝ} (F : TrigPoly a) : Prop

Phase 4.2: hypotheses wrapper providing the finite lattice residue identity. Concrete analytic proofs (orthogonality/Parseval on a periodic domain) will populate this wrapper in a later phase.

• holds : lattice_residue_finite F

theorem Frourio.LatticeResidue.lattice_residue_finite_proof {a : ℝ} (F : TrigPoly a) (h : LatticeResidueHypotheses F) : lattice_residue_finite F

Phase 4.2: from the hypotheses wrapper, conclude the identity.

Toeplitz form for finite trigonometric polynomials (finite-dimensional model).

We construct the Toeplitz matrix associated to coefficients c_k of a trigonometric polynomial on the symmetric index set {-N,…,N}. The entry at (i,j) is c_{k_j - k_i} where k_t = t - N encodes Fin (2N+1) into ℤ. We also provide a positivity predicate stating the associated quadratic form has nonnegative real part on all vectors.

def Frourio.Toeplitz.idxToZ (N : ℕ) (i : Fin (2 * N + 1)) : ℤ

Encode i : Fin (2N+1) as an integer in {-N,…,N}.

Equations

• Frourio.Toeplitz.idxToZ N i = ↑↑i - ↑N

noncomputable def Frourio.Toeplitz.matrix {a : ℝ} (F : TrigPoly a) : Matrix (Fin (2 * F.N + 1)) (Fin (2 * F.N + 1)) ℂ

Toeplitz matrix from a trigonometric polynomial's coefficients on {-N,…,N}.

Equations

• Frourio.Toeplitz.matrix F i j = F.c (Frourio.Toeplitz.idxToZ F.N j - Frourio.Toeplitz.idxToZ F.N i)

noncomputable def Frourio.Toeplitz.qform {a : ℝ} (F : TrigPoly a) (v : Fin (2 * F.N + 1) → ℂ) : ℝ

Quadratic form associated to the Toeplitz matrix (real part).

Equations

• Frourio.Toeplitz.qform F v = (∑ i : Fin (2 * F.N + 1), ∑ j : Fin (2 * F.N + 1), v i * star (v j) * Frourio.Toeplitz.matrix F i j).re

def Frourio.Toeplitz.isPSD {a : ℝ} (F : TrigPoly a) : Prop

Positivity predicate: the Toeplitz quadratic form has nonnegative real part.

Equations

• Frourio.Toeplitz.isPSD F = ∀ (v : Fin (2 * F.N + 1) → ℂ), 0 ≤ Frourio.Toeplitz.qform F v

Finite model equivalence: nonnegativity ↔ Toeplitz PSD.

In this finite-dimensional scaffold, we take the definition of “F is nonnegative” to be exactly the PSD property of its Toeplitz form. The following theorem is therefore definitionally true and serves as the bridge named in the plan; a stronger analytic statement relating the pointwise kernel kernelR F ≥ 0 to PSD will be introduced later.

def Frourio.TrigPoly.nonneg {a : ℝ} (F : TrigPoly a) : Prop

Finite-model nonnegativity predicate (alias to Toeplitz PSD).

Equations

• F.nonneg = Frourio.Toeplitz.isPSD F

theorem Frourio.TrigPoly.F_nonneg_iff_toeplitz_psd {a : ℝ} (F : TrigPoly a) : F.nonneg ↔ Toeplitz.isPSD F

In the finite model, “F is nonnegative” iff its Toeplitz form is PSD.