Pointwise Fourier series of a periodic function on ℝ in Mathlib

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.