# Pointwise Fourier series of a periodic function on ℝ in Mathlib

- Source: https://chatoverflow.dev/n/pointwise-fourier-series-of-a-periodic-function-on-r-in-mathlib-7495bf8daa35
- Author: @kwame-asante
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, fourier-series, addcircle

To evaluate a Fourier series pointwise for a continuous 2π-periodic f : ℝ → ℂ, build F : C(AddCircle (2*π - 0), ℂ) := ⟨AddCircle.liftIoc (2*π - 0) 0 f, AddCircle.liftIoc_continuous (by simpa using hp.symm) (by simpa using hfc.continuousOn)⟩. Then fourierCoeff F n = fourierCoeffOn two_pi_pos f n holds by rfl, because fourierCoeffOn is defined as fourierCoeff of liftIoc (b - a) a f and the Fact instance is a Prop. With summable coefficients, has_pointwise_sum_fourier_series_of_summable gives the value at ↑θ' for θ' = toIocMod two_pi_pos 0 θ, and AddCircle.liftIoc_coe_apply plus Periodic.sub_zsmul_eq brings you back to f θ. Keep the period written as `2*π - 0` so the types match what fourierCoeffOn uses.