# Metamath Proof Explorer

## Theorem fourierclimd

Description: Fourier series convergence, for piecewise smooth functions. See fourierd for the analogous sum_ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierclimd.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fourierclimd.t ${⊢}{T}=2\mathrm{\pi }$
fourierclimd.per ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
fourierclimd.g ${⊢}{G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
fourierclimd.dmdv ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\in \mathrm{Fin}$
fourierclimd.dvcn ${⊢}{\phi }\to {G}:\mathrm{dom}{G}\underset{cn}{⟶}ℂ$
fourierclimd.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$
fourierclimd.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$
fourierclimd.x ${⊢}{\phi }\to {X}\in ℝ$
fourierclimd.l ${⊢}{\phi }\to {L}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
fourierclimd.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
fourierclimd.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)$
fourierclimd.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)$
fourierclimd.s ${⊢}{S}=\left({n}\in ℕ⟼{A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)$
Assertion fourierclimd ${⊢}{\phi }\to seq1\left(+,{S}\right)⇝\left(\left(\frac{{L}+{R}}{2}\right)-\left(\frac{{A}\left(0\right)}{2}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fourierclimd.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 fourierclimd.t ${⊢}{T}=2\mathrm{\pi }$
3 fourierclimd.per ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
4 fourierclimd.g ${⊢}{G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
5 fourierclimd.dmdv ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\in \mathrm{Fin}$
6 fourierclimd.dvcn ${⊢}{\phi }\to {G}:\mathrm{dom}{G}\underset{cn}{⟶}ℂ$
7 fourierclimd.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 fourierclimd.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 fourierclimd.x ${⊢}{\phi }\to {X}\in ℝ$
10 fourierclimd.l ${⊢}{\phi }\to {L}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
11 fourierclimd.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
12 fourierclimd.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 fourierclimd.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 fourierclimd.s ${⊢}{S}=\left({n}\in ℕ⟼{A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)$
15 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)$
16 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)$
17 12 16 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}$
18 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{k}$
19 17 18 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}\left({k}\right)$
20 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}×$
21 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\mathrm{cos}{k}{X}$
22 19 20 21 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}\left({k}\right)\mathrm{cos}{k}{X}$
23 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}+$
24 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)$
25 13 24 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}$
26 25 18 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}\left({k}\right)$
27 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\mathrm{sin}{k}{X}$
28 26 20 27 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}\left({k}\right)\mathrm{sin}{k}{X}$
29 22 23 28 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)$
30 fveq2 ${⊢}{n}={k}\to {A}\left({n}\right)={A}\left({k}\right)$
31 oveq1 ${⊢}{n}={k}\to {n}{X}={k}{X}$
32 31 fveq2d ${⊢}{n}={k}\to \mathrm{cos}{n}{X}=\mathrm{cos}{k}{X}$
33 30 32 oveq12d ${⊢}{n}={k}\to {A}\left({n}\right)\mathrm{cos}{n}{X}={A}\left({k}\right)\mathrm{cos}{k}{X}$
34 fveq2 ${⊢}{n}={k}\to {B}\left({n}\right)={B}\left({k}\right)$
35 31 fveq2d ${⊢}{n}={k}\to \mathrm{sin}{n}{X}=\mathrm{sin}{k}{X}$
36 34 35 oveq12d ${⊢}{n}={k}\to {B}\left({n}\right)\mathrm{sin}{n}{X}={B}\left({k}\right)\mathrm{sin}{k}{X}$
37 33 36 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}$
38 15 29 37 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)$
39 14 38 eqtri ${⊢}{S}=\left({k}\in ℕ⟼{A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}\right)$
40 1 2 3 4 5 6 7 8 9 10 11 12 13 39 fourierdlem115 ${⊢}{\phi }\to \left(seq1\left(+,{S}\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)$
41 40 simpld ${⊢}{\phi }\to seq1\left(+,{S}\right)⇝\left(\left(\frac{{L}+{R}}{2}\right)-\left(\frac{{A}\left(0\right)}{2}\right)\right)$