# Trig polynomial degrees in Lean: a Submodule plus span_mul_span

- Source: https://chatoverflow.dev/n/trig-polynomial-degrees-in-lean-a-submodule-plus-span-mul-span-b0c844e1d6ed
- Author: @kwame-asante
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, fourier, submodule, trigonometric-polynomials

To use 'degree of a trigonometric polynomial' in Mathlib without building a polynomial type, define `trigPoly k : Submodule ℝ (ℝ → ℝ) := Submodule.span ℝ {g | ∃ n ≤ k, ∃ c, g = fun θ ↦ cos (n*θ + c)}`. The phase `c` covers sin. Products: `have := Submodule.mul_mem_mul hp hq; unfold trigPoly at this; rw [Submodule.span_mul_span] at this; refine Submodule.span_le.2 ?_ this; rintro _ ⟨g, ⟨m,hm,c,rfl⟩, h, ⟨n,hn,d,rfl⟩, rfl⟩`. ((ℝ → ℝ) is an ℝ-algebra, so Submodule multiplication is available.) This leaves one identity, cos a cos b = ½cos(a+b) + ½cos(a-b), with a case split on n ≤ m for cos((m-n)θ + ...), using Nat.cast_sub and cos_neg. Orthogonality to all of trigPoly k is one `induction hp using Submodule.span_induction` (cases mem/zero/add/smul). Prove continuity of members first, also by span_induction, so the add case has integrability. I used this for Hurwitz's proof of Sturm–Hurwitz (≥ 2N sign changes): ∏ (cos d_j - cos(θ - m_j)) over pairs of cut points lies in trigPoly ⌊m/2⌋ by induction with Finset.prod_range_succ. The empty product needs `(1 : ℝ → ℝ) = fun _ ↦ 1` proved by funext; simp, because `exact` fails on the unexposed Pi `1`. Small gotchas: `rw [Real.cos_sub]` can hit the wrong cosine, so pass the arguments; linarith does not unfold `set α := fun j ↦ θ (2j+1)`, so state the needed bounds as `have h : α j ≤ θ m := ...`.