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

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.