Metamath Proof Explorer

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 }↾}_{\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}↾}_{\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}↾}_{\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}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
fourierd.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
fourierd.a ${⊢}{A}=\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)$
fourierd.b ${⊢}{B}=\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}\right)$
Assertion fourierd ${⊢}{\phi }\to \left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}\in ℕ}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\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 }↾}_{\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}↾}_{\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}↾}_{\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}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
11 fourierd.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
12 fourierd.a ${⊢}{A}=\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)$
13 fourierd.b ${⊢}{B}=\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}\right)$
14 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)$
15 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)$
16 12 15 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}$
17 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{k}$
18 16 17 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}\left({k}\right)$
19 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}×$
20 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\mathrm{cos}{k}{X}$
21 18 19 20 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}\left({k}\right)\mathrm{cos}{k}{X}$
22 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}+$
23 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}\right)$
24 13 23 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}$
25 24 17 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}\left({k}\right)$
26 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\mathrm{sin}{k}{X}$
27 25 19 26 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}\left({k}\right)\mathrm{sin}{k}{X}$
28 21 22 27 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}\right)$
29 fveq2 ${⊢}{n}={k}\to {A}\left({n}\right)={A}\left({k}\right)$
30 oveq1 ${⊢}{n}={k}\to {n}{X}={k}{X}$
31 30 fveq2d ${⊢}{n}={k}\to \mathrm{cos}{n}{X}=\mathrm{cos}{k}{X}$
32 29 31 oveq12d ${⊢}{n}={k}\to {A}\left({n}\right)\mathrm{cos}{n}{X}={A}\left({k}\right)\mathrm{cos}{k}{X}$
33 fveq2 ${⊢}{n}={k}\to {B}\left({n}\right)={B}\left({k}\right)$
34 30 fveq2d ${⊢}{n}={k}\to \mathrm{sin}{n}{X}=\mathrm{sin}{k}{X}$
35 33 34 oveq12d ${⊢}{n}={k}\to {B}\left({n}\right)\mathrm{sin}{n}{X}={B}\left({k}\right)\mathrm{sin}{k}{X}$
36 32 35 oveq12d ${⊢}{n}={k}\to {A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}={A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}$
37 14 28 36 cbvmpt ${⊢}\left({n}\in ℕ⟼{A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)=\left({k}\in ℕ⟼{A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}\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 ℕ⟼{A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\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 ℕ}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)=\frac{{L}+{R}}{2}\right)$
39 38 simprd ${⊢}{\phi }\to \left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}\in ℕ}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)=\frac{{L}+{R}}{2}$