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	\|- ( ph -> F : RR --> RR )
	fouriercn.t	\|- T = ( 2 x. _pi )
	fouriercn.per	\|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
	fouriercn.dv	\|- ( ph -> ( RR _D F ) e. ( RR -cn-> CC ) )
	fouriercn.g	\|- G = ( ( RR _D F ) \|` ( -u _pi (,) _pi ) )
	fouriercn.x	\|- ( ph -> X e. RR )
	fouriercn.a	\|- A = ( n e. NN0 \|-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
	fouriercn.b	\|- B = ( n e. NN \|-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
Assertion	fouriercn	\|- ( ph -> ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( F ` X ) )

Proof

Step	Hyp	Ref	Expression
1		fouriercn.f	\|- ( ph -> F : RR --> RR )
2		fouriercn.t	\|- T = ( 2 x. _pi )
3		fouriercn.per	\|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4		fouriercn.dv	\|- ( ph -> ( RR _D F ) e. ( RR -cn-> CC ) )
5		fouriercn.g	\|- G = ( ( RR _D F ) \|` ( -u _pi (,) _pi ) )
6		fouriercn.x	\|- ( ph -> X e. RR )
7		fouriercn.a	\|- A = ( n e. NN0 \|-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
8		fouriercn.b	\|- B = ( n e. NN \|-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
9	5	dmeqi	\|- dom G = dom ( ( RR _D F ) \|` ( -u _pi (,) _pi ) )
10		ioossre	\|- ( -u _pi (,) _pi ) C_ RR
11		cncff	\|- ( ( RR _D F ) e. ( RR -cn-> CC ) -> ( RR _D F ) : RR --> CC )
12		fdm	\|- ( ( RR _D F ) : RR --> CC -> dom ( RR _D F ) = RR )
13	4 11 12	3syl	\|- ( ph -> dom ( RR _D F ) = RR )
14	10 13	sseqtrrid	\|- ( ph -> ( -u _pi (,) _pi ) C_ dom ( RR _D F ) )
15		ssdmres	\|- ( ( -u _pi (,) _pi ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) \|` ( -u _pi (,) _pi ) ) = ( -u _pi (,) _pi ) )
16	14 15	sylib	\|- ( ph -> dom ( ( RR _D F ) \|` ( -u _pi (,) _pi ) ) = ( -u _pi (,) _pi ) )
17	9 16	syl5eq	\|- ( ph -> dom G = ( -u _pi (,) _pi ) )
18	17	difeq2d	\|- ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) = ( ( -u _pi (,) _pi ) \ ( -u _pi (,) _pi ) ) )
19		difid	\|- ( ( -u _pi (,) _pi ) \ ( -u _pi (,) _pi ) ) = (/)
20	18 19	eqtrdi	\|- ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) = (/) )
21		0fin	\|- (/) e. Fin
22	20 21	eqeltrdi	\|- ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
23		rescncf	\|- ( ( -u _pi (,) _pi ) C_ RR -> ( ( RR _D F ) e. ( RR -cn-> CC ) -> ( ( RR _D F ) \|` ( -u _pi (,) _pi ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) ) )
24	10 4 23	mpsyl	\|- ( ph -> ( ( RR _D F ) \|` ( -u _pi (,) _pi ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
25	5	a1i	\|- ( ph -> G = ( ( RR _D F ) \|` ( -u _pi (,) _pi ) ) )
26	17	oveq1d	\|- ( ph -> ( dom G -cn-> CC ) = ( ( -u _pi (,) _pi ) -cn-> CC ) )
27	24 25 26	3eltr4d	\|- ( ph -> G e. ( dom G -cn-> CC ) )
28		pire	\|- _pi e. RR
29	28	renegcli	\|- -u _pi e. RR
30	28	rexri	\|- _pi e. RR*
31		icossre	\|- ( ( -u _pi e. RR /\ _pi e. RR* ) -> ( -u _pi [,) _pi ) C_ RR )
32	29 30 31	mp2an	\|- ( -u _pi [,) _pi ) C_ RR
33		eldifi	\|- ( x e. ( ( -u _pi [,) _pi ) \ dom G ) -> x e. ( -u _pi [,) _pi ) )
34	32 33	sseldi	\|- ( x e. ( ( -u _pi [,) _pi ) \ dom G ) -> x e. RR )
35		limcresi	\|- ( ( RR _D F ) limCC x ) C_ ( ( ( RR _D F ) \|` ( ( -u _pi (,) _pi ) i^i ( x (,) +oo ) ) ) limCC x )
36	5	reseq1i	\|- ( G \|` ( x (,) +oo ) ) = ( ( ( RR _D F ) \|` ( -u _pi (,) _pi ) ) \|` ( x (,) +oo ) )
37		resres	\|- ( ( ( RR _D F ) \|` ( -u _pi (,) _pi ) ) \|` ( x (,) +oo ) ) = ( ( RR _D F ) \|` ( ( -u _pi (,) _pi ) i^i ( x (,) +oo ) ) )
38	36 37	eqtr2i	\|- ( ( RR _D F ) \|` ( ( -u _pi (,) _pi ) i^i ( x (,) +oo ) ) ) = ( G \|` ( x (,) +oo ) )
39	38	oveq1i	\|- ( ( ( RR _D F ) \|` ( ( -u _pi (,) _pi ) i^i ( x (,) +oo ) ) ) limCC x ) = ( ( G \|` ( x (,) +oo ) ) limCC x )
40	35 39	sseqtri	\|- ( ( RR _D F ) limCC x ) C_ ( ( G \|` ( x (,) +oo ) ) limCC x )
41	4	adantr	\|- ( ( ph /\ x e. RR ) -> ( RR _D F ) e. ( RR -cn-> CC ) )
42		simpr	\|- ( ( ph /\ x e. RR ) -> x e. RR )
43	41 42	cnlimci	\|- ( ( ph /\ x e. RR ) -> ( ( RR _D F ) ` x ) e. ( ( RR _D F ) limCC x ) )
44	40 43	sseldi	\|- ( ( ph /\ x e. RR ) -> ( ( RR _D F ) ` x ) e. ( ( G \|` ( x (,) +oo ) ) limCC x ) )
45	44	ne0d	\|- ( ( ph /\ x e. RR ) -> ( ( G \|` ( x (,) +oo ) ) limCC x ) =/= (/) )
46	34 45	sylan2	\|- ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G \|` ( x (,) +oo ) ) limCC x ) =/= (/) )
47		negpitopissre	\|- ( -u _pi (,] _pi ) C_ RR
48		eldifi	\|- ( x e. ( ( -u _pi (,] _pi ) \ dom G ) -> x e. ( -u _pi (,] _pi ) )
49	47 48	sseldi	\|- ( x e. ( ( -u _pi (,] _pi ) \ dom G ) -> x e. RR )
50		limcresi	\|- ( ( RR _D F ) limCC x ) C_ ( ( ( RR _D F ) \|` ( ( -u _pi (,) _pi ) i^i ( -oo (,) x ) ) ) limCC x )
51	5	reseq1i	\|- ( G \|` ( -oo (,) x ) ) = ( ( ( RR _D F ) \|` ( -u _pi (,) _pi ) ) \|` ( -oo (,) x ) )
52		resres	\|- ( ( ( RR _D F ) \|` ( -u _pi (,) _pi ) ) \|` ( -oo (,) x ) ) = ( ( RR _D F ) \|` ( ( -u _pi (,) _pi ) i^i ( -oo (,) x ) ) )
53	51 52	eqtr2i	\|- ( ( RR _D F ) \|` ( ( -u _pi (,) _pi ) i^i ( -oo (,) x ) ) ) = ( G \|` ( -oo (,) x ) )
54	53	oveq1i	\|- ( ( ( RR _D F ) \|` ( ( -u _pi (,) _pi ) i^i ( -oo (,) x ) ) ) limCC x ) = ( ( G \|` ( -oo (,) x ) ) limCC x )
55	50 54	sseqtri	\|- ( ( RR _D F ) limCC x ) C_ ( ( G \|` ( -oo (,) x ) ) limCC x )
56	55 43	sseldi	\|- ( ( ph /\ x e. RR ) -> ( ( RR _D F ) ` x ) e. ( ( G \|` ( -oo (,) x ) ) limCC x ) )
57	56	ne0d	\|- ( ( ph /\ x e. RR ) -> ( ( G \|` ( -oo (,) x ) ) limCC x ) =/= (/) )
58	49 57	sylan2	\|- ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G \|` ( -oo (,) x ) ) limCC x ) =/= (/) )
59		eqid	\|- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
60		ax-resscn	\|- RR C_ CC
61	60	a1i	\|- ( ph -> RR C_ CC )
62	1 61	fssd	\|- ( ph -> F : RR --> CC )
63		ssid	\|- RR C_ RR
64	63	a1i	\|- ( ph -> RR C_ RR )
65		dvcn	\|- ( ( ( RR C_ CC /\ F : RR --> CC /\ RR C_ RR ) /\ dom ( RR _D F ) = RR ) -> F e. ( RR -cn-> CC ) )
66	61 62 64 13 65	syl31anc	\|- ( ph -> F e. ( RR -cn-> CC ) )
67		cncffvrn	\|- ( ( RR C_ CC /\ F e. ( RR -cn-> CC ) ) -> ( F e. ( RR -cn-> RR ) <-> F : RR --> RR ) )
68	61 66 67	syl2anc	\|- ( ph -> ( F e. ( RR -cn-> RR ) <-> F : RR --> RR ) )
69	1 68	mpbird	\|- ( ph -> F e. ( RR -cn-> RR ) )
70		eqid	\|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
71	70	tgioo2	\|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) \|`t RR )
72	70 71 71	cncfcn	\|- ( ( RR C_ CC /\ RR C_ CC ) -> ( RR -cn-> RR ) = ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
73	61 61 72	syl2anc	\|- ( ph -> ( RR -cn-> RR ) = ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
74	69 73	eleqtrd	\|- ( ph -> F e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
75		uniretop	\|- RR = U. ( topGen ` ran (,) )
76	75	cncnpi	\|- ( ( F e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) /\ X e. RR ) -> F e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` X ) )
77	74 6 76	syl2anc	\|- ( ph -> F e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` X ) )
78	1 2 3 5 22 27 46 58 59 77 7 8	fouriercnp	\|- ( ph -> ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( F ` X ) )

Metamath Proof Explorer

Theorem fouriercn

Proof