Metamath Proof Explorer


Theorem fourierclim

Description: Fourier series convergence, for piecewise smooth functions. See fourier for the analogous sum_ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierclim.f 𝐹 : ℝ ⟶ ℝ
fourierclim.t 𝑇 = ( 2 · π )
fourierclim.per ( 𝑥 ∈ ℝ → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
fourierclim.g 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
fourierclim.dmdv ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin
fourierclim.dvcn 𝐺 ∈ ( dom 𝐺cn→ ℂ )
fourierclim.rlim ( 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) lim 𝑥 ) ≠ ∅ )
fourierclim.llim ( 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) lim 𝑥 ) ≠ ∅ )
fourierclim.x 𝑋 ∈ ℝ
fourierclim.l 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 )
fourierclim.r 𝑅 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 )
fourierclim.a 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
fourierclim.b 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
fourierclim.s 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) )
Assertion fourierclim seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 fourierclim.f 𝐹 : ℝ ⟶ ℝ
2 fourierclim.t 𝑇 = ( 2 · π )
3 fourierclim.per ( 𝑥 ∈ ℝ → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
4 fourierclim.g 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
5 fourierclim.dmdv ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin
6 fourierclim.dvcn 𝐺 ∈ ( dom 𝐺cn→ ℂ )
7 fourierclim.rlim ( 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) lim 𝑥 ) ≠ ∅ )
8 fourierclim.llim ( 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) lim 𝑥 ) ≠ ∅ )
9 fourierclim.x 𝑋 ∈ ℝ
10 fourierclim.l 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 )
11 fourierclim.r 𝑅 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 )
12 fourierclim.a 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
13 fourierclim.b 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
14 fourierclim.s 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) )
15 1 a1i ( ⊤ → 𝐹 : ℝ ⟶ ℝ )
16 3 adantl ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
17 5 a1i ( ⊤ → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
18 6 a1i ( ⊤ → 𝐺 ∈ ( dom 𝐺cn→ ℂ ) )
19 7 adantl ( ( ⊤ ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) lim 𝑥 ) ≠ ∅ )
20 8 adantl ( ( ⊤ ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) lim 𝑥 ) ≠ ∅ )
21 9 a1i ( ⊤ → 𝑋 ∈ ℝ )
22 10 a1i ( ⊤ → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 ) )
23 11 a1i ( ⊤ → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) )
24 15 2 16 4 17 18 19 20 21 22 23 12 13 14 fourierclimd ( ⊤ → seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) ) )
25 24 mptru seq 1 ( + , 𝑆 ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) )