Theorem fourierd

Description: Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp . Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierd.f	$$⊢\phi \to F:ℝ⟶ℝ$$
	fourierd.t	$$⊢T=2\mathrm{\pi }$$
	fourierd.per	$$⊢\left(\phi \wedge x\in ℝ\right)\to F\left(x+T\right)=F\left(x\right)$$
	fourierd.g	$$⊢G={F_{ℝ}^{\prime }\upharpoonright }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$$
	fourierd.dmdv	$$⊢\phi \to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}G\in \mathrm{Fin}$$
	fourierd.dvcn	$$⊢\phi \to G:\mathrm{dom}G\underset{cn}{⟶}ℂ$$
	fourierd.rlim	$$⊢\left(\phi \wedge x\in \left(\left[-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}G\right)\right)\to \left({G\upharpoonright }_{\left(x,\mathrm{+\infty }\right)}\right){lim}_{ℂ}x\ne \varnothing$$
	fourierd.llim	$$⊢\left(\phi \wedge x\in \left(\left(-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}G\right)\right)\to \left({G\upharpoonright }_{\left(\mathrm{-\infty },x\right)}\right){lim}_{ℂ}x\ne \varnothing$$
	fourierd.x	$$⊢\phi \to X\in ℝ$$
	fourierd.l	$$⊢\phi \to L\in \left(\left({F\upharpoonright }_{\left(\mathrm{-\infty },X\right)}\right){lim}_{ℂ}X\right)$$
	fourierd.r	$$⊢\phi \to R\in \left(\left({F\upharpoonright }_{\left(X,\mathrm{+\infty }\right)}\right){lim}_{ℂ}X\right)$$
	fourierd.a	$$⊢A=\left(n\in {\mathbb{N}}_0⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}F\left(x\right)\cos nxdx}{\mathrm{\pi }}\right)$$
	fourierd.b	$$⊢B=\left(n\in \mathbb{N}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}F\left(x\right)\sin nxdx}{\mathrm{\pi }}\right)$$
Assertion	fourierd	$$⊢\phi \to \left(\frac{A\left(0\right)}{2}\right)+\sum _{n\in \mathbb{N}}\left(A\left(n\right)\cos nX+B\left(n\right)\sin nX\right)=\frac{L+R}{2}$$

Proof

