Theorem fourierd

Description: Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp . Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn . (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		fourierd.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierd.t	⊢ 𝑇 = ( 2 · π )
3		fourierd.per	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
4		fourierd.g	⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
5		fourierd.dmdv	⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
6		fourierd.dvcn	⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
7		fourierd.rlim	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
8		fourierd.llim	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
9		fourierd.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
10		fourierd.l	⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
11		fourierd.r	⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
12		fourierd.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
13		fourierd.b	⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
14		nfcv	⊢ Ⅎ 𝑘 ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) )
15		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
16	12 15	nfcxfr	⊢ Ⅎ 𝑛 𝐴
17		nfcv	⊢ Ⅎ 𝑛 𝑘
18	16 17	nffv	⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑘 )
19		nfcv	⊢ Ⅎ 𝑛 ·
20		nfcv	⊢ Ⅎ 𝑛 ( cos ‘ ( 𝑘 · 𝑋 ) )
21	18 19 20	nfov	⊢ Ⅎ 𝑛 ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) )
22		nfcv	⊢ Ⅎ 𝑛 +
23		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
24	13 23	nfcxfr	⊢ Ⅎ 𝑛 𝐵
25	24 17	nffv	⊢ Ⅎ 𝑛 ( 𝐵 ‘ 𝑘 )
26		nfcv	⊢ Ⅎ 𝑛 ( sin ‘ ( 𝑘 · 𝑋 ) )
27	25 19 26	nfov	⊢ Ⅎ 𝑛 ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) )
28	21 22 27	nfov	⊢ Ⅎ 𝑛 ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) )
29		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) )
30		oveq1	⊢ ( 𝑛 = 𝑘 → ( 𝑛 · 𝑋 ) = ( 𝑘 · 𝑋 ) )
31	30	fveq2d	⊢ ( 𝑛 = 𝑘 → ( cos ‘ ( 𝑛 · 𝑋 ) ) = ( cos ‘ ( 𝑘 · 𝑋 ) ) )
32	29 31	oveq12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) )
33		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐵 ‘ 𝑛 ) = ( 𝐵 ‘ 𝑘 ) )
34	30	fveq2d	⊢ ( 𝑛 = 𝑘 → ( sin ‘ ( 𝑛 · 𝑋 ) ) = ( sin ‘ ( 𝑘 · 𝑋 ) ) )
35	33 34	oveq12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) )
36	32 35	oveq12d	⊢ ( 𝑛 = 𝑘 → ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) )
37	14 28 36	cbvmpt	⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑘 ) · ( cos ‘ ( 𝑘 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( sin ‘ ( 𝑘 · 𝑋 ) ) ) ) )
38	1 2 3 4 5 6 7 8 9 10 11 12 13 37	fourierdlem115	⊢ ( 𝜑 → ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) ) ⇝ ( ( ( 𝐿 + 𝑅 ) / 2 ) − ( ( 𝐴 ‘ 0 ) / 2 ) ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝐿 + 𝑅 ) / 2 ) ) )
39	38	simprd	⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝐿 + 𝑅 ) / 2 ) )