fourierdlem115

Description: Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem115.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem115.t	$⊢ T = 2 π$
3		fourierdlem115.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
4		fourierdlem115.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
5		fourierdlem115.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
6		fourierdlem115.dvcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
7		fourierdlem115.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
8		fourierdlem115.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
9		fourierdlem115.x	$⊢ φ \to X \in ℝ$
10		fourierdlem115.l	$⊢ φ \to L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
11		fourierdlem115.r	$⊢ φ \to R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
12		fourierdlem115.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
13		fourierdlem115.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
14		fourierdlem115.s	$⊢ S = (k \in ℕ ⟼ A (k) \cos k X + B (k) \sin k X)$
15		oveq1	$⊢ n = k \to n x = k x$
16	15	fveq2d	$⊢ n = k \to \cos n x = \cos k x$
17	16	oveq2d	$⊢ n = k \to F (x) \cos n x = F (x) \cos k x$
18	17	adantr	$⊢ (n = k \land x \in (- π, π)) \to F (x) \cos n x = F (x) \cos k x$
19	18	itgeq2dv	$⊢ n = k \to \int_{(- π, π)} F (x) \cos n x d x = \int_{(- π, π)} F (x) \cos k x d x$
20	19	oveq1d	$⊢ n = k \to \frac{\int_{(- π, π)} F (x) \cos n x d x}{π} = \frac{\int_{(- π, π)} F (x) \cos k x d x}{π}$
21	20	cbvmptv	$⊢ (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π}) = (k \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos k x d x}{π})$
22	12 21	eqtri	$⊢ A = (k \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos k x d x}{π})$
23	15	fveq2d	$⊢ n = k \to \sin n x = \sin k x$
24	23	oveq2d	$⊢ n = k \to F (x) \sin n x = F (x) \sin k x$
25	24	adantr	$⊢ (n = k \land x \in (- π, π)) \to F (x) \sin n x = F (x) \sin k x$
26	25	itgeq2dv	$⊢ n = k \to \int_{(- π, π)} F (x) \sin n x d x = \int_{(- π, π)} F (x) \sin k x d x$
27	26	oveq1d	$⊢ n = k \to \frac{\int_{(- π, π)} F (x) \sin n x d x}{π} = \frac{\int_{(- π, π)} F (x) \sin k x d x}{π}$
28	27	cbvmptv	$⊢ (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π}) = (k \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin k x d x}{π})$
29	13 28	eqtri	$⊢ B = (k \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin k x d x}{π})$
30		eqid	$⊢ (k \in ℕ ⟼ \{w \in (ℝ^{(0 \dots k)}) \| ((w (0) = - π \land w (k) = π) \land \forall z \in (0 ..^k) w (z) < w (z + 1))\}) = (k \in ℕ ⟼ \{w \in (ℝ^{(0 \dots k)}) \| ((w (0) = - π \land w (k) = π) \land \forall z \in (0 ..^k) w (z) < w (z + 1))\})$
31		id	$⊢ y = x \to y = x$
32		oveq2	$⊢ y = x \to π - y = π - x$
33	32	oveq1d	$⊢ y = x \to \frac{π - y}{T} = \frac{π - x}{T}$
34	33	fveq2d	$⊢ y = x \to ⌊\frac{π - y}{T}⌋ = ⌊\frac{π - x}{T}⌋$
35	34	oveq1d	$⊢ y = x \to ⌊\frac{π - y}{T}⌋ T = ⌊\frac{π - x}{T}⌋ T$
36	31 35	oveq12d	$⊢ y = x \to y + ⌊\frac{π - y}{T}⌋ T = x + ⌊\frac{π - x}{T}⌋ T$
37	36	cbvmptv	$⊢ (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) = (x \in ℝ ⟼ x + ⌊\frac{π - x}{T}⌋ T)$
38		eqid	$⊢ \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G) = \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)$
39		eqid	$⊢ \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1 = \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1$
40		isoeq1	$⊢ g = f \to (g {Isom}_{<, <} ((0 \dots \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1), \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1), \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)))$
41	40	cbviotavw	$⊢ (ι g \| g {Isom}_{<, <} ((0 \dots \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1), \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G))) = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)\| - 1), \{- π, π, (y \in ℝ ⟼ y + ⌊\frac{π - y}{T}⌋ T) (X)\} \cup ([- π, π] ∖ dom G)))$
42	1 2 3 4 5 6 7 8 9 10 11 22 29 14 30 37 38 39 41	fourierdlem114	$⊢ φ \to (seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2})) \land (\frac{A (0)}{2}) + \sum_{k \in ℕ} (A (k) \cos k X + B (k) \sin k X) = \frac{L + R}{2})$
43	42	simpld	$⊢ φ \to seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2}))$
44		fveq2	$⊢ n = k \to A (n) = A (k)$
45		oveq1	$⊢ n = k \to n X = k X$
46	45	fveq2d	$⊢ n = k \to \cos n X = \cos k X$
47	44 46	oveq12d	$⊢ n = k \to A (n) \cos n X = A (k) \cos k X$
48		fveq2	$⊢ n = k \to B (n) = B (k)$
49	45	fveq2d	$⊢ n = k \to \sin n X = \sin k X$
50	48 49	oveq12d	$⊢ n = k \to B (n) \sin n X = B (k) \sin k X$
51	47 50	oveq12d	$⊢ n = k \to A (n) \cos n X + B (n) \sin n X = A (k) \cos k X + B (k) \sin k X$
52		nfcv	$⊢ \underline{Ⅎ} k (A (n) \cos n X + B (n) \sin n X)$
53		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
54	12 53	nfcxfr	$⊢ \underline{Ⅎ} n A$
55		nfcv	$⊢ \underline{Ⅎ} n k$
56	54 55	nffv	$⊢ \underline{Ⅎ} n A (k)$
57		nfcv	$⊢ \underline{Ⅎ} n \times$
58		nfcv	$⊢ \underline{Ⅎ} n \cos k X$
59	56 57 58	nfov	$⊢ \underline{Ⅎ} n A (k) \cos k X$
60		nfcv	$⊢ \underline{Ⅎ} n +$
61		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
62	13 61	nfcxfr	$⊢ \underline{Ⅎ} n B$
63	62 55	nffv	$⊢ \underline{Ⅎ} n B (k)$
64		nfcv	$⊢ \underline{Ⅎ} n \sin k X$
65	63 57 64	nfov	$⊢ \underline{Ⅎ} n B (k) \sin k X$
66	59 60 65	nfov	$⊢ \underline{Ⅎ} n (A (k) \cos k X + B (k) \sin k X)$
67	51 52 66	cbvsum	$⊢ \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \sum_{k \in ℕ} (A (k) \cos k X + B (k) \sin k X)$
68	67	oveq2i	$⊢ (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = (\frac{A (0)}{2}) + \sum_{k \in ℕ} (A (k) \cos k X + B (k) \sin k X)$
69	42	simprd	$⊢ φ \to (\frac{A (0)}{2}) + \sum_{k \in ℕ} (A (k) \cos k X + B (k) \sin k X) = \frac{L + R}{2}$
70	68 69	eqtrid	$⊢ φ \to (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{L + R}{2}$
71	43 70	jca	$⊢ φ \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})$

Metamath Proof Explorer

Theorem fourierdlem115

Proof