fouriercn

Description: If the derivative of F is continuous, then the Fourier series for F converges to F everywhere and the hypothesis are simpler than those for the more general case of a piecewise smooth function (see fourierd for a comparison). (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fouriercn.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fouriercn.t	$⊢ T = 2 π$
	fouriercn.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fouriercn.dv	$⊢ φ \to F_{ℝ}^{'} : ℝ \underset{cn}{⟶} ℂ$
	fouriercn.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
	fouriercn.x	$⊢ φ \to X \in ℝ$
	fouriercn.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
	fouriercn.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
Assertion	fouriercn	$⊢ φ \to (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = F (X)$

Proof

Step	Hyp	Ref	Expression
1		fouriercn.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fouriercn.t	$⊢ T = 2 π$
3		fouriercn.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
4		fouriercn.dv	$⊢ φ \to F_{ℝ}^{'} : ℝ \underset{cn}{⟶} ℂ$
5		fouriercn.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
6		fouriercn.x	$⊢ φ \to X \in ℝ$
7		fouriercn.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
8		fouriercn.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
9	5	dmeqi	$⊢ dom G = dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
10		ioossre	$⊢ (- π, π) \subseteq ℝ$
11		cncff	$⊢ F_{ℝ}^{'} : ℝ \underset{cn}{⟶} ℂ \to F_{ℝ}^{'} : ℝ ⟶ ℂ$
12		fdm	$⊢ F_{ℝ}^{'} : ℝ ⟶ ℂ \to dom F_{ℝ}^{'} = ℝ$
13	4 11 12	3syl	$⊢ φ \to dom F_{ℝ}^{'} = ℝ$
14	10 13	sseqtrrid	$⊢ φ \to (- π, π) \subseteq dom F_{ℝ}^{'}$
15		ssdmres	$⊢ (- π, π) \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) = (- π, π)$
16	14 15	sylib	$⊢ φ \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) = (- π, π)$
17	9 16	syl5eq	$⊢ φ \to dom G = (- π, π)$
18	17	difeq2d	$⊢ φ \to (- π, π) ∖ dom G = (- π, π) ∖ (- π, π)$
19		difid	$⊢ (- π, π) ∖ (- π, π) = \emptyset$
20	18 19	eqtrdi	$⊢ φ \to (- π, π) ∖ dom G = \emptyset$
21		0fin	$⊢ \emptyset \in Fin$
22	20 21	eqeltrdi	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
23		rescncf	$⊢ (- π, π) \subseteq ℝ \to (F_{ℝ}^{'} : ℝ \underset{cn}{⟶} ℂ \to ({F_{ℝ}^{'} ↾}_{(- π, π)}) : (- π, π) \underset{cn}{⟶} ℂ)$
24	10 4 23	mpsyl	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{(- π, π)}) : (- π, π) \underset{cn}{⟶} ℂ$
25	5	a1i	$⊢ φ \to G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
26	17	oveq1d	$⊢ φ \to dom G \underset{cn}{⟶} ℂ = (- π, π) \underset{cn}{⟶} ℂ$
27	24 25 26	3eltr4d	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
28		pire	$⊢ π \in ℝ$
29	28	renegcli	$⊢ - π \in ℝ$
30	28	rexri	$⊢ π \in ℝ^{*}$
31		icossre	$⊢ (- π \in ℝ \land π \in ℝ^{*}) \to [- π, π) \subseteq ℝ$
32	29 30 31	mp2an	$⊢ [- π, π) \subseteq ℝ$
33		eldifi	$⊢ x \in ([- π, π) ∖ dom G) \to x \in [- π, π)$
34	32 33	sseldi	$⊢ x \in ([- π, π) ∖ dom G) \to x \in ℝ$
35		limcresi	$⊢ F_{ℝ}^{'} {lim}_{ℂ} x \subseteq ({F_{ℝ}^{'} ↾}_{((- π, π) \cap (x, +∞))}) {lim}_{ℂ} x$
36	5	reseq1i	$⊢ {G ↾}_{(x, +∞)} = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)}$
37		resres	$⊢ {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)} = {F_{ℝ}^{'} ↾}_{((- π, π) \cap (x, +∞))}$
38	36 37	eqtr2i	$⊢ {F_{ℝ}^{'} ↾}_{((- π, π) \cap (x, +∞))} = {G ↾}_{(x, +∞)}$
39	38	oveq1i	$⊢ ({F_{ℝ}^{'} ↾}_{((- π, π) \cap (x, +∞))}) {lim}_{ℂ} x = ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x$
40	35 39	sseqtri	$⊢ F_{ℝ}^{'} {lim}_{ℂ} x \subseteq ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x$
41	4	adantr	$⊢ (φ \land x \in ℝ) \to F_{ℝ}^{'} : ℝ \underset{cn}{⟶} ℂ$
42		simpr	$⊢ (φ \land x \in ℝ) \to x \in ℝ$
43	41 42	cnlimci	$⊢ (φ \land x \in ℝ) \to F_{ℝ}^{'} (x) \in (F_{ℝ}^{'} {lim}_{ℂ} x)$
44	40 43	sseldi	$⊢ (φ \land x \in ℝ) \to F_{ℝ}^{'} (x) \in (({G ↾}_{(x, +∞)}) {lim}_{ℂ} x)$
45	44	ne0d	$⊢ (φ \land x \in ℝ) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
46	34 45	sylan2	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
47		negpitopissre	$⊢ (- π, π] \subseteq ℝ$
48		eldifi	$⊢ x \in ((- π, π] ∖ dom G) \to x \in (- π, π]$
49	47 48	sseldi	$⊢ x \in ((- π, π] ∖ dom G) \to x \in ℝ$
50		limcresi	$⊢ F_{ℝ}^{'} {lim}_{ℂ} x \subseteq ({F_{ℝ}^{'} ↾}_{((- π, π) \cap (−∞, x))}) {lim}_{ℂ} x$
51	5	reseq1i	$⊢ {G ↾}_{(−∞, x)} = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)}$
52		resres	$⊢ {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)} = {F_{ℝ}^{'} ↾}_{((- π, π) \cap (−∞, x))}$
53	51 52	eqtr2i	$⊢ {F_{ℝ}^{'} ↾}_{((- π, π) \cap (−∞, x))} = {G ↾}_{(−∞, x)}$
54	53	oveq1i	$⊢ ({F_{ℝ}^{'} ↾}_{((- π, π) \cap (−∞, x))}) {lim}_{ℂ} x = ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x$
55	50 54	sseqtri	$⊢ F_{ℝ}^{'} {lim}_{ℂ} x \subseteq ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x$
56	55 43	sseldi	$⊢ (φ \land x \in ℝ) \to F_{ℝ}^{'} (x) \in (({G ↾}_{(−∞, x)}) {lim}_{ℂ} x)$
57	56	ne0d	$⊢ (φ \land x \in ℝ) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
58	49 57	sylan2	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
59		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
60		ax-resscn	$⊢ ℝ \subseteq ℂ$
61	60	a1i	$⊢ φ \to ℝ \subseteq ℂ$
62	1 61	fssd	$⊢ φ \to F : ℝ ⟶ ℂ$
63		ssid	$⊢ ℝ \subseteq ℝ$
64	63	a1i	$⊢ φ \to ℝ \subseteq ℝ$
65		dvcn	$⊢ ((ℝ \subseteq ℂ \land F : ℝ ⟶ ℂ \land ℝ \subseteq ℝ) \land dom F_{ℝ}^{'} = ℝ) \to F : ℝ \underset{cn}{⟶} ℂ$
66	61 62 64 13 65	syl31anc	$⊢ φ \to F : ℝ \underset{cn}{⟶} ℂ$
67		cncffvrn	$⊢ (ℝ \subseteq ℂ \land F : ℝ \underset{cn}{⟶} ℂ) \to (F : ℝ \underset{cn}{⟶} ℝ \leftrightarrow F : ℝ ⟶ ℝ)$
68	61 66 67	syl2anc	$⊢ φ \to (F : ℝ \underset{cn}{⟶} ℝ \leftrightarrow F : ℝ ⟶ ℝ)$
69	1 68	mpbird	$⊢ φ \to F : ℝ \underset{cn}{⟶} ℝ$
70		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
71	70	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
72	70 71 71	cncfcn	$⊢ (ℝ \subseteq ℂ \land ℝ \subseteq ℂ) \to ℝ \underset{cn}{⟶} ℝ = topGen (ran (.)) Cn topGen (ran (.))$
73	61 61 72	syl2anc	$⊢ φ \to ℝ \underset{cn}{⟶} ℝ = topGen (ran (.)) Cn topGen (ran (.))$
74	69 73	eleqtrd	$⊢ φ \to F \in (topGen (ran (.)) Cn topGen (ran (.)))$
75		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
76	75	cncnpi	$⊢ (F \in (topGen (ran (.)) Cn topGen (ran (.))) \land X \in ℝ) \to F \in (topGen (ran (.)) CnP topGen (ran (.))) (X)$
77	74 6 76	syl2anc	$⊢ φ \to F \in (topGen (ran (.)) CnP topGen (ran (.))) (X)$
78	1 2 3 5 22 27 46 58 59 77 7 8	fouriercnp	$⊢ φ \to (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = F (X)$

Metamath Proof Explorer

Theorem fouriercn

Proof