Metamath Proof Explorer

Theorem fouriercnp

Description: If F is continuous at the point X , then its Fourier series at X , converges to ( FX ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 fouriercnp.f 
 |-  ( ph -> F : RR --> RR )
2 fouriercnp.t 
 |-  T = ( 2 x. _pi )
3 fouriercnp.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4 fouriercnp.g 
 |-  G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
5 fouriercnp.dmdv 
 |-  ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
6 fouriercnp.dvcn 
 |-  ( ph -> G e. ( dom G -cn-> CC ) )
7 fouriercnp.rlim 
 |-  ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
8 fouriercnp.llim 
 |-  ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
9 fouriercnp.j 
 |-  J = ( topGen ` ran (,) )
10 fouriercnp.cnp 
 |-  ( ph -> F e. ( ( J CnP J ) ` X ) )
11 fouriercnp.a 
 |-  A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
12 fouriercnp.b 
 |-  B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
13 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
14 9 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
15 13 14 eqtr4i 
 |-  RR = U. J
16 15 cnprcl 
 |-  ( F e. ( ( J CnP J ) ` X ) -> X e. RR )
17 10 16 syl 
 |-  ( ph -> X e. RR )
18 limcresi 
 |-  ( F limCC X ) C_ ( ( F |` ( -oo (,) X ) ) limCC X )
19 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
20 19 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
21 9 20 eqtri 
 |-  J = ( ( TopOpen ` CCfld ) |`t RR )
22 21 oveq2i 
 |-  ( J CnP J ) = ( J CnP ( ( TopOpen ` CCfld ) |`t RR ) )
23 22 fveq1i 
 |-  ( ( J CnP J ) ` X ) = ( ( J CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` X )
24 10 23 eleqtrdi 
 |-  ( ph -> F e. ( ( J CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` X ) )
25 19 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
26 25 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
27 ax-resscn 
 |-  RR C_ CC
28 27 a1i 
 |-  ( ph -> RR C_ CC )
29 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
30 15 29 cnprest2 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ F : RR --> RR /\ RR C_ CC ) -> ( F e. ( ( J CnP ( TopOpen ` CCfld ) ) ` X ) <-> F e. ( ( J CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` X ) ) )
31 26 1 28 30 syl3anc 
 |-  ( ph -> ( F e. ( ( J CnP ( TopOpen ` CCfld ) ) ` X ) <-> F e. ( ( J CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` X ) ) )
32 24 31 mpbird 
 |-  ( ph -> F e. ( ( J CnP ( TopOpen ` CCfld ) ) ` X ) )
33 19 21 cnplimc 
 |-  ( ( RR C_ CC /\ X e. RR ) -> ( F e. ( ( J CnP ( TopOpen ` CCfld ) ) ` X ) <-> ( F : RR --> CC /\ ( F ` X ) e. ( F limCC X ) ) ) )
34 27 17 33 sylancr 
 |-  ( ph -> ( F e. ( ( J CnP ( TopOpen ` CCfld ) ) ` X ) <-> ( F : RR --> CC /\ ( F ` X ) e. ( F limCC X ) ) ) )
35 32 34 mpbid 
 |-  ( ph -> ( F : RR --> CC /\ ( F ` X ) e. ( F limCC X ) ) )
36 35 simprd 
 |-  ( ph -> ( F ` X ) e. ( F limCC X ) )
37 18 36 sseldi 
 |-  ( ph -> ( F ` X ) e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
38 limcresi 
 |-  ( F limCC X ) C_ ( ( F |` ( X (,) +oo ) ) limCC X )
39 38 36 sseldi 
 |-  ( ph -> ( F ` X ) e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
40 1 2 3 4 5 6 7 8 17 37 39 11 12 fourierd 
 |-  ( ph -> ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( ( F ` X ) + ( F ` X ) ) / 2 ) )
41 1 17 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. RR )
42 41 recnd 
 |-  ( ph -> ( F ` X ) e. CC )
43 42 2timesd 
 |-  ( ph -> ( 2 x. ( F ` X ) ) = ( ( F ` X ) + ( F ` X ) ) )
44 43 eqcomd 
 |-  ( ph -> ( ( F ` X ) + ( F ` X ) ) = ( 2 x. ( F ` X ) ) )
45 44 oveq1d 
 |-  ( ph -> ( ( ( F ` X ) + ( F ` X ) ) / 2 ) = ( ( 2 x. ( F ` X ) ) / 2 ) )
46 2cnd 
 |-  ( ph -> 2 e. CC )
47 2ne0 
 |-  2 =/= 0
48 47 a1i 
 |-  ( ph -> 2 =/= 0 )
49 42 46 48 divcan3d 
 |-  ( ph -> ( ( 2 x. ( F ` X ) ) / 2 ) = ( F ` X ) )
50 40 45 49 3eqtrd 
 |-  ( ph -> ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( F ` X ) )