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

Proof

Step Hyp Ref Expression
1 fourierclimd.f 
 |-  ( ph -> F : RR --> RR )
2 fourierclimd.t 
 |-  T = ( 2 x. _pi )
3 fourierclimd.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4 fourierclimd.g 
 |-  G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
5 fourierclimd.dmdv 
 |-  ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
6 fourierclimd.dvcn 
 |-  ( ph -> G e. ( dom G -cn-> CC ) )
7 fourierclimd.rlim 
 |-  ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
8 fourierclimd.llim 
 |-  ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
9 fourierclimd.x 
 |-  ( ph -> X e. RR )
10 fourierclimd.l 
 |-  ( ph -> L e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
11 fourierclimd.r 
 |-  ( ph -> R e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
12 fourierclimd.a 
 |-  A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
13 fourierclimd.b 
 |-  B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
14 fourierclimd.s 
 |-  S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
15 nfcv 
 |-  F/_ k ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) )
16 nfmpt1 
 |-  F/_ n ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
17 12 16 nfcxfr 
 |-  F/_ n A
18 nfcv 
 |-  F/_ n k
19 17 18 nffv 
 |-  F/_ n ( A ` k )
20 nfcv 
 |-  F/_ n x.
21 nfcv 
 |-  F/_ n ( cos ` ( k x. X ) )
22 19 20 21 nfov 
 |-  F/_ n ( ( A ` k ) x. ( cos ` ( k x. X ) ) )
23 nfcv 
 |-  F/_ n +
24 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
25 13 24 nfcxfr 
 |-  F/_ n B
26 25 18 nffv 
 |-  F/_ n ( B ` k )
27 nfcv 
 |-  F/_ n ( sin ` ( k x. X ) )
28 26 20 27 nfov 
 |-  F/_ n ( ( B ` k ) x. ( sin ` ( k x. X ) ) )
29 22 23 28 nfov 
 |-  F/_ n ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) )
30 fveq2 
 |-  ( n = k -> ( A ` n ) = ( A ` k ) )
31 oveq1 
 |-  ( n = k -> ( n x. X ) = ( k x. X ) )
32 31 fveq2d 
 |-  ( n = k -> ( cos ` ( n x. X ) ) = ( cos ` ( k x. X ) ) )
33 30 32 oveq12d 
 |-  ( n = k -> ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) = ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) )
34 fveq2 
 |-  ( n = k -> ( B ` n ) = ( B ` k ) )
35 31 fveq2d 
 |-  ( n = k -> ( sin ` ( n x. X ) ) = ( sin ` ( k x. X ) ) )
36 34 35 oveq12d 
 |-  ( n = k -> ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) = ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) )
37 33 36 oveq12d 
 |-  ( n = k -> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) = ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
38 15 29 37 cbvmpt 
 |-  ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( k e. NN |-> ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
39 14 38 eqtri 
 |-  S = ( k e. NN |-> ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
40 1 2 3 4 5 6 7 8 9 10 11 12 13 39 fourierdlem115 
 |-  ( ph -> ( seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( L + R ) / 2 ) ) )
41 40 simpld 
 |-  ( ph -> seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) )