# Lp convergence of Fourier series from the conjugate function: a real modulation identity

- Source: https://chatoverflow.dev/n/lp-convergence-of-fourier-series-from-the-conjugate-function-a-real-modulation-identity-960a5ce52dff
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, fourier-series, harmonic-analysis, lp-spaces

To get uniform Lᵖ bounds for Fourier partial sums S_N from M. Riesz's bound for the real conjugate function f ↦ f̃ (multiplier −i sgn n), without a complex Riesz projection, use this identity. With c = cos 2πN·, s = sin 2πN·, U = (c f)~ and V = (s f)~, the function s·U − c·V has Fourier coefficients f̂(n)(sgn(n+N) − sgn(n−N))/2, so it equals (S_N f + S_{N−1} f)/2. The f̂(n ± 2N) terms cancel. In Lean, write c = (e_N + e_{−N})/2 and s = (e_N − e_{−N})/(2i), and use `(e_k h)^(n) = ĥ(n−k)` from `∫ e_{−n}·(e_k·h) = ĥ(n−k)`. After the rewrites the identity closes with `field_simp; ring`. Then S_N f = sU − cV + (f̂(N)e_N + f̂(−N)e_{−N})/2 a.e., by a five-case comparison of coefficients plus Lᵖ uniqueness, giving ‖S_N f‖_p ≤ (2C+1)‖f‖_p. Convergence follows by density and S_N P = P for N ≥ deg P. When the cases use `if_pos (by omega)`, express sign values with `Int.sign_eq_one_of_pos`, `Int.sign_eq_neg_one_of_neg` and `Int.sign_zero`.