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 φ F :
fouriercn.t T = 2 π
fouriercn.per φ x F x + T = F x
fouriercn.dv φ F : cn
fouriercn.g G = F π π
fouriercn.x φ X
fouriercn.a A = n 0 π π F x cos n x dx π
fouriercn.b B = n π π F x sin n x dx π
Assertion fouriercn φ A 0 2 + n A n cos n X + B n sin n X = F X

Proof

Step Hyp Ref Expression
1 fouriercn.f φ F :
2 fouriercn.t T = 2 π
3 fouriercn.per φ x F x + T = F x
4 fouriercn.dv φ F : cn
5 fouriercn.g G = F π π
6 fouriercn.x φ X
7 fouriercn.a A = n 0 π π F x cos n x dx π
8 fouriercn.b B = n π π F x sin n x dx π
9 5 dmeqi dom G = dom F π π
10 ioossre π π
11 cncff F : cn F :
12 fdm F : dom F =
13 4 11 12 3syl φ dom F =
14 10 13 sseqtrrid φ π π dom F
15 ssdmres π π dom F dom F π π = π π
16 14 15 sylib φ dom F π π = π π
17 9 16 syl5eq φ dom G = π π
18 17 difeq2d φ π π dom G = π π π π
19 difid π π π π =
20 18 19 syl6eq φ π π dom G =
21 0fin Fin
22 20 21 eqeltrdi φ π π dom G Fin
23 rescncf π π F : cn F π π : π π cn
24 10 4 23 mpsyl φ F π π : π π cn
25 5 a1i φ G = F π π
26 17 oveq1d φ dom G cn = π π cn
27 24 25 26 3eltr4d φ G : dom G cn
28 pire π
29 28 renegcli π
30 28 rexri π *
31 icossre π π * π π
32 29 30 31 mp2an π π
33 eldifi x π π dom G x π π
34 32 33 sseldi x π π dom G x
35 limcresi F lim x F π π x +∞ lim x
36 5 reseq1i G x +∞ = F π π x +∞
37 resres F π π x +∞ = F π π x +∞
38 36 37 eqtr2i F π π x +∞ = G x +∞
39 38 oveq1i F π π x +∞ lim x = G x +∞ lim x
40 35 39 sseqtri F lim x G x +∞ lim x
41 4 adantr φ x F : cn
42 simpr φ x x
43 41 42 cnlimci φ x F x F lim x
44 40 43 sseldi φ x F x G x +∞ lim x
45 44 ne0d φ x G x +∞ lim x
46 34 45 sylan2 φ x π π dom G G x +∞ lim x
47 negpitopissre π π
48 eldifi x π π dom G x π π
49 47 48 sseldi x π π dom G x
50 limcresi F lim x F π π −∞ x lim x
51 5 reseq1i G −∞ x = F π π −∞ x
52 resres F π π −∞ x = F π π −∞ x
53 51 52 eqtr2i F π π −∞ x = G −∞ x
54 53 oveq1i F π π −∞ x lim x = G −∞ x lim x
55 50 54 sseqtri F lim x G −∞ x lim x
56 55 43 sseldi φ x F x G −∞ x lim x
57 56 ne0d φ x G −∞ x lim x
58 49 57 sylan2 φ x π π dom G G −∞ x lim x
59 eqid topGen ran . = topGen ran .
60 ax-resscn
61 60 a1i φ
62 1 61 fssd φ F :
63 ssid
64 63 a1i φ
65 dvcn F : dom F = F : cn
66 61 62 64 13 65 syl31anc φ F : cn
67 cncffvrn F : cn F : cn F :
68 61 66 67 syl2anc φ F : cn F :
69 1 68 mpbird φ F : cn
70 eqid TopOpen fld = TopOpen fld
71 70 tgioo2 topGen ran . = TopOpen fld 𝑡
72 70 71 71 cncfcn cn = topGen ran . Cn topGen ran .
73 61 61 72 syl2anc φ cn = topGen ran . Cn topGen ran .
74 69 73 eleqtrd φ F topGen ran . Cn topGen ran .
75 uniretop = topGen ran .
76 75 cncnpi F topGen ran . Cn topGen ran . X F topGen ran . CnP topGen ran . X
77 74 6 76 syl2anc φ F topGen ran . CnP topGen ran . X
78 1 2 3 5 22 27 46 58 59 77 7 8 fouriercnp φ A 0 2 + n A n cos n X + B n sin n X = F X