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 : RR --> RR
fourierclim.t 
|- T = ( 2 x. _pi )
fourierclim.per 
|- ( x e. RR -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierclim.g 
|- G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
fourierclim.dmdv 
|- ( ( -u _pi (,) _pi ) \ dom G ) e. Fin
fourierclim.dvcn 
|- G e. ( dom G -cn-> CC )
fourierclim.rlim 
|- ( x e. ( ( -u _pi [,) _pi ) \ dom G ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
fourierclim.llim 
|- ( x e. ( ( -u _pi (,] _pi ) \ dom G ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
fourierclim.x 
|- X e. RR
fourierclim.l 
|- L e. ( ( F |` ( -oo (,) X ) ) limCC X )
fourierclim.r 
|- R e. ( ( F |` ( X (,) +oo ) ) limCC X )
fourierclim.a 
|- A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
fourierclim.b 
|- B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
fourierclim.s 
|- S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
Assertion fourierclim 
|- seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 fourierclim.f 
 |-  F : RR --> RR
2 fourierclim.t 
 |-  T = ( 2 x. _pi )
3 fourierclim.per 
 |-  ( x e. RR -> ( F ` ( x + T ) ) = ( F ` x ) )
4 fourierclim.g 
 |-  G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
5 fourierclim.dmdv 
 |-  ( ( -u _pi (,) _pi ) \ dom G ) e. Fin
6 fourierclim.dvcn 
 |-  G e. ( dom G -cn-> CC )
7 fourierclim.rlim 
 |-  ( x e. ( ( -u _pi [,) _pi ) \ dom G ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
8 fourierclim.llim 
 |-  ( x e. ( ( -u _pi (,] _pi ) \ dom G ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
9 fourierclim.x 
 |-  X e. RR
10 fourierclim.l 
 |-  L e. ( ( F |` ( -oo (,) X ) ) limCC X )
11 fourierclim.r 
 |-  R e. ( ( F |` ( X (,) +oo ) ) limCC X )
12 fourierclim.a 
 |-  A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
13 fourierclim.b 
 |-  B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
14 fourierclim.s 
 |-  S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
15 1 a1i 
 |-  ( T. -> F : RR --> RR )
16 3 adantl 
 |-  ( ( T. /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
17 5 a1i 
 |-  ( T. -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
18 6 a1i 
 |-  ( T. -> G e. ( dom G -cn-> CC ) )
19 7 adantl 
 |-  ( ( T. /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
20 8 adantl 
 |-  ( ( T. /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
21 9 a1i 
 |-  ( T. -> X e. RR )
22 10 a1i 
 |-  ( T. -> L e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
23 11 a1i 
 |-  ( T. -> R e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
24 15 2 16 4 17 18 19 20 21 22 23 12 13 14 fourierclimd 
 |-  ( T. -> seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) )
25 24 mptru 
 |-  seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) )