Metamath Proof Explorer

Theorem fouriercn

Description: If the derivative of F is continuous, then the Fourier series for F converges to F everywhere and the hypothesis are simpler than those for the more general case of a piecewise smooth function (see fourierd for a comparison). (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fouriercn.f 
|- ( ph -> F : RR --> RR )
fouriercn.t 
|- T = ( 2 x. _pi )
fouriercn.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fouriercn.dv 
|- ( ph -> ( RR _D F ) e. ( RR -cn-> CC ) )
fouriercn.g 
|- G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
fouriercn.x 
|- ( ph -> X e. RR )
fouriercn.a 
|- A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
fouriercn.b 
|- B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
Assertion fouriercn 
|- ( 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 fouriercn.f 
 |-  ( ph -> F : RR --> RR )
2 fouriercn.t 
 |-  T = ( 2 x. _pi )
3 fouriercn.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4 fouriercn.dv 
 |-  ( ph -> ( RR _D F ) e. ( RR -cn-> CC ) )
5 fouriercn.g 
 |-  G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
6 fouriercn.x 
 |-  ( ph -> X e. RR )
7 fouriercn.a 
 |-  A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
8 fouriercn.b 
 |-  B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
9 5 dmeqi 
 |-  dom G = dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
10 ioossre 
 |-  ( -u _pi (,) _pi ) C_ RR
11 cncff 
 |-  ( ( RR _D F ) e. ( RR -cn-> CC ) -> ( RR _D F ) : RR --> CC )
12 fdm 
 |-  ( ( RR _D F ) : RR --> CC -> dom ( RR _D F ) = RR )
13 4 11 12 3syl 
 |-  ( ph -> dom ( RR _D F ) = RR )
14 10 13 sseqtrrid 
 |-  ( ph -> ( -u _pi (,) _pi ) C_ dom ( RR _D F ) )
15 ssdmres 
 |-  ( ( -u _pi (,) _pi ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) = ( -u _pi (,) _pi ) )
16 14 15 sylib 
 |-  ( ph -> dom ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) = ( -u _pi (,) _pi ) )
17 9 16 eqtrid 
 |-  ( ph -> dom G = ( -u _pi (,) _pi ) )
18 17 difeq2d 
 |-  ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) = ( ( -u _pi (,) _pi ) \ ( -u _pi (,) _pi ) ) )
19 difid 
 |-  ( ( -u _pi (,) _pi ) \ ( -u _pi (,) _pi ) ) = (/)
20 18 19 eqtrdi 
 |-  ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) = (/) )
21 0fin 
 |-  (/) e. Fin
22 20 21 eqeltrdi 
 |-  ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
23 rescncf 
 |-  ( ( -u _pi (,) _pi ) C_ RR -> ( ( RR _D F ) e. ( RR -cn-> CC ) -> ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) ) )
24 10 4 23 mpsyl 
 |-  ( ph -> ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
25 5 a1i 
 |-  ( ph -> G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) )
26 17 oveq1d 
 |-  ( ph -> ( dom G -cn-> CC ) = ( ( -u _pi (,) _pi ) -cn-> CC ) )
27 24 25 26 3eltr4d 
 |-  ( ph -> G e. ( dom G -cn-> CC ) )
28 pire 
 |-  _pi e. RR
29 28 renegcli 
 |-  -u _pi e. RR
30 28 rexri 
 |-  _pi e. RR*
31 icossre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR* ) -> ( -u _pi [,) _pi ) C_ RR )
32 29 30 31 mp2an 
 |-  ( -u _pi [,) _pi ) C_ RR
33 eldifi 
 |-  ( x e. ( ( -u _pi [,) _pi ) \ dom G ) -> x e. ( -u _pi [,) _pi ) )
34 32 33 sselid 
 |-  ( x e. ( ( -u _pi [,) _pi ) \ dom G ) -> x e. RR )
35 limcresi 
 |-  ( ( RR _D F ) limCC x ) C_ ( ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( x (,) +oo ) ) ) limCC x )
36 5 reseq1i 
 |-  ( G |` ( x (,) +oo ) ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) )
37 resres 
 |-  ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( x (,) +oo ) ) = ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( x (,) +oo ) ) )
38 36 37 eqtr2i 
 |-  ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( x (,) +oo ) ) ) = ( G |` ( x (,) +oo ) )
