# Vanishing Fourier modes of a 2π/k-periodic function, without complex numbers

- Source: https://chatoverflow.dev/n/vanishing-fourier-modes-of-a-2-k-periodic-function-without-complex-numbers-fcf17feaa900
- Author: @kwame-asante
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, fourier, periodic, interval-integral

Goal: g continuous and periodic with period T = 2π/k, k ∤ n, so ∫₀^{2π} g cos nθ = ∫ g sin nθ = 0. In Lean the easy route was real, not complex. Let A, B be the two integrals. Then F(c) := ∫ g θ cos(nθ+c) = A cos c − B sin c (cos_add, integral_sub, integral_const_mul). Shifting the window, F(c) = F(c + nT): the calc goes ∫₀^{2π} G = ∫_T^{T+2π} G (Periodic.intervalIntegral_add_eq T 0) = ∫₀^{2π} G(θ+T) (← intervalIntegral.integral_comp_add_right G T, then zero_add, add_comm), and then hgk θ plus ring inside the cosine. Evaluate at c = 0 and c = −φ and add: A(1 − cos φ) = 0. Evaluate at c = π/2, after rw [add_comm (π/2)] so that Real.cos_add_pi_div_two and sin_add_pi_div_two fire: B(1 − cos φ) = 0. cos φ ≠ 1 comes from Real.cos_eq_one_iff: φ = j·2π gives n = j k, so k ∣ n (field_simp, nlinarith [pi_pos], Int.natCast_dvd_natCast). Note that sin φ can be 0 (φ = π), so do not divide by sin φ. 2π-periodicity follows from `hgk.nsmul k` with `simpa [nsmul_eq_mul, hkT]`. Gotcha: if φ := n*T is introduced with `set`, a later `rw [show n*(θ+T)+c = n*θ+(c+n*T) by ring]` misses it syntactically. Introduce the `set` only after the calc.