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	$⊢ F : ℝ ⟶ ℝ$
	fourierclim.t	$⊢ T = 2 π$
	fourierclim.per	$⊢ x \in ℝ \to F (x + T) = F (x)$
	fourierclim.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
	fourierclim.dmdv	$⊢ (- π, π) ∖ dom G \in Fin$
	fourierclim.dvcn	$⊢ G : dom G \underset{cn}{⟶} ℂ$
	fourierclim.rlim	$⊢ x \in ([- π, π) ∖ dom G) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
	fourierclim.llim	$⊢ x \in ((- π, π] ∖ dom G) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
	fourierclim.x	$⊢ X \in ℝ$
	fourierclim.l	$⊢ L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
	fourierclim.r	$⊢ R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierclim.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
	fourierclim.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
	fourierclim.s	$⊢ S = (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X)$
Assertion	fourierclim	$⊢ seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2}))$

Proof

Step	Hyp	Ref	Expression
1		fourierclim.f	$⊢ F : ℝ ⟶ ℝ$
2		fourierclim.t	$⊢ T = 2 π$
3		fourierclim.per	$⊢ x \in ℝ \to F (x + T) = F (x)$
4		fourierclim.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
5		fourierclim.dmdv	$⊢ (- π, π) ∖ dom G \in Fin$
6		fourierclim.dvcn	$⊢ G : dom G \underset{cn}{⟶} ℂ$
7		fourierclim.rlim	$⊢ x \in ([- π, π) ∖ dom G) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
8		fourierclim.llim	$⊢ x \in ((- π, π] ∖ dom G) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
9		fourierclim.x	$⊢ X \in ℝ$
10		fourierclim.l	$⊢ L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
11		fourierclim.r	$⊢ R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
12		fourierclim.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
13		fourierclim.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
14		fourierclim.s	$⊢ S = (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X)$
15	1	a1i	$⊢ ⊤ \to F : ℝ ⟶ ℝ$
16	3	adantl	$⊢ (⊤ \land x \in ℝ) \to F (x + T) = F (x)$
17	5	a1i	$⊢ ⊤ \to (- π, π) ∖ dom G \in Fin$
18	6	a1i	$⊢ ⊤ \to G : dom G \underset{cn}{⟶} ℂ$
19	7	adantl	$⊢ (⊤ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
20	8	adantl	$⊢ (⊤ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
21	9	a1i	$⊢ ⊤ \to X \in ℝ$
22	10	a1i	$⊢ ⊤ \to L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
23	11	a1i	$⊢ ⊤ \to R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
24	15 2 16 4 17 18 19 20 21 22 23 12 13 14	fourierclimd	$⊢ ⊤ \to seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2}))$
25	24	mptru	$⊢ seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2}))$

Metamath Proof Explorer

Theorem fourierclim

Proof