fourierclimd

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

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

Proof

Step	Hyp	Ref	Expression
1		fourierclimd.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierclimd.t	$⊢ T = 2 π$
3		fourierclimd.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
4		fourierclimd.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
5		fourierclimd.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
6		fourierclimd.dvcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
7		fourierclimd.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
8		fourierclimd.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
9		fourierclimd.x	$⊢ φ \to X \in ℝ$
10		fourierclimd.l	$⊢ φ \to L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
11		fourierclimd.r	$⊢ φ \to R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
12		fourierclimd.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
13		fourierclimd.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
14		fourierclimd.s	$⊢ S = (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X)$
15		nfcv	$⊢ \underline{Ⅎ} k (A (n) \cos n X + B (n) \sin n X)$
16		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
17	12 16	nfcxfr	$⊢ \underline{Ⅎ} n A$
18		nfcv	$⊢ \underline{Ⅎ} n k$
19	17 18	nffv	$⊢ \underline{Ⅎ} n A (k)$
20		nfcv	$⊢ \underline{Ⅎ} n \times$
21		nfcv	$⊢ \underline{Ⅎ} n \cos k X$
22	19 20 21	nfov	$⊢ \underline{Ⅎ} n A (k) \cos k X$
23		nfcv	$⊢ \underline{Ⅎ} n +$
24		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
25	13 24	nfcxfr	$⊢ \underline{Ⅎ} n B$
26	25 18	nffv	$⊢ \underline{Ⅎ} n B (k)$
27		nfcv	$⊢ \underline{Ⅎ} n \sin k X$
28	26 20 27	nfov	$⊢ \underline{Ⅎ} n B (k) \sin k X$
29	22 23 28	nfov	$⊢ \underline{Ⅎ} n (A (k) \cos k X + B (k) \sin k X)$
30		fveq2	$⊢ n = k \to A (n) = A (k)$
31		oveq1	$⊢ n = k \to n X = k X$
32	31	fveq2d	$⊢ n = k \to \cos n X = \cos k X$
33	30 32	oveq12d	$⊢ n = k \to A (n) \cos n X = A (k) \cos k X$
34		fveq2	$⊢ n = k \to B (n) = B (k)$
35	31	fveq2d	$⊢ n = k \to \sin n X = \sin k X$
36	34 35	oveq12d	$⊢ n = k \to B (n) \sin n X = B (k) \sin k X$
37	33 36	oveq12d	$⊢ n = k \to A (n) \cos n X + B (n) \sin n X = A (k) \cos k X + B (k) \sin k X$
38	15 29 37	cbvmpt	$⊢ (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X) = (k \in ℕ ⟼ A (k) \cos k X + B (k) \sin k X)$
39	14 38	eqtri	$⊢ S = (k \in ℕ ⟼ A (k) \cos k X + B (k) \sin k X)$
40	1 2 3 4 5 6 7 8 9 10 11 12 13 39	fourierdlem115	$⊢ φ \to (seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2})) \land (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{L + R}{2})$
41	40	simpld	$⊢ φ \to seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2}))$

Metamath Proof Explorer

Theorem fourierclimd

Proof