Step	Hyp	Ref	Expression
1		fourierd.f	$$⊢\phi \to F:ℝ⟶ℝ$$
2		fourierd.t	$$⊢T=2\mathrm{\pi }$$
3		fourierd.per	$$⊢\left(\phi \wedge x\in ℝ\right)\to F\left(x+T\right)=F\left(x\right)$$
4		fourierd.g	$$⊢G={F_{ℝ}^{\prime }\upharpoonright }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$$
5		fourierd.dmdv	$$⊢\phi \to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}G\in \mathrm{Fin}$$
6		fourierd.dvcn	$$⊢\phi \to G:\mathrm{dom}G\underset{cn}{⟶}ℂ$$
7		fourierd.rlim	$$⊢\left(\phi \wedge x\in \left(\left[-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}G\right)\right)\to \left({G\upharpoonright }_{\left(x,\mathrm{+\infty }\right)}\right){lim}_{ℂ}x\ne \varnothing$$
8		fourierd.llim	$$⊢\left(\phi \wedge x\in \left(\left(-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}G\right)\right)\to \left({G\upharpoonright }_{\left(\mathrm{-\infty },x\right)}\right){lim}_{ℂ}x\ne \varnothing$$
9		fourierd.x	$$⊢\phi \to X\in ℝ$$
10		fourierd.l	$$⊢\phi \to L\in \left(\left({F\upharpoonright }_{\left(\mathrm{-\infty },X\right)}\right){lim}_{ℂ}X\right)$$
11		fourierd.r	$$⊢\phi \to R\in \left(\left({F\upharpoonright }_{\left(X,\mathrm{+\infty }\right)}\right){lim}_{ℂ}X\right)$$
12		fourierd.a	$$⊢A=\left(n\in {\mathbb{N}}_0⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}F\left(x\right)\cos nxdx}{\mathrm{\pi }}\right)$$
13		fourierd.b	$$⊢B=\left(n\in \mathbb{N}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}F\left(x\right)\sin nxdx}{\mathrm{\pi }}\right)$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}k\left(A\left(n\right)\cos nX+B\left(n\right)\sin nX\right)$$
15		nfmpt1	$$⊢\underset{\_}{Ⅎ}n\left(n\in {\mathbb{N}}_0⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}F\left(x\right)\cos nxdx}{\mathrm{\pi }}\right)$$
16	12 15	nfcxfr	$$⊢\underset{\_}{Ⅎ}nA$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}nk$$
18	16 17	nffv	$$⊢\underset{\_}{Ⅎ}nA\left(k\right)$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}n\times$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}n\cos kX$$
21	18 19 20	nfov	$$⊢\underset{\_}{Ⅎ}nA\left(k\right)\cos kX$$
22		nfcv	$$⊢\underset{\_}{Ⅎ}n+$$
23		nfmpt1	$$⊢\underset{\_}{Ⅎ}n\left(n\in \mathbb{N}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}F\left(x\right)\sin nxdx}{\mathrm{\pi }}\right)$$
24	13 23	nfcxfr	$$⊢\underset{\_}{Ⅎ}nB$$
25	24 17	nffv	$$⊢\underset{\_}{Ⅎ}nB\left(k\right)$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}n\sin kX$$
27	25 19 26	nfov	$$⊢\underset{\_}{Ⅎ}nB\left(k\right)\sin kX$$
28	21 22 27	nfov	$$⊢\underset{\_}{Ⅎ}n\left(A\left(k\right)\cos kX+B\left(k\right)\sin kX\right)$$
29		fveq2	$$⊢n=k\to A\left(n\right)=A\left(k\right)$$
30		oveq1	$$⊢n=k\to nX=kX$$
31	30	fveq2d	$$⊢n=k\to \cos nX=\cos kX$$
32	29 31	oveq12d	$$⊢n=k\to A\left(n\right)\cos nX=A\left(k\right)\cos kX$$
33		fveq2	$$⊢n=k\to B\left(n\right)=B\left(k\right)$$
34	30	fveq2d	$$⊢n=k\to \sin nX=\sin kX$$
35	33 34	oveq12d	$$⊢n=k\to B\left(n\right)\sin nX=B\left(k\right)\sin kX$$
36	32 35	oveq12d	$$⊢n=k\to A\left(n\right)\cos nX+B\left(n\right)\sin nX=A\left(k\right)\cos kX+B\left(k\right)\sin kX$$
37	14 28 36	cbvmpt	$$⊢\left(n\in \mathbb{N}⟼A\left(n\right)\cos nX+B\left(n\right)\sin nX\right)=\left(k\in \mathbb{N}⟼A\left(k\right)\cos kX+B\left(k\right)\sin kX\right)$$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 37	fourierdlem115	$$⊢\phi \to \left(seq1\left(+,\left(n\in \mathbb{N}⟼A\left(n\right)\cos nX+B\left(n\right)\sin nX\right)\right)⇝\left(\left(\frac{L+R}{2}\right)-\left(\frac{A\left(0\right)}{2}\right)\right)\wedge \left(\frac{A\left(0\right)}{2}\right)+\sum _{n\in \mathbb{N}}\left(A\left(n\right)\cos nX+B\left(n\right)\sin nX\right)=\frac{L+R}{2}\right)$$
39	38	simprd	$$⊢\phi \to \left(\frac{A\left(0\right)}{2}\right)+\sum _{n\in \mathbb{N}}\left(A\left(n\right)\cos nX+B\left(n\right)\sin nX\right)=\frac{L+R}{2}$$