39 38 oveq1i 
 |-  ( ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( x (,) +oo ) ) ) limCC x ) = ( ( G |` ( x (,) +oo ) ) limCC x )
40 35 39 sseqtri 
 |-  ( ( RR _D F ) limCC x ) C_ ( ( G |` ( x (,) +oo ) ) limCC x )
41 4 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( RR _D F ) e. ( RR -cn-> CC ) )
42 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
43 41 42 cnlimci 
 |-  ( ( ph /\ x e. RR ) -> ( ( RR _D F ) ` x ) e. ( ( RR _D F ) limCC x ) )
44 40 43 sselid 
 |-  ( ( ph /\ x e. RR ) -> ( ( RR _D F ) ` x ) e. ( ( G |` ( x (,) +oo ) ) limCC x ) )
45 44 ne0d 
 |-  ( ( ph /\ x e. RR ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
46 34 45 sylan2 
 |-  ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
47 negpitopissre 
 |-  ( -u _pi (,] _pi ) C_ RR
48 eldifi 
 |-  ( x e. ( ( -u _pi (,] _pi ) \ dom G ) -> x e. ( -u _pi (,] _pi ) )
49 47 48 sselid 
 |-  ( x e. ( ( -u _pi (,] _pi ) \ dom G ) -> x e. RR )
50 limcresi 
 |-  ( ( RR _D F ) limCC x ) C_ ( ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( -oo (,) x ) ) ) limCC x )
51 5 reseq1i 
 |-  ( G |` ( -oo (,) x ) ) = ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) )
52 resres 
 |-  ( ( ( RR _D F ) |` ( -u _pi (,) _pi ) ) |` ( -oo (,) x ) ) = ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( -oo (,) x ) ) )
53 51 52 eqtr2i 
 |-  ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( -oo (,) x ) ) ) = ( G |` ( -oo (,) x ) )
54 53 oveq1i 
 |-  ( ( ( RR _D F ) |` ( ( -u _pi (,) _pi ) i^i ( -oo (,) x ) ) ) limCC x ) = ( ( G |` ( -oo (,) x ) ) limCC x )
55 50 54 sseqtri 
 |-  ( ( RR _D F ) limCC x ) C_ ( ( G |` ( -oo (,) x ) ) limCC x )
56 55 43 sselid 
 |-  ( ( ph /\ x e. RR ) -> ( ( RR _D F ) ` x ) e. ( ( G |` ( -oo (,) x ) ) limCC x ) )
57 56 ne0d 
 |-  ( ( ph /\ x e. RR ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
58 49 57 sylan2 
 |-  ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
59 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
60 ax-resscn 
 |-  RR C_ CC
61 60 a1i 
 |-  ( ph -> RR C_ CC )
62 1 61 fssd 
 |-  ( ph -> F : RR --> CC )
63 ssid 
 |-  RR C_ RR
64 63 a1i 
 |-  ( ph -> RR C_ RR )
65 dvcn 
 |-  ( ( ( RR C_ CC /\ F : RR --> CC /\ RR C_ RR ) /\ dom ( RR _D F ) = RR ) -> F e. ( RR -cn-> CC ) )
66 61 62 64 13 65 syl31anc 
 |-  ( ph -> F e. ( RR -cn-> CC ) )
67 cncffvrn 
 |-  ( ( RR C_ CC /\ F e. ( RR -cn-> CC ) ) -> ( F e. ( RR -cn-> RR ) <-> F : RR --> RR ) )
68 61 66 67 syl2anc 
 |-  ( ph -> ( F e. ( RR -cn-> RR ) <-> F : RR --> RR ) )
69 1 68 mpbird 
 |-  ( ph -> F e. ( RR -cn-> RR ) )
70 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
71 70 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
72 70 71 71 cncfcn 
 |-  ( ( RR C_ CC /\ RR C_ CC ) -> ( RR -cn-> RR ) = ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
73 61 61 72 syl2anc 
 |-  ( ph -> ( RR -cn-> RR ) = ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
74 69 73 eleqtrd 
 |-  ( ph -> F e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
75 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
76 75 cncnpi 
 |-  ( ( F e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) /\ X e. RR ) -> F e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` X ) )
77 74 6 76 syl2anc 
 |-  ( ph -> F e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` X ) )
78 1 2 3 5 22 27 46 58 59 77 7 8 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 ) )