fouriercnp

Description: If F is continuous at the point X , then its Fourier series at X , converges to ( FX ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fouriercnp.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fouriercnp.t	$⊢ T = 2 π$
	fouriercnp.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fouriercnp.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
	fouriercnp.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
	fouriercnp.dvcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
	fouriercnp.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
	fouriercnp.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
	fouriercnp.j	$⊢ J = topGen (ran (.))$
	fouriercnp.cnp	$⊢ φ \to F \in (J CnP J) (X)$
	fouriercnp.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
	fouriercnp.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
Assertion	fouriercnp	$⊢ φ \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		fouriercnp.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fouriercnp.t	$⊢ T = 2 π$
3		fouriercnp.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
4		fouriercnp.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
5		fouriercnp.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
6		fouriercnp.dvcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
7		fouriercnp.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
8		fouriercnp.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
9		fouriercnp.j	$⊢ J = topGen (ran (.))$
10		fouriercnp.cnp	$⊢ φ \to F \in (J CnP J) (X)$
11		fouriercnp.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
12		fouriercnp.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
13		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
14	9	unieqi	$⊢ ⋃ J = ⋃ topGen (ran (.))$
15	13 14	eqtr4i	$⊢ ℝ = ⋃ J$
16	15	cnprcl	$⊢ F \in (J CnP J) (X) \to X \in ℝ$
17	10 16	syl	$⊢ φ \to X \in ℝ$
18		limcresi	$⊢ F {lim}_{ℂ} X \subseteq ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X$
19		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
20	9 19	eqtri	$⊢ J = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
21	20	oveq2i	$⊢ J CnP J = J CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
22	21	fveq1i	$⊢ (J CnP J) (X) = (J CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) (X)$
23	10 22	eleqtrdi	$⊢ φ \to F \in (J CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) (X)$
24		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
25	24	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
26	25	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Top$
27		ax-resscn	$⊢ ℝ \subseteq ℂ$
28	27	a1i	$⊢ φ \to ℝ \subseteq ℂ$
29		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
30	15 29	cnprest2	$⊢ (TopOpen (ℂ_{fld}) \in Top \land F : ℝ ⟶ ℝ \land ℝ \subseteq ℂ) \to (F \in (J CnP TopOpen (ℂ_{fld})) (X) \leftrightarrow F \in (J CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) (X))$
31	26 1 28 30	syl3anc	$⊢ φ \to (F \in (J CnP TopOpen (ℂ_{fld})) (X) \leftrightarrow F \in (J CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) (X))$
32	23 31	mpbird	$⊢ φ \to F \in (J CnP TopOpen (ℂ_{fld})) (X)$
33	24 20	cnplimc	$⊢ (ℝ \subseteq ℂ \land X \in ℝ) \to (F \in (J CnP TopOpen (ℂ_{fld})) (X) \leftrightarrow (F : ℝ ⟶ ℂ \land F (X) \in (F {lim}_{ℂ} X)))$
34	27 17 33	sylancr	$⊢ φ \to (F \in (J CnP TopOpen (ℂ_{fld})) (X) \leftrightarrow (F : ℝ ⟶ ℂ \land F (X) \in (F {lim}_{ℂ} X)))$
35	32 34	mpbid	$⊢ φ \to (F : ℝ ⟶ ℂ \land F (X) \in (F {lim}_{ℂ} X))$
36	35	simprd	$⊢ φ \to F (X) \in (F {lim}_{ℂ} X)$
37	18 36	sselid	$⊢ φ \to F (X) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
38		limcresi	$⊢ F {lim}_{ℂ} X \subseteq ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X$
39	38 36	sselid	$⊢ φ \to F (X) \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
40	1 2 3 4 5 6 7 8 17 37 39 11 12	fourierd	$⊢ φ \to (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{F (X) + F (X)}{2}$
41	1 17	ffvelcdmd	$⊢ φ \to F (X) \in ℝ$
42	41	recnd	$⊢ φ \to F (X) \in ℂ$
43	42	2timesd	$⊢ φ \to 2 F (X) = F (X) + F (X)$
44	43	eqcomd	$⊢ φ \to F (X) + F (X) = 2 F (X)$
45	44	oveq1d	$⊢ φ \to \frac{F (X) + F (X)}{2} = \frac{2 F (X)}{2}$
46		2cnd	$⊢ φ \to 2 \in ℂ$
47		2ne0	$⊢ 2 \neq 0$
48	47	a1i	$⊢ φ \to 2 \neq 0$
49	42 46 48	divcan3d	$⊢ φ \to \frac{2 F (X)}{2} = F (X)$
50	40 45 49	3eqtrd	$⊢ φ \to (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = F (X)$

Metamath Proof Explorer

Theorem fouriercnp

Proof