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 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fouriercn.t ⊢ 𝑇 = ( 2 · π )
fouriercn.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fouriercn.dv ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( ℝ –cn→ ℂ ) )
fouriercn.g ⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
fouriercn.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fouriercn.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
fouriercn.b ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
Assertion fouriercn ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 fouriercn.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fouriercn.t ⊢ 𝑇 = ( 2 · π )
3 fouriercn.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
4 fouriercn.dv ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( ℝ –cn→ ℂ ) )
5 fouriercn.g ⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
6 fouriercn.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
7 fouriercn.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
8 fouriercn.b ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
9 5 dmeqi ⊢ dom 𝐺 = dom ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
10 ioossre ⊢ ( - π (,) π ) ⊆ ℝ
11 cncff ⊢ ( ( ℝ D 𝐹 ) ∈ ( ℝ –cn→ ℂ ) → ( ℝ D 𝐹 ) : ℝ ⟶ ℂ )
12 fdm ⊢ ( ( ℝ D 𝐹 ) : ℝ ⟶ ℂ → dom ( ℝ D 𝐹 ) = ℝ )
13 4 11 12 3syl ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ℝ )
14 10 13 sseqtrrid ⊢ ( 𝜑 → ( - π (,) π ) ⊆ dom ( ℝ D 𝐹 ) )
15 ssdmres ⊢ ( ( - π (,) π ) ⊆ dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) = ( - π (,) π ) )
16 14 15 sylib ⊢ ( 𝜑 → dom ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) = ( - π (,) π ) )
17 9 16 eqtrid ⊢ ( 𝜑 → dom 𝐺 = ( - π (,) π ) )
18 17 difeq2d ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) = ( ( - π (,) π ) ∖ ( - π (,) π ) ) )
19 difid ⊢ ( ( - π (,) π ) ∖ ( - π (,) π ) ) = ∅
20 18 19 eqtrdi ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) = ∅ )
21 0fi ⊢ ∅ ∈ Fin
22 20 21 eqeltrdi ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
23 rescncf ⊢ ( ( - π (,) π ) ⊆ ℝ → ( ( ℝ D 𝐹 ) ∈ ( ℝ –cn→ ℂ ) → ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ∈ ( ( - π (,) π ) –cn→ ℂ ) ) )
24 10 4 23 mpsyl ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ∈ ( ( - π (,) π ) –cn→ ℂ ) )
25 5 a1i ⊢ ( 𝜑 → 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) )
26 17 oveq1d ⊢ ( 𝜑 → ( dom 𝐺 –cn→ ℂ ) = ( ( - π (,) π ) –cn→ ℂ ) )
27 24 25 26 3eltr4d ⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
28 pire ⊢ π ∈ ℝ
29 28 renegcli ⊢ - π ∈ ℝ
30 28 rexri ⊢ π ∈ ℝ*
31 icossre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ* ) → ( - π [,) π ) ⊆ ℝ )
32 29 30 31 mp2an ⊢ ( - π [,) π ) ⊆ ℝ
33 eldifi ⊢ ( 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) → 𝑥 ∈ ( - π [,) π ) )
34 32 33 sselid ⊢ ( 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) → 𝑥 ∈ ℝ )
35 limcresi ⊢ ( ( ℝ D 𝐹 ) limℂ 𝑥 ) ⊆ ( ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( 𝑥 (,) +∞ ) ) ) limℂ 𝑥 )
36 5 reseq1i ⊢ ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) = ( ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ↾ ( 𝑥 (,) +∞ ) )
37 resres ⊢ ( ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ↾ ( 𝑥 (,) +∞ ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( 𝑥 (,) +∞ ) ) )
38 36 37 eqtr2i ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( 𝑥 (,) +∞ ) ) ) = ( 𝐺 ↾ ( 𝑥 (,) +∞ ) )
39 38 oveq1i ⊢ ( ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( 𝑥 (,) +∞ ) ) ) limℂ 𝑥 ) = ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 )
40 35 39 sseqtri ⊢ ( ( ℝ D 𝐹 ) limℂ 𝑥 ) ⊆ ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 )
41 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ℝ D 𝐹 ) ∈ ( ℝ –cn→ ℂ ) )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
43 41 42 cnlimci ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ( ( ℝ D 𝐹 ) limℂ 𝑥 ) )
44 40 43 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) )
45 44 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
46 34 45 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
47 negpitopissre ⊢ ( - π (,] π ) ⊆ ℝ
48 eldifi ⊢ ( 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) → 𝑥 ∈ ( - π (,] π ) )
49 47 48 sselid ⊢ ( 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) → 𝑥 ∈ ℝ )
50 limcresi ⊢ ( ( ℝ D 𝐹 ) limℂ 𝑥 ) ⊆ ( ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( -∞ (,) 𝑥 ) ) ) limℂ 𝑥 )
51 5 reseq1i ⊢ ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) = ( ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ↾ ( -∞ (,) 𝑥 ) )
52 resres ⊢ ( ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) ) ↾ ( -∞ (,) 𝑥 ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( -∞ (,) 𝑥 ) ) )
53 51 52 eqtr2i ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( -∞ (,) 𝑥 ) ) ) = ( 𝐺 ↾ ( -∞ (,) 𝑥 ) )
54 53 oveq1i ⊢ ( ( ( ℝ D 𝐹 ) ↾ ( ( - π (,) π ) ∩ ( -∞ (,) 𝑥 ) ) ) limℂ 𝑥 ) = ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 )
55 50 54 sseqtri ⊢ ( ( ℝ D 𝐹 ) limℂ 𝑥 ) ⊆ ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 )
56 55 43 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) )
57 56 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
58 49 57 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
59 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
60 ax-resscn ⊢ ℝ ⊆ ℂ
61 60 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
62 1 61 fssd ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
63 ssid ⊢ ℝ ⊆ ℝ
64 63 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ )
65 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ℝ ⟶ ℂ ∧ ℝ ⊆ ℝ ) ∧ dom ( ℝ D 𝐹 ) = ℝ ) → 𝐹 ∈ ( ℝ –cn→ ℂ ) )
66 61 62 64 13 65 syl31anc ⊢ ( 𝜑 → 𝐹 ∈ ( ℝ –cn→ ℂ ) )
67 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ℝ –cn→ ℂ ) ) → ( 𝐹 ∈ ( ℝ –cn→ ℝ ) ↔ 𝐹 : ℝ ⟶ ℝ ) )
68 61 66 67 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ℝ –cn→ ℝ ) ↔ 𝐹 : ℝ ⟶ ℝ ) )
69 1 68 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( ℝ –cn→ ℝ ) )
70 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
71 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
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 ⊢ ( 𝜑 → 𝐹 ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
75 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
76 75 cncnpi ⊢ ( ( 𝐹 ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) ∧ 𝑋 ∈ ℝ ) → 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) )
77 74 6 76 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) )
78 1 2 3 5 22 27 46 58 59 77 7 8 fouriercnp ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( 𝐹 ‘ 𝑋 ) )