fourierd - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fourierd		Structured version Visualization version GIF version

Theorem fourierd 47505

Description: Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 47509. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 47510 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 47515. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierd.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierd.t	⊢ 𝑇 = (2 · π)
fourierd.per	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
fourierd.g	⊢ 𝐺 = ((ℝ D 𝐹) ↾ ( -π(,)π))
fourierd.dmdv	⊢ (𝜑 → (( -π(,)π) ∖ dom 𝐺) ∈ Fin)
fourierd.dvcn	⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
fourierd.rlim	⊢ ((𝜑 ∧ 𝑥 ∈ (( -π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
fourierd.llim	⊢ ((𝜑 ∧ 𝑥 ∈ (( -π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
fourierd.x	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierd.l	⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
fourierd.r	⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
fourierd.a	⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
fourierd.b	⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))

**Assertion**
Ref	Expression
fourierd	⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))

Distinct variable groups: 𝑛,𝐹,𝑥 𝑥,𝐺 𝑥,𝑇 𝑛,𝑋,𝑥 𝜑,𝑥 Allowed substitution hints: 𝜑(𝑛) 𝐴(𝑥, 𝑛) 𝐵(𝑥, 𝑛) 𝑅(𝑥, 𝑛) 𝑇(𝑛) 𝐺(𝑛) 𝐿(𝑥, 𝑛)

Proof of Theorem fourierd Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierd.f	. . 3 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
2		fourierd.t	. . 3 ⊢ 𝑇 = (2 · π)
3		fourierd.per	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
4		fourierd.g	. . 3 ⊢ 𝐺 = ((ℝ D 𝐹) ↾ ( -π(,)π))
5		fourierd.dmdv	. . 3 ⊢ (𝜑 → (( -π(,)π) ∖ dom 𝐺) ∈ Fin)
6		fourierd.dvcn	. . 3 ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
7		fourierd.rlim	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (( -π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
8		fourierd.llim	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (( -π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
9		fourierd.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ ℝ)
10		fourierd.l	. . 3 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
11		fourierd.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
12		fourierd.a	. . 3 ⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
13		fourierd.b	. . 3 ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
14		nfcv 2926	. . . 4 ⊢ Ⅎ𝑘(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))
15		nfmpt1 5210	. . . . . . . 8 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ₀ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
16	12, 15	nfcxfr 2924	. . . . . . 7 ⊢ Ⅎ𝑛𝐴
17		nfcv 2926	. . . . . . 7 ⊢ Ⅎ𝑛𝑘
18	16, 17	nffv 6926	. . . . . 6 ⊢ Ⅎ𝑛(𝐴‘𝑘)
19		nfcv 2926	. . . . . 6 ⊢ Ⅎ𝑛 ·
20		nfcv 2926	. . . . . 6 ⊢ Ⅎ𝑛(cos‘(𝑘 · 𝑋))
21	18, 19, 20	nfov 7481	. . . . 5 ⊢ Ⅎ𝑛((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋)))
22		nfcv 2926	. . . . 5 ⊢ Ⅎ𝑛 +
23		nfmpt1 5210	. . . . . . . 8 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ ↦ (∫( -π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
24	13, 23	nfcxfr 2924	. . . . . . 7 ⊢ Ⅎ𝑛𝐵
25	24, 17	nffv 6926	. . . . . 6 ⊢ Ⅎ𝑛(𝐵‘𝑘)
26		nfcv 2926	. . . . . 6 ⊢ Ⅎ𝑛(sin‘(𝑘 · 𝑋))
27	25, 19, 26	nfov 7481	. . . . 5 ⊢ Ⅎ𝑛((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))
28	21, 22, 27	nfov 7481	. . . 4 ⊢ Ⅎ𝑛(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
29		fveq2 6916	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
30		oveq1 7458	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛 · 𝑋) = (𝑘 · 𝑋))
31	30	fveq2d 6920	. . . . . 6 ⊢ (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑋)) = (cos‘(𝑘 · 𝑋)))
32	29, 31	oveq12d 7469	. . . . 5 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))))
33		fveq2 6916	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝐵‘𝑛) = (𝐵‘𝑘))
34	30	fveq2d 6920	. . . . . 6 ⊢ (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑋)) = (sin‘(𝑘 · 𝑋)))
35	33, 34	oveq12d 7469	. . . . 5 ⊢ (𝑛 = 𝑘 → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
36	32, 35	oveq12d 7469	. . . 4 ⊢ (𝑛 = 𝑘 → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
37	14, 28, 36	cbvmpt 5213	. . 3 ⊢ (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (𝑘 ∈ ℕ ↦ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
38	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 37	fourierdlem115 47504	. 2 ⊢ (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))
39	38	simprd 501	1 ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∖ cdif 4048 ∅c0 4281 class class class wbr 5108 ↦ cmpt 5192 dom cdm 5658 ↾ cres 5660 ⟶wf 6562 ‘cfv 6566 (class class class)co 7451 Fincfn 9011 ℂcc 11237 ℝcr 11238 0cc0 11239 1c1 11240 + caddc 11242 · cmul 11244 +∞cpnf 11379 -∞cmnf 11380 − cmin 11580 -cneg 11581 / cdiv 12013 ℕcn 12375 2c2 12437 ℕ₀cn0 12646 (,)cioo 13516 (,]cioc 13517 [,)cico 13518 seqcseq 14184 ⇝ cli 15695 Σcsu 15897 sincsin 16273 cosccos 16274 πcpi 16276 –cn→ccncf 25252 ∫citg 25994 lim_ℂ climc 26237 D cdv 26238

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-inf2 9679 ax-cc 10552 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317 ax-addf 11318

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-symdif 4201 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-disj 5076 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7725 df-ofr 7726 df-om 7912 df-1st 8035 df-2nd 8036 df-supp 8215 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-oadd 8518 df-omul 8519 df-er 8755 df-map 8887 df-pm 8888 df-ixp 8964 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fsupp 9392 df-fi 9440 df-sup 9471 df-inf 9472 df-oi 9541 df-dju 10019 df-card 10057 df-acn 10060 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-xnn0 12720 df-z 12734 df-dec 12855 df-uz 13006 df-q 13116 df-rp 13161 df-xneg 13281 df-xadd 13282 df-xmul 13283 df-ioo 13520 df-ioc 13521 df-ico 13522 df-icc 13523 df-fz 13680 df-fzo 13829 df-fl 13972 df-mod 14050 df-seq 14185 df-exp 14245 df-fac 14459 df-bc 14488 df-hash 14516 df-shft 15263 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-limsup 15682 df-clim 15699 df-rlim 15700 df-sum 15898 df-ef 16277 df-sin 16279 df-cos 16280 df-pi 16282 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-starv 17488 df-sca 17489 df-vsca 17490 df-ip 17491 df-tset 17492 df-ple 17493 df-ds 17495 df-unif 17496 df-hom 17497 df-cco 17498 df-euf 17499 df-rest 17643 df-topn 17644 df-0g 17662 df-gsum 17663 df-topgen 17664 df-pt 17665 df-prds 17668 df-xrs 17724 df-qtop 17729 df-imas 17730 df-xps 17732 df-mre 17806 df-mrc 17807 df-acs 17809 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-submnd 19029 df-mulg 19328 df-cntz 19582 df-cmn 20047 df-psmet 21721 df-xmet 21722 df-met 21723 df-bl 21724 df-mopn 21725 df-fbas 21726 df-fg 21727 df-cnfld 21730 df-top 23267 df-topon 23284 df-topsp 23306 df-bases 23319 df-cld 23392 df-ntr 23393 df-cls 23394 df-nei 23471 df-lp 23509 df-perf 23510 df-cn 23600 df-cnp 23601 df-t1 23687 df-haus 23688 df-cmp 23760 df-tx 23936 df-hmeo 24129 df-fil 24220 df-fm 24312 df-flim 24313 df-flf 24314 df-xms 24694 df-ms 24695 df-tms 24696 df-cncf 25254 df-ovol 25840 df-vol 25841 df-mbf 25995 df-itg1 25996 df-itg2 25997 df-ibl 25998 df-itg 25999 df-0p 26046 df-ditg 26222 df-limc 26241 df-dv 26242

This theorem is used by: fourier 47508 fouriercnp 47509 fourier2 47510

W3C validator