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 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fouriercnp.t ⊢ 𝑇 = ( 2 · π )
fouriercnp.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fouriercnp.g ⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
fouriercnp.dmdv ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
fouriercnp.dvcn ⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
fouriercnp.rlim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
fouriercnp.llim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
fouriercnp.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
fouriercnp.cnp ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 CnP 𝐽 ) ‘ 𝑋 ) )
fouriercnp.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
fouriercnp.b ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
Assertion fouriercnp ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 fouriercnp.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fouriercnp.t ⊢ 𝑇 = ( 2 · π )
3 fouriercnp.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
4 fouriercnp.g ⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
5 fouriercnp.dmdv ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
6 fouriercnp.dvcn ⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
7 fouriercnp.rlim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
8 fouriercnp.llim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
9 fouriercnp.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
10 fouriercnp.cnp ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 CnP 𝐽 ) ‘ 𝑋 ) )
11 fouriercnp.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
12 fouriercnp.b ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
13 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
14 9 unieqi ⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
15 13 14 eqtr4i ⊢ ℝ = ∪ 𝐽
16 15 cnprcl ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐽 ) ‘ 𝑋 ) → 𝑋 ∈ ℝ )
17 10 16 syl ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
18 limcresi ⊢ ( 𝐹 limℂ 𝑋 ) ⊆ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 )
19 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
20 9 19 eqtri ⊢ 𝐽 = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
21 20 oveq2i ⊢ ( 𝐽 CnP 𝐽 ) = ( 𝐽 CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
22 21 fveq1i ⊢ ( ( 𝐽 CnP 𝐽 ) ‘ 𝑋 ) = ( ( 𝐽 CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑋 )
23 10 22 eleqtrdi ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑋 ) )
24 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
25 24 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
26 25 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
27 ax-resscn ⊢ ℝ ⊆ ℂ
28 27 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
29 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
30 15 29 cnprest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝐹 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝐹 ∈ ( ( 𝐽 CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑋 ) ↔ 𝐹 ∈ ( ( 𝐽 CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑋 ) ) )
31 26 1 28 30 syl3anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑋 ) ↔ 𝐹 ∈ ( ( 𝐽 CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑋 ) ) )
32 23 31 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑋 ) )
33 24 20 cnplimc ⊢ ( ( ℝ ⊆ ℂ ∧ 𝑋 ∈ ℝ ) → ( 𝐹 ∈ ( ( 𝐽 CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑋 ) ↔ ( 𝐹 : ℝ ⟶ ℂ ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 limℂ 𝑋 ) ) ) )
34 27 17 33 sylancr ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑋 ) ↔ ( 𝐹 : ℝ ⟶ ℂ ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 limℂ 𝑋 ) ) ) )
35 32 34 mpbid ⊢ ( 𝜑 → ( 𝐹 : ℝ ⟶ ℂ ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 limℂ 𝑋 ) ) )
36 35 simprd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 limℂ 𝑋 ) )
37 18 36 sselid ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
38 limcresi ⊢ ( 𝐹 limℂ 𝑋 ) ⊆ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 )
39 38 36 sselid ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
40 1 2 3 4 5 6 7 8 17 37 39 11 12 fourierd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
41 1 17 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )
42 41 recnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℂ )
43 42 2timesd ⊢ ( 𝜑 → ( 2 · ( 𝐹 ‘ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑋 ) ) )
44 43 eqcomd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑋 ) ) = ( 2 · ( 𝐹 ‘ 𝑋 ) ) )
45 44 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑋 ) ) / 2 ) = ( ( 2 · ( 𝐹 ‘ 𝑋 ) ) / 2 ) )
46 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
47 2ne0 ⊢ 2 ≠ 0
48 47 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
49 42 46 48 divcan3d ⊢ ( 𝜑 → ( ( 2 · ( 𝐹 ‘ 𝑋 ) ) / 2 ) = ( 𝐹 ‘ 𝑋 ) )
50 40 45 49 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( 𝐹 ‘ 𝑋 ) )