fourier2

Description: Fourier series convergence, for a piecewise smooth function. Here it is also proven the existence of the left and right limits of F at any given point X . See fourierd for a comparison. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourier2.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourier2.t	$⊢ T = 2 π$
	fourier2.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourier2.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
	fourier2.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
	fourier2.dvcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
	fourier2.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
	fourier2.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
	fourier2.x	$⊢ φ \to X \in ℝ$
	fourier2.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
	fourier2.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
Assertion	fourier2	$⊢ φ \to \exists l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X) \exists r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) (\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		fourier2.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourier2.t	$⊢ T = 2 π$
3		fourier2.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
4		fourier2.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
5		fourier2.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
6		fourier2.dvcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
7		fourier2.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
8		fourier2.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
9		fourier2.x	$⊢ φ \to X \in ℝ$
10		fourier2.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
11		fourier2.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
12	1 2 3 4 5 6 7 8 9	fourierdlem106	$⊢ φ \to (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X \neq \emptyset \land ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset)$
13	12	simpld	$⊢ φ \to ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X \neq \emptyset$
14		n0	$⊢ ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X \neq \emptyset \leftrightarrow \exists l l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
15	13 14	sylib	$⊢ φ \to \exists l l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
16		simpr	$⊢ (φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \to l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
17	12	simprd	$⊢ φ \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$
18		n0	$⊢ ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset \leftrightarrow \exists r r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
19	17 18	sylib	$⊢ φ \to \exists r r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
20	19	adantr	$⊢ (φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \to \exists r r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
21		simpr	$⊢ ((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \to r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
22	1	ad2antrr	$⊢ ((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \to F : ℝ ⟶ ℝ$
23	3	ad4ant14	$⊢ (((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \land x \in ℝ) \to F (x + T) = F (x)$
24	5	ad2antrr	$⊢ ((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \to (- π, π) ∖ dom G \in Fin$
25	6	ad2antrr	$⊢ ((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \to G : dom G \underset{cn}{⟶} ℂ$
26	7	ad4ant14	$⊢ (((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
27	8	ad4ant14	$⊢ (((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
28	9	ad2antrr	$⊢ ((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \to X \in ℝ$
29	16	adantr	$⊢ ((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \to l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
30	22 2 23 4 24 25 26 27 28 29 21 10 11	fourierd	$⊢ ((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \to (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2}$
31	21 30	jca	$⊢ ((φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \land r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \to (r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) \land (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2})$
32	31	ex	$⊢ (φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \to (r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) \to (r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) \land (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2}))$
33	32	eximdv	$⊢ (φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \to (\exists r r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) \to \exists r (r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) \land (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2}))$
34	20 33	mpd	$⊢ (φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \to \exists r (r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) \land (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2})$
35		df-rex	$⊢ \exists r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2} \leftrightarrow \exists r (r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) \land (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2})$
36	34 35	sylibr	$⊢ (φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \to \exists r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2}$
37	16 36	jca	$⊢ (φ \land l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \to (l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X) \land \exists r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2})$
38	37	ex	$⊢ φ \to (l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X) \to (l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X) \land \exists r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2}))$
39	38	eximdv	$⊢ φ \to (\exists l l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X) \to \exists l (l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X) \land \exists r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2}))$
40	15 39	mpd	$⊢ φ \to \exists l (l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X) \land \exists r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2})$
41		df-rex	$⊢ \exists l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X) \exists r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2} \leftrightarrow \exists l (l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X) \land \exists r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{l + r}{2})$
42	40 41	sylibr	$⊢ φ \to \exists l \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X) \exists r \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X) (\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 fourier2

Proof