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 43717

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 43721. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 43722 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 43727. (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 2908	. . . 4 ⊢ Ⅎ𝑘(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))
15		nfmpt1 5186	. . . . . . . 8 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ₀ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
16	12, 15	nfcxfr 2906	. . . . . . 7 ⊢ Ⅎ𝑛𝐴
17		nfcv 2908	. . . . . . 7 ⊢ Ⅎ𝑛𝑘
18	16, 17	nffv 6778	. . . . . 6 ⊢ Ⅎ𝑛(𝐴‘𝑘)
19		nfcv 2908	. . . . . 6 ⊢ Ⅎ𝑛 ·
20		nfcv 2908	. . . . . 6 ⊢ Ⅎ𝑛(cos‘(𝑘 · 𝑋))
21	18, 19, 20	nfov 7298	. . . . 5 ⊢ Ⅎ𝑛((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋)))
22		nfcv 2908	. . . . 5 ⊢ Ⅎ𝑛 +
23		nfmpt1 5186	. . . . . . . 8 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
24	13, 23	nfcxfr 2906	. . . . . . 7 ⊢ Ⅎ𝑛𝐵
25	24, 17	nffv 6778	. . . . . 6 ⊢ Ⅎ𝑛(𝐵‘𝑘)
26		nfcv 2908	. . . . . 6 ⊢ Ⅎ𝑛(sin‘(𝑘 · 𝑋))
27	25, 19, 26	nfov 7298	. . . . 5 ⊢ Ⅎ𝑛((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))
28	21, 22, 27	nfov 7298	. . . 4 ⊢ Ⅎ𝑛(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
29		fveq2 6768	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
30		oveq1 7275	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛 · 𝑋) = (𝑘 · 𝑋))
31	30	fveq2d 6772	. . . . . 6 ⊢ (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑋)) = (cos‘(𝑘 · 𝑋)))
32	29, 31	oveq12d 7286	. . . . 5 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))))
33		fveq2 6768	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝐵‘𝑛) = (𝐵‘𝑘))
34	30	fveq2d 6772	. . . . . 6 ⊢ (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑋)) = (sin‘(𝑘 · 𝑋)))
35	33, 34	oveq12d 7286	. . . . 5 ⊢ (𝑛 = 𝑘 → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
36	32, 35	oveq12d 7286	. . . 4 ⊢ (𝑛 = 𝑘 → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
37	14, 28, 36	cbvmpt 5189	. . 3 ⊢ (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (𝑘 ∈ ℕ ↦ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
38	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 37	fourierdlem115 43716	. 2 ⊢ (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))
39	38	simprd 495	1 ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2109 ≠ wne 2944 ∖ cdif 3888 ∅c0 4261 class class class wbr 5078 ↦ cmpt 5161 dom cdm 5588 ↾ cres 5590 ⟶wf 6426 ‘cfv 6430 (class class class)co 7268 Fincfn 8707 ℂcc 10853 ℝcr 10854 0cc0 10855 1c1 10856 + caddc 10858 · cmul 10860 +∞cpnf 10990 -∞cmnf 10991 − cmin 11188 -cneg 11189 / cdiv 11615 ℕcn 11956 2c2 12011 ℕ₀cn0 12216 (,)cioo 13061 (,]cioc 13062 [,)cico 13063 seqcseq 13702 ⇝ cli 15174 Σcsu 15378 sincsin 15754 cosccos 15755 πcpi 15757 –cn→ccncf 24020 ∫citg 24763 lim_ℂ climc 25007 D cdv 25008

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-rep 5213 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7579 ax-inf2 9360 ax-cc 10175 ax-cnex 10911 ax-resscn 10912 ax-1cn 10913 ax-icn 10914 ax-addcl 10915 ax-addrcl 10916 ax-mulcl 10917 ax-mulrcl 10918 ax-mulcom 10919 ax-addass 10920 ax-mulass 10921 ax-distr 10922 ax-i2m1 10923 ax-1ne0 10924 ax-1rid 10925 ax-rnegex 10926 ax-rrecex 10927 ax-cnre 10928 ax-pre-lttri 10929 ax-pre-lttrn 10930 ax-pre-ltadd 10931 ax-pre-mulgt0 10932 ax-pre-sup 10933 ax-addf 10934 ax-mulf 10935

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-reu 3072 df-rmo 3073 df-rab 3074 df-v 3432 df-sbc 3720 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-pss 3910 df-symdif 4181 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4845 df-int 4885 df-iun 4931 df-iin 4932 df-disj 5044 df-br 5079 df-opab 5141 df-mpt 5162 df-tr 5196 df-id 5488 df-eprel 5494 df-po 5502 df-so 5503 df-fr 5543 df-se 5544 df-we 5545 df-xp 5594 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-rn 5599 df-res 5600 df-ima 5601 df-pred 6199 df-ord 6266 df-on 6267 df-lim 6268 df-suc 6269 df-iota 6388 df-fun 6432 df-fn 6433 df-f 6434 df-f1 6435 df-fo 6436 df-f1o 6437 df-fv 6438 df-isom 6439 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-of 7524 df-ofr 7525 df-om 7701 df-1st 7817 df-2nd 7818 df-supp 7962 df-frecs 8081 df-wrecs 8112 df-recs 8186 df-rdg 8225 df-1o 8281 df-2o 8282 df-oadd 8285 df-omul 8286 df-er 8472 df-map 8591 df-pm 8592 df-ixp 8660 df-en 8708 df-dom 8709 df-sdom 8710 df-fin 8711 df-fsupp 9090 df-fi 9131 df-sup 9162 df-inf 9163 df-oi 9230 df-dju 9643 df-card 9681 df-acn 9684 df-pnf 10995 df-mnf 10996 df-xr 10997 df-ltxr 10998 df-le 10999 df-sub 11190 df-neg 11191 df-div 11616 df-nn 11957 df-2 12019 df-3 12020 df-4 12021 df-5 12022 df-6 12023 df-7 12024 df-8 12025 df-9 12026 df-n0 12217 df-xnn0 12289 df-z 12303 df-dec 12420 df-uz 12565 df-q 12671 df-rp 12713 df-xneg 12830 df-xadd 12831 df-xmul 12832 df-ioo 13065 df-ioc 13066 df-ico 13067 df-icc 13068 df-fz 13222 df-fzo 13365 df-fl 13493 df-mod 13571 df-seq 13703 df-exp 13764 df-fac 13969 df-bc 13998 df-hash 14026 df-shft 14759 df-cj 14791 df-re 14792 df-im 14793 df-sqrt 14927 df-abs 14928 df-limsup 15161 df-clim 15178 df-rlim 15179 df-sum 15379 df-ef 15758 df-sin 15760 df-cos 15761 df-pi 15763 df-struct 16829 df-sets 16846 df-slot 16864 df-ndx 16876 df-base 16894 df-ress 16923 df-plusg 16956 df-mulr 16957 df-starv 16958 df-sca 16959 df-vsca 16960 df-ip 16961 df-tset 16962 df-ple 16963 df-ds 16965 df-unif 16966 df-hom 16967 df-cco 16968 df-rest 17114 df-topn 17115 df-0g 17133 df-gsum 17134 df-topgen 17135 df-pt 17136 df-prds 17139 df-xrs 17194 df-qtop 17199 df-imas 17200 df-xps 17202 df-mre 17276 df-mrc 17277 df-acs 17279 df-mgm 18307 df-sgrp 18356 df-mnd 18367 df-submnd 18412 df-mulg 18682 df-cntz 18904 df-cmn 19369 df-psmet 20570 df-xmet 20571 df-met 20572 df-bl 20573 df-mopn 20574 df-fbas 20575 df-fg 20576 df-cnfld 20579 df-top 22024 df-topon 22041 df-topsp 22063 df-bases 22077 df-cld 22151 df-ntr 22152 df-cls 22153 df-nei 22230 df-lp 22268 df-perf 22269 df-cn 22359 df-cnp 22360 df-t1 22446 df-haus 22447 df-cmp 22519 df-tx 22694 df-hmeo 22887 df-fil 22978 df-fm 23070 df-flim 23071 df-flf 23072 df-xms 23454 df-ms 23455 df-tms 23456 df-cncf 24022 df-ovol 24609 df-vol 24610 df-mbf 24764 df-itg1 24765 df-itg2 24766 df-ibl 24767 df-itg 24768 df-0p 24815 df-ditg 24992 df-limc 25011 df-dv 25012

This theorem is referenced by: fourier 43720 fouriercnp 43721 fourier2 43722

W3C validator