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