![]() |
Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > fourierd | Structured version Visualization version GIF version |
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 44779. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 44780 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 44785. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
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 | β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) |
fourierd.b | β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) |
Ref | Expression |
---|---|
fourierd | β’ (π β (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π ) / 2)) |
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 β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) | |
13 | fourierd.b | . . 3 β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) | |
14 | nfcv 2903 | . . . 4 β’ β²π(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) | |
15 | nfmpt1 5250 | . . . . . . . 8 β’ β²π(π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) | |
16 | 12, 15 | nfcxfr 2901 | . . . . . . 7 β’ β²ππ΄ |
17 | nfcv 2903 | . . . . . . 7 β’ β²ππ | |
18 | 16, 17 | nffv 6889 | . . . . . 6 β’ β²π(π΄βπ) |
19 | nfcv 2903 | . . . . . 6 β’ β²π Β· | |
20 | nfcv 2903 | . . . . . 6 β’ β²π(cosβ(π Β· π)) | |
21 | 18, 19, 20 | nfov 7424 | . . . . 5 β’ β²π((π΄βπ) Β· (cosβ(π Β· π))) |
22 | nfcv 2903 | . . . . 5 β’ β²π + | |
23 | nfmpt1 5250 | . . . . . . . 8 β’ β²π(π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) | |
24 | 13, 23 | nfcxfr 2901 | . . . . . . 7 β’ β²ππ΅ |
25 | 24, 17 | nffv 6889 | . . . . . 6 β’ β²π(π΅βπ) |
26 | nfcv 2903 | . . . . . 6 β’ β²π(sinβ(π Β· π)) | |
27 | 25, 19, 26 | nfov 7424 | . . . . 5 β’ β²π((π΅βπ) Β· (sinβ(π Β· π))) |
28 | 21, 22, 27 | nfov 7424 | . . . 4 β’ β²π(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) |
29 | fveq2 6879 | . . . . . 6 β’ (π = π β (π΄βπ) = (π΄βπ)) | |
30 | oveq1 7401 | . . . . . . 7 β’ (π = π β (π Β· π) = (π Β· π)) | |
31 | 30 | fveq2d 6883 | . . . . . 6 β’ (π = π β (cosβ(π Β· π)) = (cosβ(π Β· π))) |
32 | 29, 31 | oveq12d 7412 | . . . . 5 β’ (π = π β ((π΄βπ) Β· (cosβ(π Β· π))) = ((π΄βπ) Β· (cosβ(π Β· π)))) |
33 | fveq2 6879 | . . . . . 6 β’ (π = π β (π΅βπ) = (π΅βπ)) | |
34 | 30 | fveq2d 6883 | . . . . . 6 β’ (π = π β (sinβ(π Β· π)) = (sinβ(π Β· π))) |
35 | 33, 34 | oveq12d 7412 | . . . . 5 β’ (π = π β ((π΅βπ) Β· (sinβ(π Β· π))) = ((π΅βπ) Β· (sinβ(π Β· π)))) |
36 | 32, 35 | oveq12d 7412 | . . . 4 β’ (π = π β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
37 | 14, 28, 36 | cbvmpt 5253 | . . 3 β’ (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
38 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 37 | fourierdlem115 44774 | . 2 β’ (π β (seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) β (((πΏ + π ) / 2) β ((π΄β0) / 2)) β§ (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π ) / 2))) |
39 | 38 | simprd 496 | 1 β’ (π β (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π ) / 2)) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 396 = wceq 1541 β wcel 2106 β wne 2940 β cdif 3942 β c0 4319 class class class wbr 5142 β¦ cmpt 5225 dom cdm 5670 βΎ cres 5672 βΆwf 6529 βcfv 6533 (class class class)co 7394 Fincfn 8924 βcc 11092 βcr 11093 0cc0 11094 1c1 11095 + caddc 11097 Β· cmul 11099 +βcpnf 11229 -βcmnf 11230 β cmin 11428 -cneg 11429 / cdiv 11855 βcn 12196 2c2 12251 β0cn0 12456 (,)cioo 13308 (,]cioc 13309 [,)cico 13310 seqcseq 13950 β cli 15412 Ξ£csu 15616 sincsin 15991 cosccos 15992 Οcpi 15994 βcnβccncf 24323 β«citg 25066 limβ climc 25310 D cdv 25311 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5357 ax-pr 5421 ax-un 7709 ax-inf2 9620 ax-cc 10414 ax-cnex 11150 ax-resscn 11151 ax-1cn 11152 ax-icn 11153 ax-addcl 11154 ax-addrcl 11155 ax-mulcl 11156 ax-mulrcl 11157 ax-mulcom 11158 ax-addass 11159 ax-mulass 11160 ax-distr 11161 ax-i2m1 11162 ax-1ne0 11163 ax-1rid 11164 ax-rnegex 11165 ax-rrecex 11166 ax-cnre 11167 ax-pre-lttri 11168 ax-pre-lttrn 11169 ax-pre-ltadd 11170 ax-pre-mulgt0 11171 ax-pre-sup 11172 ax-addf 11173 ax-mulf 11174 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-symdif 4239 df-nul 4320 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4903 df-int 4945 df-iun 4993 df-iin 4994 df-disj 5108 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5568 df-eprel 5574 df-po 5582 df-so 5583 df-fr 5625 df-se 5626 df-we 5627 df-xp 5676 df-rel 5677 df-cnv 5678 df-co 5679 df-dm 5680 df-rn 5681 df-res 5682 df-ima 5683 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7350 df-ov 7397 df-oprab 7398 df-mpo 7399 df-of 7654 df-ofr 7655 df-om 7840 df-1st 7959 df-2nd 7960 df-supp 8131 df-frecs 8250 df-wrecs 8281 df-recs 8355 df-rdg 8394 df-1o 8450 df-2o 8451 df-oadd 8454 df-omul 8455 df-er 8688 df-map 8807 df-pm 8808 df-ixp 8877 df-en 8925 df-dom 8926 df-sdom 8927 df-fin 8928 df-fsupp 9347 df-fi 9390 df-sup 9421 df-inf 9422 df-oi 9489 df-dju 9880 df-card 9918 df-acn 9921 df-pnf 11234 df-mnf 11235 df-xr 11236 df-ltxr 11237 df-le 11238 df-sub 11430 df-neg 11431 df-div 11856 df-nn 12197 df-2 12259 df-3 12260 df-4 12261 df-5 12262 df-6 12263 df-7 12264 df-8 12265 df-9 12266 df-n0 12457 df-xnn0 12529 df-z 12543 df-dec 12662 df-uz 12807 df-q 12917 df-rp 12959 df-xneg 13076 df-xadd 13077 df-xmul 13078 df-ioo 13312 df-ioc 13313 df-ico 13314 df-icc 13315 df-fz 13469 df-fzo 13612 df-fl 13741 df-mod 13819 df-seq 13951 df-exp 14012 df-fac 14218 df-bc 14247 df-hash 14275 df-shft 14998 df-cj 15030 df-re 15031 df-im 15032 df-sqrt 15166 df-abs 15167 df-limsup 15399 df-clim 15416 df-rlim 15417 df-sum 15617 df-ef 15995 df-sin 15997 df-cos 15998 df-pi 16000 df-struct 17064 df-sets 17081 df-slot 17099 df-ndx 17111 df-base 17129 df-ress 17158 df-plusg 17194 df-mulr 17195 df-starv 17196 df-sca 17197 df-vsca 17198 df-ip 17199 df-tset 17200 df-ple 17201 df-ds 17203 df-unif 17204 df-hom 17205 df-cco 17206 df-rest 17352 df-topn 17353 df-0g 17371 df-gsum 17372 df-topgen 17373 df-pt 17374 df-prds 17377 df-xrs 17432 df-qtop 17437 df-imas 17438 df-xps 17440 df-mre 17514 df-mrc 17515 df-acs 17517 df-mgm 18545 df-sgrp 18594 df-mnd 18605 df-submnd 18650 df-mulg 18925 df-cntz 19149 df-cmn 19616 df-psmet 20872 df-xmet 20873 df-met 20874 df-bl 20875 df-mopn 20876 df-fbas 20877 df-fg 20878 df-cnfld 20881 df-top 22327 df-topon 22344 df-topsp 22366 df-bases 22380 df-cld 22454 df-ntr 22455 df-cls 22456 df-nei 22533 df-lp 22571 df-perf 22572 df-cn 22662 df-cnp 22663 df-t1 22749 df-haus 22750 df-cmp 22822 df-tx 22997 df-hmeo 23190 df-fil 23281 df-fm 23373 df-flim 23374 df-flf 23375 df-xms 23757 df-ms 23758 df-tms 23759 df-cncf 24325 df-ovol 24912 df-vol 24913 df-mbf 25067 df-itg1 25068 df-itg2 25069 df-ibl 25070 df-itg 25071 df-0p 25118 df-ditg 25295 df-limc 25314 df-dv 25315 |
This theorem is referenced by: fourier 44778 fouriercnp 44779 fourier2 44780 |
Copyright terms: Public domain | W3C validator |