This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )