Metamath Proof Explorer


Theorem fourierclim

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

Ref Expression
Hypotheses fourierclim.f F :
fourierclim.t T = 2 π
fourierclim.per x F x + T = F x
fourierclim.g G = F π π
fourierclim.dmdv π π dom G Fin
fourierclim.dvcn G : dom G cn
fourierclim.rlim x π π dom G G x +∞ lim x
fourierclim.llim x π π dom G G −∞ x lim x
fourierclim.x X
fourierclim.l L F −∞ X lim X
fourierclim.r R F X +∞ lim X
fourierclim.a A = n 0 π π F x cos n x dx π
fourierclim.b B = n π π F x sin n x dx π
fourierclim.s S = n A n cos n X + B n sin n X
Assertion fourierclim seq 1 + S L + R 2 A 0 2

Proof

Step Hyp Ref Expression
1 fourierclim.f F :
2 fourierclim.t T = 2 π
3 fourierclim.per x F x + T = F x
4 fourierclim.g G = F π π
5 fourierclim.dmdv π π dom G Fin
6 fourierclim.dvcn G : dom G cn
7 fourierclim.rlim x π π dom G G x +∞ lim x
8 fourierclim.llim x π π dom G G −∞ x lim x
9 fourierclim.x X
10 fourierclim.l L F −∞ X lim X
11 fourierclim.r R F X +∞ lim X
12 fourierclim.a A = n 0 π π F x cos n x dx π
13 fourierclim.b B = n π π F x sin n x dx π
14 fourierclim.s S = n A n cos n X + B n sin n X
15 1 a1i F :
16 3 adantl x F x + T = F x
17 5 a1i π π dom G Fin
18 6 a1i G : dom G cn
19 7 adantl x π π dom G G x +∞ lim x
20 8 adantl x π π dom G G −∞ x lim x
21 9 a1i X
22 10 a1i L F −∞ X lim X
23 11 a1i R F X +∞ lim X
24 15 2 16 4 17 18 19 20 21 22 23 12 13 14 fourierclimd seq 1 + S L + R 2 A 0 2
25 24 mptru seq 1 + S L + R 2 A 0 2