Metamath Proof Explorer

Theorem fourier2

Description: Fourier series convergence, for a piecewise smooth function. Here it is also proven the existence of the left and right limits of F at any given point X . See fourierd for a comparison. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourier2.f 
|- ( ph -> F : RR --> RR )
fourier2.t 
|- T = ( 2 x. _pi )
fourier2.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourier2.g 
|- G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
fourier2.dmdv 
|- ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
fourier2.dvcn 
|- ( ph -> G e. ( dom G -cn-> CC ) )
fourier2.rlim 
|- ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
fourier2.llim 
|- ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
fourier2.x 
|- ( ph -> X e. RR )
fourier2.a 
|- A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
fourier2.b 
|- B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
Assertion fourier2 
|- ( ph -> E. l e. ( ( F |` ( -oo (,) X ) ) limCC X ) E. r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) )

Proof

Step Hyp Ref Expression
1 fourier2.f 
 |-  ( ph -> F : RR --> RR )
2 fourier2.t 
 |-  T = ( 2 x. _pi )
3 fourier2.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4 fourier2.g 
 |-  G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
5 fourier2.dmdv 
 |-  ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
6 fourier2.dvcn 
 |-  ( ph -> G e. ( dom G -cn-> CC ) )
7 fourier2.rlim 
 |-  ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
8 fourier2.llim 
 |-  ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
9 fourier2.x 
 |-  ( ph -> X e. RR )
10 fourier2.a 
 |-  A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
11 fourier2.b 
 |-  B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
12 1 2 3 4 5 6 7 8 9 fourierdlem106 
 |-  ( ph -> ( ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) /\ ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) )
13 12 simpld 
 |-  ( ph -> ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) )
14 n0 
 |-  ( ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) <-> E. l l e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
15 13 14 sylib 
 |-  ( ph -> E. l l e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
16 simpr 
 |-  ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) -> l e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
17 12 simprd 
 |-  ( ph -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )
18 n0 
 |-  ( ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) <-> E. r r e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
19 17 18 sylib 
 |-  ( ph -> E. r r e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
20 19 adantr 
 |-  ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) -> E. r r e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
21 simpr 
 |-  ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) -> r e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
22 1 ad2antrr 
 |-  ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) -> F : RR --> RR )
23 3 ad4ant14 
 |-  ( ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
24 5 ad2antrr 
 |-  ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
25 6 ad2antrr 
 |-  ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) -> G e. ( dom G -cn-> CC ) )
26 7 ad4ant14 
 |-  ( ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
27 8 ad4ant14 
 |-  ( ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
28 9 ad2antrr 
 |-  ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) -> X e. RR )
29 16 adantr 
 |-  ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) -> l e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
30 22 2 23 4 24 25 26 27 28 29 21 10 11 fourierd 
 |-  ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) -> ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) )
31 21 30 jca 
 |-  ( ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) /\ r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ) -> ( r e. ( ( F |` ( X (,) +oo ) ) limCC X ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) ) )
32 31 ex 
 |-  ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) -> ( r e. ( ( F |` ( X (,) +oo ) ) limCC X ) -> ( r e. ( ( F |` ( X (,) +oo ) ) limCC X ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) ) ) )
33 32 eximdv 
 |-  ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) -> ( E. r r e. ( ( F |` ( X (,) +oo ) ) limCC X ) -> E. r ( r e. ( ( F |` ( X (,) +oo ) ) limCC X ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) ) ) )
34 20 33 mpd 
 |-  ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) -> E. r ( r e. ( ( F |` ( X (,) +oo ) ) limCC X ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) ) )
35 df-rex 
 |-  ( E. r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) <-> E. r ( r e. ( ( F |` ( X (,) +oo ) ) limCC X ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) ) )
36 34 35 sylibr 
 |-  ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) -> E. r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) )
37 16 36 jca 
 |-  ( ( ph /\ l e. ( ( F |` ( -oo (,) X ) ) limCC X ) ) -> ( l e. ( ( F |` ( -oo (,) X ) ) limCC X ) /\ E. r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) ) )
38 37 ex 
 |-  ( ph -> ( l e. ( ( F |` ( -oo (,) X ) ) limCC X ) -> ( l e. ( ( F |` ( -oo (,) X ) ) limCC X ) /\ E. r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) ) ) )
39 38 eximdv 
 |-  ( ph -> ( E. l l e. ( ( F |` ( -oo (,) X ) ) limCC X ) -> E. l ( l e. ( ( F |` ( -oo (,) X ) ) limCC X ) /\ E. r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) ) ) )
40 15 39 mpd 
 |-  ( ph -> E. l ( l e. ( ( F |` ( -oo (,) X ) ) limCC X ) /\ E. r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ( ( ( 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 df-rex 
 |-  ( E. l e. ( ( F |` ( -oo (,) X ) ) limCC X ) E. r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) <-> E. l ( l e. ( ( F |` ( -oo (,) X ) ) limCC X ) /\ E. r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) ) )
42 40 41 sylibr 
 |-  ( ph -> E. l e. ( ( F |` ( -oo (,) X ) ) limCC X ) E. r e. ( ( F |` ( X (,) +oo ) ) limCC X ) ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( l + r ) / 2 ) )