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 φ F :
fourierclimd.t T = 2 π
fourierclimd.per φ x F x + T = F x
fourierclimd.g G = F π π
fourierclimd.dmdv φ π π dom G Fin
fourierclimd.dvcn φ G : dom G cn
fourierclimd.rlim φ x π π dom G G x +∞ lim x
fourierclimd.llim φ x π π dom G G −∞ x lim x
fourierclimd.x φ X
fourierclimd.l φ L F −∞ X lim X
fourierclimd.r φ R F X +∞ lim X
fourierclimd.a A = n 0 π π F x cos n x dx π
fourierclimd.b B = n π π F x sin n x dx π
fourierclimd.s S = n A n cos n X + B n sin n X
Assertion fourierclimd φ seq 1 + S L + R 2 A 0 2

Proof

Step Hyp Ref Expression
1 fourierclimd.f φ F :
2 fourierclimd.t T = 2 π
3 fourierclimd.per φ x F x + T = F x
4 fourierclimd.g G = F π π
5 fourierclimd.dmdv φ π π dom G Fin
6 fourierclimd.dvcn φ G : dom G cn
7 fourierclimd.rlim φ x π π dom G G x +∞ lim x
8 fourierclimd.llim φ x π π dom G G −∞ x lim x
9 fourierclimd.x φ X
10 fourierclimd.l φ L F −∞ X lim X
11 fourierclimd.r φ R F X +∞ lim X
12 fourierclimd.a A = n 0 π π F x cos n x dx π
13 fourierclimd.b B = n π π F x sin n x dx π
14 fourierclimd.s S = n A n cos n X + B n sin n X
15 nfcv _ k A n cos n X + B n sin n X
16 nfmpt1 _ n n 0 π π F x cos n x dx π
17 12 16 nfcxfr _ n A
18 nfcv _ n k
19 17 18 nffv _ n A k
20 nfcv _ n ×
21 nfcv _ n cos k X
22 19 20 21 nfov _ n A k cos k X
23 nfcv _ n +
24 nfmpt1 _ n n π π F x sin n x dx π
25 13 24 nfcxfr _ n B
26 25 18 nffv _ n B k
27 nfcv _ n sin k X
28 26 20 27 nfov _ n B k sin k X
29 22 23 28 nfov _ n A k cos k X + B k sin k X
30 fveq2 n = k A n = A k
31 oveq1 n = k n X = k X
32 31 fveq2d n = k cos n X = cos k X
33 30 32 oveq12d n = k A n cos n X = A k cos k X
34 fveq2 n = k B n = B k
35 31 fveq2d n = k sin n X = sin k X
36 34 35 oveq12d n = k B n sin n X = B k sin k X
37 33 36 oveq12d n = k A n cos n X + B n sin n X = A k cos k X + B k sin k X
38 15 29 37 cbvmpt n A n cos n X + B n sin n X = k A k cos k X + B k sin k X
39 14 38 eqtri S = k A k cos k X + B k sin k X
40 1 2 3 4 5 6 7 8 9 10 11 12 13 39 fourierdlem115 φ seq 1 + S L + R 2 A 0 2 A 0 2 + n A n cos n X + B n sin n X = L + R 2
41 40 simpld φ seq 1 + S L + R 2 A 0 2