![]() |
Metamath
Proof Explorer Theorem List (p. 450 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dirkertrigeqlem3 44901* | Trigonometric equality lemma for the Dirichlet Kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of Ο. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β πΎ β β€) & β’ π΄ = (((2 Β· πΎ) + 1) Β· Ο) β β’ (π β (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π΄))) / Ο) = ((sinβ((π + (1 / 2)) Β· π΄)) / ((2 Β· Ο) Β· (sinβ(π΄ / 2))))) | ||
Theorem | dirkertrigeq 44902* | Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) & β’ (π β π β β) & β’ πΉ = (π·βπ) & β’ π» = (π β β β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) β β’ (π β πΉ = π») | ||
Theorem | dirkeritg 44903* | The definite integral of the Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π₯ β β β¦ if((π₯ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β· (sinβ(π₯ / 2))))))) & β’ (π β π β β) & β’ πΉ = (π·βπ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ (((π₯ / 2) + Ξ£π β (1...π)((sinβ(π Β· π₯)) / π)) / Ο)) β β’ (π β β«(π΄(,)π΅)(πΉβπ₯) dπ₯ = ((πΊβπ΅) β (πΊβπ΄))) | ||
Theorem | dirkercncflem1 44904* | If π is a multiple of Ο then it belongs to an open inerval (π΄(,)π΅) such that for any other point π¦ in the interval, cos y/2 and sin y/2 are nonzero. Such an interval is needed to apply De L'Hopital theorem. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π΄ = (π β Ο) & β’ π΅ = (π + Ο) & β’ (π β π β β) & β’ (π β (π mod (2 Β· Ο)) = 0) β β’ (π β (π β (π΄(,)π΅) β§ βπ¦ β ((π΄(,)π΅) β {π})((sinβ(π¦ / 2)) β 0 β§ (cosβ(π¦ / 2)) β 0))) | ||
Theorem | dirkercncflem2 44905* | Lemma used to prove that the Dirichlet Kernel is continuous at π points that are multiples of (2 Β· Ο). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ πΉ = (π¦ β ((π΄(,)π΅) β {π}) β¦ (sinβ((π + (1 / 2)) Β· π¦))) & β’ πΊ = (π¦ β ((π΄(,)π΅) β {π}) β¦ ((2 Β· Ο) Β· (sinβ(π¦ / 2)))) & β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (sinβ(π¦ / 2)) β 0) & β’ π» = (π¦ β ((π΄(,)π΅) β {π}) β¦ ((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π¦)))) & β’ πΌ = (π¦ β ((π΄(,)π΅) β {π}) β¦ (Ο Β· (cosβ(π¦ / 2)))) & β’ πΏ = (π€ β (π΄(,)π΅) β¦ (((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π€))) / (Ο Β· (cosβ(π€ / 2))))) & β’ (π β π β β) & β’ (π β π β (π΄(,)π΅)) & β’ (π β (π mod (2 Β· Ο)) = 0) & β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (cosβ(π¦ / 2)) β 0) β β’ (π β ((π·βπ)βπ) β (((π·βπ) βΎ ((π΄(,)π΅) β {π})) limβ π)) | ||
Theorem | dirkercncflem3 44906* | The Dirichlet Kernel is continuous at π points that are multiples of (2 Β· Ο). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ π΄ = (π β Ο) & β’ π΅ = (π + Ο) & β’ πΉ = (π¦ β (π΄(,)π΅) β¦ ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))) & β’ πΊ = (π¦ β (π΄(,)π΅) β¦ ((2 Β· Ο) Β· (sinβ(π¦ / 2)))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π mod (2 Β· Ο)) = 0) β β’ (π β ((π·βπ)βπ) β ((π·βπ) limβ π)) | ||
Theorem | dirkercncflem4 44907* | The Dirichlet Kernel is continuos at points that are not multiple of 2 Ο . This is the easier condition, for the proof of the continuity of the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π mod (2 Β· Ο)) β 0) & β’ π΄ = (ββ(π / (2 Β· Ο))) & β’ π΅ = (π΄ + 1) & β’ πΆ = (π΄ Β· (2 Β· Ο)) & β’ πΈ = (π΅ Β· (2 Β· Ο)) β β’ (π β (π·βπ) β (((topGenβran (,)) CnP (topGenβran (,)))βπ)) | ||
Theorem | dirkercncf 44908* | For any natural number π, the Dirichlet Kernel (π·βπ) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) β β’ (π β β β (π·βπ) β (ββcnββ)) | ||
Theorem | fourierdlem1 44909 | A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ (π β πΌ β (0..^π)) & β’ (π β π β ((πβπΌ)[,](πβ(πΌ + 1)))) β β’ (π β π β (π΄[,]π΅)) | ||
Theorem | fourierdlem2 44910* | Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) β β’ (π β β β (π β (πβπ) β (π β (β βm (0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) | ||
Theorem | fourierdlem3 44911* | Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β ((-Ο[,]Ο) βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) β β’ (π β β β (π β (πβπ) β (π β ((-Ο[,]Ο) βm (0...π)) β§ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) | ||
Theorem | fourierdlem4 44912* | πΈ is a function that maps any point to a periodic corresponding point in (π΄, π΅]. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) β β’ (π β πΈ:ββΆ(π΄(,]π΅)) | ||
Theorem | fourierdlem5 44913* | π is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π₯ β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π₯))) β β’ (π β β β π:(-Ο[,]Ο)βΆβ) | ||
Theorem | fourierdlem6 44914 | π is in the periodic partition, when the considered interval is centered at π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β πΌ β β€) & β’ (π β π½ β β€) & β’ (π β πΌ < π½) & β’ (π β (π + (πΌ Β· π)) β (π΄[,]π΅)) & β’ (π β (π + (π½ Β· π)) β (π΄[,]π΅)) β β’ (π β π½ = (πΌ + 1)) | ||
Theorem | fourierdlem7 44915* | The difference between the periodic sawtooth function and the identity function is decreasing. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) β β’ (π β ((πΈβπ) β π) β€ ((πΈβπ) β π)) | ||
Theorem | fourierdlem8 44916 | A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ (π β πΌ β (0..^π)) β β’ (π β ((πβπΌ)[,](πβ(πΌ + 1))) β (π΄[,]π΅)) | ||
Theorem | fourierdlem9 44917* | π» is a complex function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) β β’ (π β π»:(-Ο[,]Ο)βΆβ) | ||
Theorem | fourierdlem10 44918 | Condition on the bounds of a nonempty subinterval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ (π β (πΆ(,)π·) β (π΄(,)π΅)) β β’ (π β (π΄ β€ πΆ β§ π· β€ π΅)) | ||
Theorem | fourierdlem11 44919* | If there is a partition, than the lower bound is strictly less than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) β β’ (π β (π΄ β β β§ π΅ β β β§ π΄ < π΅)) | ||
Theorem | fourierdlem12 44920* | A point of a partition is not an element of any open interval determined by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β π β ran π) β β’ ((π β§ π β (0..^π)) β Β¬ π β ((πβπ)(,)(πβ(π + 1)))) | ||
Theorem | fourierdlem13 44921* | Value of π in terms of value of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (π΄ + π) β§ (πβπ) = (π΅ + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΌ β (0...π)) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) β β’ (π β ((πβπΌ) = ((πβπΌ) β π) β§ (πβπΌ) = (π + (πβπΌ)))) | ||
Theorem | fourierdlem14 44922* | Given the partition π, π is the partition shifted to the left by π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (π΄ + π) β§ (πβπ) = (π΅ + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) β β’ (π β π β (πβπ)) | ||
Theorem | fourierdlem15 44923* | The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) β β’ (π β π:(0...π)βΆ(π΄[,]π΅)) | ||
Theorem | fourierdlem16 44924* | The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ πΆ = (-Ο(,)Ο) & β’ (π β (πΉ βΎ πΆ) β πΏ1) & β’ π΄ = (π β β0 β¦ (β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ (π β π β β0) β β’ (π β (((π΄βπ) β β β§ (π₯ β πΆ β¦ (πΉβπ₯)) β πΏ1) β§ β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β)) | ||
Theorem | fourierdlem17 44925* | The defined πΏ is actually a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ πΏ = (π₯ β (π΄(,]π΅) β¦ if(π₯ = π΅, π΄, π₯)) β β’ (π β πΏ:(π΄(,]π΅)βΆ(π΄[,]π΅)) | ||
Theorem | fourierdlem18 44926* | The function π is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) β β’ (π β π β ((-Ο[,]Ο)βcnββ)) | ||
Theorem | fourierdlem19 44927* | If two elements of π· have the same periodic image in (π΄(,]π΅) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β π β β) & β’ π· = {π¦ β ((π΄ + π)(,](π΅ + π)) β£ βπ β β€ (π¦ + (π Β· π)) β πΆ} & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β π β π·) & β’ (π β π β π·) & β’ (π β (πΈβπ) = (πΈβπ)) β β’ (π β Β¬ π < π) | ||
Theorem | fourierdlem20 44928* | Every interval in the partition π is included in an interval of the partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π:(0...π)βΆβ) & β’ (π β (πβ0) β€ π΄) & β’ (π β π΅ β€ (πβπ)) & β’ (π β π½ β (0..^π)) & β’ π = ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) & β’ (π β π Isom < , < ((0...π), π)) & β’ πΌ = sup({π β (0..^π) β£ (πβπ) β€ (πβπ½)}, β, < ) β β’ (π β βπ β (0..^π)((πβπ½)(,)(πβ(π½ + 1))) β ((πβπ)(,)(πβ(π + 1)))) | ||
Theorem | fourierdlem21 44929* | The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ πΆ = (-Ο(,)Ο) & β’ (π β (πΉ βΎ πΆ) β πΏ1) & β’ π΅ = (π β β β¦ (β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) & β’ (π β π β β) β β’ (π β (((π΅βπ) β β β§ (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β πΏ1) β§ β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β)) | ||
Theorem | fourierdlem22 44930* | The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ πΆ = (-Ο(,)Ο) & β’ (π β (πΉ βΎ πΆ) β πΏ1) & β’ π΄ = (π β β0 β¦ (β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) β β’ (π β ((π β β0 β (π΄βπ) β β) β§ (π β β β (π΅βπ) β β))) | ||
Theorem | fourierdlem23 44931* | If πΉ is continuous and π is constant, then (πΉβ(π + π )) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ ((π β§ π β π΅) β (π + π ) β π΄) β β’ (π β (π β π΅ β¦ (πΉβ(π + π ))) β (π΅βcnββ)) | ||
Theorem | fourierdlem24 44932 | A sufficient condition for module being nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β ((-Ο[,]Ο) β {0}) β (π΄ mod (2 Β· Ο)) β 0) | ||
Theorem | fourierdlem25 44933* | If πΆ is not in the range of the partition, then it is in an open interval induced by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π:(0...π)βΆβ) & β’ (π β πΆ β ((πβ0)[,](πβπ))) & β’ (π β Β¬ πΆ β ran π) & β’ πΌ = sup({π β (0..^π) β£ (πβπ) < πΆ}, β, < ) β β’ (π β βπ β (0..^π)πΆ β ((πβπ)(,)(πβ(π + 1)))) | ||
Theorem | fourierdlem26 44934* | Periodic image of a point π that's in the period that begins with the point π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β π β β) & β’ (π β (πΈβπ) = π΅) & β’ (π β π β (π(,](π + π))) β β’ (π β (πΈβπ) = (π΄ + (π β π))) | ||
Theorem | fourierdlem27 44935 | A partition open interval is a subset of the partitioned open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ (π β πΌ β (0..^π)) β β’ (π β ((πβπΌ)(,)(πβ(πΌ + 1))) β (π΄(,)π΅)) | ||
Theorem | fourierdlem28 44936* | Derivative of (πΉβ(π + π )). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ π· = (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))) & β’ (π β π·:((π + π΄)(,)(π + π΅))βΆβ) β β’ (π β (β D (π β (π΄(,)π΅) β¦ (πΉβ(π + π )))) = (π β (π΄(,)π΅) β¦ (π·β(π + π )))) | ||
Theorem | fourierdlem29 44937* | Explicit function value for πΎ applied to π΄. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) β β’ (π΄ β (-Ο[,]Ο) β (πΎβπ΄) = if(π΄ = 0, 1, (π΄ / (2 Β· (sinβ(π΄ / 2)))))) | ||
Theorem | fourierdlem30 44938* | Sum of three small pieces is less than Ξ΅. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β πΌ β¦ (πΉ Β· -πΊ)) β πΏ1) & β’ ((π β§ π₯ β πΌ) β πΉ β β) & β’ ((π β§ π₯ β πΌ) β πΊ β β) & β’ (π β π΄ β β) & β’ π = (absβπ΄) & β’ (π β πΆ β β) & β’ π = (absβπΆ) & β’ π = (absββ«πΌ(πΉ Β· -πΊ) dπ₯) & β’ (π β πΈ β β+) & β’ (π β π β β) & β’ (π β ((((π + π) + π) / πΈ) + 1) β€ π ) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) β€ 1) & β’ (π β π· β β) & β’ (π β (absβπ·) β€ 1) β β’ (π β (absβ(((π΄ Β· -(π΅ / π )) β (πΆ Β· -(π· / π ))) β β«πΌ(πΉ Β· -(πΊ / π )) dπ₯)) < πΈ) | ||
Theorem | fourierdlem31 44939* | If π΄ is finite and for any element in π΄ there is a number π such that a property holds for all numbers larger than π, then there is a number π such that the property holds for all numbers larger than π and for all elements in π΄. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.) |
β’ β²ππ & β’ β²ππ & β’ β²ππ & β’ (π β π΄ β Fin) & β’ (π β βπ β π΄ βπ β β βπ β (π(,)+β)π) & β’ π = {π β β β£ βπ β (π(,)+β)π} & β’ π = (π β π΄ β¦ inf(π, β, < )) & β’ π = sup(ran π, β, < ) β β’ (π β βπ β β βπ β (π(,)+β)βπ β π΄ π) | ||
Theorem | fourierdlem32 44940 | Limit of a continuous function on an open subinterval. Lower bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β π β (πΉ limβ π΄)) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ (π β (πΆ(,)π·) β (π΄(,)π΅)) & β’ π = if(πΆ = π΄, π , (πΉβπΆ)) & β’ π½ = ((TopOpenββfld) βΎt (π΄[,)π΅)) β β’ (π β π β ((πΉ βΎ (πΆ(,)π·)) limβ πΆ)) | ||
Theorem | fourierdlem33 44941 | Limit of a continuous function on an open subinterval. Upper bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ (π β (πΆ(,)π·) β (π΄(,)π΅)) & β’ π = if(π· = π΅, πΏ, (πΉβπ·)) & β’ π½ = ((TopOpenββfld) βΎt ((π΄(,)π΅) βͺ {π΅})) β β’ (π β π β ((πΉ βΎ (πΆ(,)π·)) limβ π·)) | ||
Theorem | fourierdlem34 44942* | A partition is one to one. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) β β’ (π β π:(0...π)β1-1ββ) | ||
Theorem | fourierdlem35 44943 | There is a single point in (π΄(,]π΅) that's distant from π a multiple integer of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β πΌ β β€) & β’ (π β π½ β β€) & β’ (π β (π + (πΌ Β· π)) β (π΄(,]π΅)) & β’ (π β (π + (π½ Β· π)) β (π΄(,]π΅)) β β’ (π β πΌ = π½) | ||
Theorem | fourierdlem36 44944* | πΉ is an isomorphism. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β Fin) & β’ (π β π΄ β β) & β’ πΉ = (β©ππ Isom < , < ((0...π), π΄)) & β’ π = ((β―βπ΄) β 1) β β’ (π β πΉ Isom < , < ((0...π), π΄)) | ||
Theorem | fourierdlem37 44945* | πΌ is a function that maps any real point to the point that in the partition that immediately precedes the corresponding periodic point in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ πΏ = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) & β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}, β, < )) β β’ (π β (πΌ:ββΆ(0..^π) β§ (π₯ β β β sup({π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}, β, < ) β {π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}))) | ||
Theorem | fourierdlem38 44946* | The function πΉ is continuous on every interval induced by the partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (dom πΉβcnββ)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ π» = (π΄ βͺ ((-Ο[,]Ο) β dom πΉ)) & β’ (π β ran π = π») β β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) | ||
Theorem | fourierdlem39 44947* | Integration by parts of β«(π΄(,)π΅)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ πΊ = (β D πΉ) & β’ (π β πΊ β ((π΄(,)π΅)βcnββ)) & β’ (π β βπ¦ β β βπ₯ β (π΄(,)π΅)(absβ(πΊβπ₯)) β€ π¦) & β’ (π β π β β+) β β’ (π β β«(π΄(,)π΅)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ = ((((πΉβπ΅) Β· -((cosβ(π Β· π΅)) / π )) β ((πΉβπ΄) Β· -((cosβ(π Β· π΄)) / π ))) β β«(π΄(,)π΅)((πΊβπ₯) Β· -((cosβ(π Β· π₯)) / π )) dπ₯)) | ||
Theorem | fourierdlem40 44948* | π» is a continuous function on any partition interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π΄ β (-Ο[,]Ο)) & β’ (π β π΅ β (-Ο[,]Ο)) & β’ (π β π β β) & β’ (π β Β¬ 0 β (π΄(,)π΅)) & β’ (π β (πΉ βΎ ((π΄ + π)(,)(π΅ + π))) β (((π΄ + π)(,)(π΅ + π))βcnββ)) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) β β’ (π β (π» βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) | ||
Theorem | fourierdlem41 44949* | Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ ((π β§ π₯ β π· β§ π β β€) β (π₯ + (π Β· π)) β π·) & β’ (π β π β β) & β’ π = (π₯ β β β¦ ((ββ((π΅ β π₯) / π)) Β· π)) & β’ πΈ = (π₯ β β β¦ (π₯ + (πβπ₯))) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β π·) β β’ (π β (βπ¦ β β (π¦ < π β§ (π¦(,)π) β π·) β§ βπ¦ β β (π < π¦ β§ (π(,)π¦) β π·))) | ||
Theorem | fourierdlem42 44950* | The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ < πΆ) & β’ π = (πΆ β π΅) & β’ (π β π΄ β (π΅[,]πΆ)) & β’ (π β π΄ β Fin) & β’ (π β π΅ β π΄) & β’ (π β πΆ β π΄) & β’ π· = (abs β β ) & β’ πΌ = ((π΄ Γ π΄) β I ) & β’ π = ran (π· βΎ πΌ) & β’ πΈ = inf(π , β, < ) & β’ (π β π β β) & β’ (π β π β β) & β’ π½ = (topGenβran (,)) & β’ πΎ = (π½ βΎt (π[,]π)) & β’ π» = {π₯ β (π[,]π) β£ βπ β β€ (π₯ + (π Β· π)) β π΄} & β’ (π β ((π β§ (π β β β§ π β β β§ π < π)) β§ βπ β β€ βπ β β€ ((π + (π Β· π)) β π΄ β§ (π + (π Β· π)) β π΄))) β β’ (π β π» β Fin) | ||
Theorem | fourierdlem43 44951 | πΎ is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) β β’ πΎ:(-Ο[,]Ο)βΆβ | ||
Theorem | fourierdlem44 44952 | A condition for having (sinβ(π΄ / 2)) nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β (-Ο[,]Ο) β§ π΄ β 0) β (sinβ(π΄ / 2)) β 0) | ||
Theorem | fourierdlem46 44953* | The function πΉ has a limit at the bounds of every interval induced by the partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (dom πΉβcnββ)) & β’ ((π β§ π₯ β ((-Ο[,)Ο) β dom πΉ)) β ((πΉ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ ((π β§ π₯ β ((-Ο(,]Ο) β dom πΉ)) β ((πΉ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ (π β π Isom < , < ((0...π), π»)) & β’ (π β π:(0...π)βΆπ») & β’ (π β πΌ β (0..^π)) & β’ (π β (πβπΌ) < (πβ(πΌ + 1))) & β’ (π β ((πβπΌ)(,)(πβ(πΌ + 1))) β (-Ο(,)Ο)) & β’ (π β πΆ β β) & β’ π» = ({-Ο, Ο, πΆ} βͺ ((-Ο[,]Ο) β dom πΉ)) & β’ (π β ran π = π») β β’ (π β (((πΉ βΎ ((πβπΌ)(,)(πβ(πΌ + 1)))) limβ (πβπΌ)) β β β§ ((πΉ βΎ ((πβπΌ)(,)(πβ(πΌ + 1)))) limβ (πβ(πΌ + 1))) β β )) | ||
Theorem | fourierdlem47 44954* | For π large enough, the final expression is less than the given positive πΈ. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β πΌ β¦ πΉ) β πΏ1) & β’ ((π β§ π β β) β (π₯ β πΌ β¦ (πΉ Β· -πΊ)) β πΏ1) & β’ ((π β§ π₯ β πΌ) β πΉ β β) & β’ (((π β§ π₯ β πΌ) β§ π β β) β πΊ β β) & β’ (((π β§ π₯ β πΌ) β§ π β β) β (absβπΊ) β€ 1) & β’ (π β π΄ β β) & β’ π = (absβπ΄) & β’ (π β πΆ β β) & β’ π = (absβπΆ) & β’ π = β«πΌ(absβπΉ) dπ₯ & β’ (π β πΈ β β+) & β’ ((π β§ π β β) β π΅ β β) & β’ ((π β§ π β β) β (absβπ΅) β€ 1) & β’ ((π β§ π β β) β π· β β) & β’ ((π β§ π β β) β (absβπ·) β€ 1) & β’ π = ((ββ((((π + π) + π) / πΈ) + 1)) + 1) β β’ (π β βπ β β βπ β (π(,)+β)(absβ(((π΄ Β· -(π΅ / π)) β (πΆ Β· -(π· / π))) β β«πΌ(πΉ Β· -(πΊ / π)) dπ₯)) < πΈ) | ||
Theorem | fourierdlem48 44955* | The given periodic function πΉ has a right limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΉ:π·βΆβ) & β’ ((π β§ π₯ β π· β§ π β β€) β (π₯ + (π Β· π)) β π·) & β’ ((π β§ π₯ β π· β§ π β β€) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ (π β π β β) & β’ π = (π₯ β β β¦ ((ββ((π΅ β π₯) / π)) Β· π)) & β’ πΈ = (π₯ β β β¦ (π₯ + (πβπ₯))) & β’ (π β ((((π β§ π β (0..^π)) β§ π¦ β ((πβπ)[,)(πβ(π + 1)))) β§ π β β€) β§ π¦ = (π + (π Β· π)))) β β’ (π β ((πΉ βΎ (π(,)+β)) limβ π) β β ) | ||
Theorem | fourierdlem49 44956* | The given periodic function πΉ has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β π· β β) & β’ (π β πΉ:π·βΆβ) & β’ ((π β§ π₯ β π· β§ π β β€) β (π₯ + (π Β· π)) β π·) & β’ ((π β§ π₯ β π· β§ π β β€) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ (π β π β β) & β’ π = (π₯ β β β¦ ((ββ((π΅ β π₯) / π)) Β· π)) & β’ πΈ = (π₯ β β β¦ (π₯ + (πβπ₯))) β β’ (π β ((πΉ βΎ (-β(,)π)) limβ π) β β ) | ||
Theorem | fourierdlem50 44957* | Continuity of π and its limits with respect to the π partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β (π΄[,]π΅) β (-Ο[,]Ο)) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ π = ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) & β’ π = ((β―βπ) β 1) & β’ π = (β©ππ Isom < , < ((0...π), π)) & β’ (π β π½ β (0..^π)) & β’ π = (β©π β (0..^π)((πβπ½)(,)(πβ(π½ + 1))) β ((πβπ)(,)(πβ(π + 1)))) & β’ (π β ((((π β§ π β (0..^π)) β§ ((πβπ½)(,)(πβ(π½ + 1))) β ((πβπ)(,)(πβ(π + 1)))) β§ π β (0..^π)) β§ ((πβπ½)(,)(πβ(π½ + 1))) β ((πβπ)(,)(πβ(π + 1))))) β β’ (π β (π β (0..^π) β§ ((πβπ½)(,)(πβ(π½ + 1))) β ((πβπ)(,)(πβ(π + 1))))) | ||
Theorem | fourierdlem51 44958* | π is in the periodic partition, when the considered interval is centered at π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < 0) & β’ (π β 0 < π΅) & β’ π = (π΅ β π΄) & β’ (π β πΆ β Fin) & β’ (π β πΆ β (π΄[,]π΅)) & β’ (π β π΅ β πΆ) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β π β β) & β’ (π β (πΈβπ) β πΆ) & β’ π· = ({(π΄ + π), (π΅ + π)} βͺ {π¦ β ((π΄ + π)[,](π΅ + π)) β£ βπ β β€ (π¦ + (π Β· π)) β πΆ}) & β’ πΉ = (β©ππ Isom < , < ((0...((β―βπ·) β 1)), π·)) & β’ π» = {π¦ β ((π΄ + π)(,](π΅ + π)) β£ βπ β β€ (π¦ + (π Β· π)) β πΆ} β β’ (π β π β ran πΉ) | ||
Theorem | fourierdlem52 44959* | d16:d17,d18:jca |- ( ph -> ( ( S 0) β€ π΄ β§ π΄ β€ (π 0 ) ) ) . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β Fin) & β’ π = ((β―βπ) β 1) & β’ π = (β©ππ Isom < , < ((0...π), π)) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β (π΄[,]π΅)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β ((π:(0...π)βΆ(π΄[,]π΅) β§ (πβ0) = π΄) β§ (πβπ) = π΅)) | ||
Theorem | fourierdlem53 44960* | The limit of πΉ(π ) at (π + π·) is the limit of πΉ(π + π ) at π·. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ πΊ = (π β π΄ β¦ (πΉβ(π + π ))) & β’ ((π β§ π β π΄) β (π + π ) β π΅) & β’ (π β π΅ β β) & β’ ((π β§ π β π΄) β π β π·) & β’ (π β πΆ β ((πΉ βΎ π΅) limβ (π + π·))) & β’ (π β π· β β) β β’ (π β πΆ β (πΊ limβ π·)) | ||
Theorem | fourierdlem54 44961* | Given a partition π and an arbitrary interval [πΆ, π·], a partition π on [πΆ, π·] is built such that it preserves any periodic function piecewise continuous on π will be piecewise continuous on π, with the same limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π΅ β π΄) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π» = ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) β β’ (π β ((π β β β§ π β (πβπ)) β§ π Isom < , < ((0...π), π»))) | ||
Theorem | fourierdlem55 44962* | π is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) β β’ (π β π:(-Ο[,]Ο)βΆβ) | ||
Theorem | fourierdlem56 44963* | Derivative of the πΎ function on an interval not containing ' 0 '. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ (π β (π΄(,)π΅) β ((-Ο[,]Ο) β {0})) & β’ ((π β§ π β (π΄(,)π΅)) β π β 0) β β’ (π β (β D (π β (π΄(,)π΅) β¦ (πΎβπ ))) = (π β (π΄(,)π΅) β¦ ((((sinβ(π / 2)) β (((cosβ(π / 2)) / 2) Β· π )) / ((sinβ(π / 2))β2)) / 2))) | ||
Theorem | fourierdlem57 44964* | The derivative of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))):((π + π΄)(,)(π + π΅))βΆβ) & β’ (π β (π΄(,)π΅) β (-Ο[,]Ο)) & β’ (π β Β¬ 0 β (π΄(,)π΅)) & β’ (π β πΆ β β) & β’ π = (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))) β β’ ((π β ((β D π):(π΄(,)π΅)βΆβ β§ (β D π) = (π β (π΄(,)π΅) β¦ (((((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))β(π + π )) Β· (2 Β· (sinβ(π / 2)))) β ((cosβ(π / 2)) Β· ((πΉβ(π + π )) β πΆ))) / ((2 Β· (sinβ(π / 2)))β2))))) β§ (β D (π β (π΄(,)π΅) β¦ (2 Β· (sinβ(π / 2))))) = (π β (π΄(,)π΅) β¦ (cosβ(π / 2)))) | ||
Theorem | fourierdlem58 44965* | The derivative of πΎ is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (π β π΄ β¦ (π / (2 Β· (sinβ(π / 2))))) & β’ (π β π΄ β (-Ο[,]Ο)) & β’ (π β Β¬ 0 β π΄) & β’ (π β π΄ β (topGenβran (,))) β β’ (π β (β D πΎ) β (π΄βcnββ)) | ||
Theorem | fourierdlem59 44966* | The derivative of π» is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β Β¬ 0 β (π΄(,)π΅)) & β’ (π β (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))) β (((π + π΄)(,)(π + π΅))βcnββ)) & β’ (π β πΆ β β) & β’ π» = (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / π )) β β’ (π β (β D π») β ((π΄(,)π΅)βcnββ)) | ||
Theorem | fourierdlem60 44967* | Given a differentiable function πΉ, with finite limit of the derivative at π΄ the derived function π» has a limit at 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β π β (πΉ limβ π΅)) & β’ πΊ = (β D πΉ) & β’ (π β dom πΊ = (π΄(,)π΅)) & β’ (π β πΈ β (πΊ limβ π΅)) & β’ π» = (π β ((π΄ β π΅)(,)0) β¦ (((πΉβ(π΅ + π )) β π) / π )) & β’ π = (π β ((π΄ β π΅)(,)0) β¦ ((πΉβ(π΅ + π )) β π)) & β’ π· = (π β ((π΄ β π΅)(,)0) β¦ π ) β β’ (π β πΈ β (π» limβ 0)) | ||
Theorem | fourierdlem61 44968* | Given a differentiable function πΉ, with finite limit of the derivative at π΄ the derived function π» has a limit at 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) & β’ (π β π β (πΉ limβ π΄)) & β’ πΊ = (β D πΉ) & β’ (π β dom πΊ = (π΄(,)π΅)) & β’ (π β πΈ β (πΊ limβ π΄)) & β’ π» = (π β (0(,)(π΅ β π΄)) β¦ (((πΉβ(π΄ + π )) β π) / π )) & β’ π = (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) & β’ π· = (π β (0(,)(π΅ β π΄)) β¦ π ) β β’ (π β πΈ β (π» limβ 0)) | ||
Theorem | fourierdlem62 44969 | The function πΎ is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (π¦ β (-Ο[,]Ο) β¦ if(π¦ = 0, 1, (π¦ / (2 Β· (sinβ(π¦ / 2)))))) β β’ πΎ β ((-Ο[,]Ο)βcnββ) | ||
Theorem | fourierdlem63 44970* | The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π΅ β π΄) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π» = ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β πΎ β (0...π)) & β’ (π β π½ β (0..^π)) & β’ (π β π β ((πβπ½)[,)(πβ(π½ + 1)))) & β’ (π β (πΈβπ) < (πβπΎ)) & β’ π = ((πβπΎ) β ((πΈβπ) β π)) β β’ (π β (πΈβ(πβ(π½ + 1))) β€ (πβπΎ)) | ||
Theorem | fourierdlem64 44971* | The partition π is finer than π, when π is moved on the same interval where π lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π΅ β π΄) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ π» = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) & β’ (π β π½ β (0..^π)) & β’ πΏ = sup({π β β€ β£ ((πβ0) + (π Β· π)) β€ (πβπ½)}, β, < ) & β’ πΌ = sup({π β (0..^π) β£ ((πβπ) + (πΏ Β· π)) β€ (πβπ½)}, β, < ) β β’ (π β ((πΌ β (0..^π) β§ πΏ β β€) β§ βπ β (0..^π)βπ β β€ ((πβπ½)(,)(πβ(π½ + 1))) β (((πβπ) + (π Β· π))(,)((πβ(π + 1)) + (π Β· π))))) | ||
Theorem | fourierdlem65 44972* | The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΆ β β) & β’ (π β π· β (πΆ(,)+β)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = ((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π})) β 1) & β’ π = (β©ππ Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}))) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ πΏ = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) & β’ π = ((πβπ) + (π΅ β (πΈβ(πβπ)))) β β’ ((π β§ π β (0..^π)) β ((πΈβ(πβ(π + 1))) β (πΏβ(πΈβ(πβπ)))) = ((πβ(π + 1)) β (πβπ))) | ||
Theorem | fourierdlem66 44973* | Value of the πΊ function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) & β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) & β’ π΄ = ((-Ο[,]Ο) β {0}) β β’ (((π β§ π β β) β§ π β π΄) β (πΊβπ ) = (Ο Β· (((πΉβ(π + π )) β if(0 < π , π, π)) Β· ((π·βπ)βπ )))) | ||
Theorem | fourierdlem67 44974* | πΊ is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) & β’ (π β π β β) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) & β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) β β’ (π β πΊ:(-Ο[,]Ο)βΆβ) | ||
Theorem | fourierdlem68 44975* | The derivative of π is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β (π΄[,]π΅) β (-Ο[,]Ο)) & β’ (π β Β¬ 0 β (π΄[,]π΅)) & β’ (π β (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))):((π + π΄)(,)(π + π΅))βΆβ) & β’ (π β π· β β) & β’ ((π β§ π‘ β ((π + π΄)(,)(π + π΅))) β (absβ(πΉβπ‘)) β€ π·) & β’ (π β πΈ β β) & β’ ((π β§ π‘ β ((π + π΄)(,)(π + π΅))) β (absβ((β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))βπ‘)) β€ πΈ) & β’ (π β πΆ β β) & β’ π = (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))) β β’ (π β (dom (β D π) = (π΄(,)π΅) β§ βπ β β βπ β dom (β D π)(absβ((β D π)βπ )) β€ π)) | ||
Theorem | fourierdlem69 44976* | A piecewise continuous function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΉ:(π΄[,]π΅)βΆβ) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β β’ (π β πΉ β πΏ1) | ||
Theorem | fourierdlem70 44977* | A piecewise continuous function is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ:(π΄[,]π΅)βΆβ) & β’ (π β π β β) & β’ (π β π:(0...π)βΆβ) & β’ (π β (πβ0) = π΄) & β’ (π β (πβπ) = π΅) & β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ πΌ = (π β (0..^π) β¦ ((πβπ)(,)(πβ(π + 1)))) β β’ (π β βπ₯ β β βπ β (π΄[,]π΅)(absβ(πΉβπ )) β€ π₯) | ||
Theorem | fourierdlem71 44978* | A periodic piecewise continuous function, possibly undefined on a finite set in each periodic interval, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β dom πΉ β β) & β’ (π β πΉ:dom πΉβΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π:(0...π)βΆβ) & β’ (π β (πβ0) = π΄) & β’ (π β (πβπ) = π΅) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ (((π β§ π₯ β dom πΉ) β§ π β β€) β (π₯ + (π Β· π)) β dom πΉ) & β’ (((π β§ π₯ β dom πΉ) β§ π β β€) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) & β’ πΌ = (π β (0..^π) β¦ ((πβπ)(,)(πβ(π + 1)))) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) β β’ (π β βπ¦ β β βπ₯ β dom πΉ(absβ(πΉβπ₯)) β€ π¦) | ||
Theorem | fourierdlem72 44979* | The derivative of π is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β (π΄(,)π΅) β (-Ο[,]Ο)) & β’ (π β Β¬ 0 β (π΄[,]π΅)) & β’ (π β πΆ β β) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ (π β π β (0..^π)) & β’ (π β (π΄(,)π΅) β ((πβπ)(,)(πβ(π + 1)))) & β’ π» = (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / π )) & β’ πΎ = (π β (π΄(,)π΅) β¦ (π / (2 Β· (sinβ(π / 2))))) & β’ π = (π β (π΄(,)π΅) β¦ ((π»βπ ) Β· (πΎβπ ))) β β’ (π β (β D π) β ((π΄(,)π΅)βcnββ)) | ||
Theorem | fourierdlem73 44980* | A version of the Riemann Lebesgue lemma: as π increases, the integral in π goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄[,]π΅)βΆβ) & β’ (π β π β β) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ (π β (πβ0) = π΄) & β’ (π β (πβπ) = π΅) & β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ πΊ = (β D πΉ) & β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ (π β βπ¦ β β βπ₯ β dom πΊ(absβ(πΊβπ₯)) β€ π¦) & β’ π = (π β β+ β¦ β«(π΄(,)π΅)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯) & β’ π· = (π₯ β ((πβπ)[,](πβ(π + 1))) β¦ if(π₯ = (πβπ), π , if(π₯ = (πβ(π + 1)), πΏ, (πΉβπ₯)))) β β’ (π β βπ β β+ βπ β β βπ β (π(,)+β)(absββ«(π΄(,)π΅)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯) < π) | ||
Theorem | fourierdlem74 44981* | Given a piecewise smooth function πΉ, the derived function π» has a limit at the upper bound of each interval of the partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β πΉ:ββΆβ) & β’ (π β π β ran π) & β’ (π β π β β) & β’ (π β π β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ πΊ = (β D πΉ) & β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) & β’ (π β πΈ β ((πΊ βΎ (-β(,)π)) limβ π)) & β’ π΄ = if((πβ(π + 1)) = π, πΈ, ((π β if((πβ(π + 1)) < π, π, π)) / (πβ(π + 1)))) β β’ ((π β§ π β (0..^π)) β π΄ β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) | ||
Theorem | fourierdlem75 44982* | Given a piecewise smooth function πΉ, the derived function π» has a limit at the lower bound of each interval of the partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β πΉ:ββΆβ) & β’ (π β π β ran π) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ πΊ = (β D πΉ) & β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) & β’ (π β πΈ β ((πΊ βΎ (π(,)+β)) limβ π)) & β’ π΄ = if((πβπ) = π, πΈ, ((π β if((πβπ) < π, π, π)) / (πβπ))) β β’ ((π β§ π β (0..^π)) β π΄ β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) | ||
Theorem | fourierdlem76 44983* | Continuity of π and its limits with respect to the π partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β (π΄[,]π΅) β (-Ο[,]Ο)) & β’ (π β Β¬ 0 β (π΄[,]π΅)) & β’ (π β πΆ β β) & β’ π = (π β (π΄[,]π΅) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ π = ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) & β’ π = ((β―βπ) β 1) & β’ π = (β©ππ Isom < , < ((0...π), π)) & β’ π· = (((if((πβ(π + 1)) = (πβ(π + 1)), πΏ, (πΉβ(π + (πβ(π + 1))))) β πΆ) / (πβ(π + 1))) Β· ((πβ(π + 1)) / (2 Β· (sinβ((πβ(π + 1)) / 2))))) & β’ πΈ = (((if((πβπ) = (πβπ), π , (πΉβ(π + (πβπ)))) β πΆ) / (πβπ)) Β· ((πβπ) / (2 Β· (sinβ((πβπ) / 2))))) & β’ (π β (((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1))))) β β’ ((((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β ((π· β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) β§ πΈ β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) β§ (π βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ))) | ||
Theorem | fourierdlem77 44984* | If π» is bounded, then π is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) & β’ (π β βπ β β βπ β (-Ο[,]Ο)(absβ(π»βπ )) β€ π) β β’ (π β βπ β β+ βπ β (-Ο[,]Ο)(absβ(πβπ )) β€ π) | ||
Theorem | fourierdlem78 44985* | πΊ is continuous when restricted on an interval not containing 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π΄ β (-Ο[,]Ο)) & β’ (π β π΅ β (-Ο[,]Ο)) & β’ (π β π β β) & β’ (π β Β¬ 0 β (π΄(,)π΅)) & β’ (π β (πΉ βΎ ((π΄ + π)(,)(π΅ + π))) β (((π΄ + π)(,)(π΅ + π))βcnββ)) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) & β’ (π β π β β) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) & β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) β β’ (π β (πΊ βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) | ||
Theorem | fourierdlem79 44986* | πΈ projects every interval of the partition induced by π on π» into a corresponding interval of the partition induced by π on [π΄, π΅]. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π΅ β π΄) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π» = ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ πΏ = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) & β’ π = ((πβπ) + if(((πβ(π + 1)) β (πβπ)) < ((πβ1) β π΄), (((πβ(π + 1)) β (πβπ)) / 2), (((πβ1) β π΄) / 2))) & β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}, β, < )) β β’ ((π β§ π β (0..^π)) β ((πΏβ(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))) β ((πβ(πΌβ(πβπ)))(,)(πβ((πΌβ(πβπ)) + 1)))) | ||
Theorem | fourierdlem80 44987* | The derivative of π is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄[,]π΅) β (-Ο[,]Ο)) & β’ (π β Β¬ 0 β (π΄[,]π΅)) & β’ (π β πΆ β β) & β’ π = (π β (π΄[,]π΅) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))) & β’ πΌ = ((π + (πβπ))(,)(π + (πβ(π + 1)))) & β’ ((π β§ π β (0..^π)) β βπ€ β β βπ‘ β πΌ (absβ(πΉβπ‘)) β€ π€) & β’ ((π β§ π β (0..^π)) β βπ§ β β βπ‘ β πΌ (absβ((β D (πΉ βΎ πΌ))βπ‘)) β€ π§) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π β (0..^π)) β ((πβπ)[,](πβ(π + 1))) β (π΄[,]π΅)) & β’ (((π β§ π β (π΄[,]π΅)) β§ Β¬ π β ran π) β βπ β (0..^π)π β ((πβπ)(,)(πβ(π + 1)))) & β’ ((π β§ π β (0..^π)) β (β D (πΉ βΎ πΌ)):πΌβΆβ) & β’ π = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β πΆ) / (2 Β· (sinβ(π / 2))))) & β’ (π β (((((π β§ π β (0..^π)) β§ π€ β β) β§ π§ β β) β§ βπ‘ β πΌ (absβ(πΉβπ‘)) β€ π€) β§ βπ‘ β πΌ (absβ((β D (πΉ βΎ πΌ))βπ‘)) β€ π§)) β β’ (π β βπ β β βπ β dom (β D π)(absβ((β D π)βπ )) β€ π) | ||
Theorem | fourierdlem81 44988* | The integral of a piecewise continuous periodic function πΉ is unchanged if the domain is shifted by its period π. In this lemma, π is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β β+) & β’ (π β π β (πβπ)) & β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ π = (π β (0...π) β¦ ((πβπ) + π)) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ πΊ = (π₯ β ((πβπ)[,](πβ(π + 1))) β¦ if(π₯ = (πβπ), π , if(π₯ = (πβ(π + 1)), πΏ, (πΉβπ₯)))) & β’ π» = (π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (πΊβ(π₯ β π))) β β’ (π β β«((π΄ + π)[,](π΅ + π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | fourierdlem82 44989* | Integral by substitution, adding a constant to the function's argument, for a function on an open interval with finite limits ad boundary points. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, ((πΉ βΎ (π΄(,)π΅))βπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄[,]π΅)βΆβ) & β’ (π β (πΉ βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) & β’ (π β π β β) β β’ (π β β«(π΄[,]π΅)(πΉβπ‘) dπ‘ = β«((π΄ β π)[,](π΅ β π))(πΉβ(π + π‘)) dπ‘) | ||
Theorem | fourierdlem83 44990* | The fourier partial sum for πΉ rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ πΆ = (-Ο(,)Ο) & β’ (π β (πΉ βΎ πΆ) β πΏ1) & β’ π΄ = (π β β0 β¦ (β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) & β’ (π β π β β) & β’ π = (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) & β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) & β’ (π β π β β) β β’ (π β (πβπ) = β«πΆ((πΉβπ₯) Β· ((π·βπ)β(π₯ β π))) dπ₯) | ||
Theorem | fourierdlem84 44991* | If πΉ is piecewise coninuous and π· is continuous, then πΊ is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (π΄ + π) β§ (πβπ) = (π΅ + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π· β (ββcnββ)) & β’ πΊ = (π β (π΄[,]π΅) β¦ ((πΉβ(π + π )) Β· (π·βπ ))) β β’ (π β πΊ β πΏ1) | ||
Theorem | fourierdlem85 44992* | Limit of the function πΊ at the lower bounds of the partition intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β πΉ:ββΆβ) & β’ (π β π β ran π) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) & β’ (π β π β β) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) & β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ πΌ = (β D πΉ) & β’ ((π β§ π β (0..^π)) β (πΌ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) & β’ (π β πΈ β ((πΌ βΎ (π(,)+β)) limβ π)) & β’ π΄ = ((if((πβπ) = π, πΈ, ((π β if((πβπ) < π, π, π)) / (πβπ))) Β· (πΎβ(πβπ))) Β· (πβ(πβπ))) β β’ ((π β§ π β (0..^π)) β π΄ β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) | ||
Theorem | fourierdlem86 44993* | Continuity of π and its limits with respect to the π partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β (π΄[,]π΅) β (-Ο[,]Ο)) & β’ (π β Β¬ 0 β (π΄[,]π΅)) & β’ (π β πΆ β β) & β’ π = (π β (π΄[,]π΅) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ π = ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) & β’ π = ((β―βπ) β 1) & β’ π = (β©ππ Isom < , < ((0...π), π)) & β’ π· = (((if((πβ(π + 1)) = (πβ(π + 1)), β¦π / πβ¦πΏ, (πΉβ(π + (πβ(π + 1))))) β πΆ) / (πβ(π + 1))) Β· ((πβ(π + 1)) / (2 Β· (sinβ((πβ(π + 1)) / 2))))) & β’ πΈ = (((if((πβπ) = (πβπ), β¦π / πβ¦π , (πΉβ(π + (πβπ)))) β πΆ) / (πβπ)) Β· ((πβπ) / (2 Β· (sinβ((πβπ) / 2))))) & β’ π = (β©π β (0..^π)((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β β’ ((π β§ π β (0..^π)) β ((π· β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) β§ πΈ β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) β§ (π βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ))) | ||
Theorem | fourierdlem87 44994* | The integral of πΊ goes uniformly ( with respect to π) to zero if the measure of the domain of integration goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) & β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) & β’ (π β βπ₯ β β βπ β (-Ο[,]Ο)(absβ(π»βπ )) β€ π₯) & β’ ((π β§ π β β) β πΊ β πΏ1) & β’ π· = ((π / 3) / π) & β’ (π β (((((π β§ π β β+) β§ π β β+ β§ βπ β β βπ β (-Ο[,]Ο)(absβ(πΊβπ )) β€ π) β§ π’ β dom vol) β§ (π’ β (-Ο[,]Ο) β§ (volβπ’) β€ π·)) β§ π β β)) β β’ ((π β§ π β β+) β βπ β β+ βπ’ β dom vol((π’ β (-Ο[,]Ο) β§ (volβπ’) β€ π) β βπ β β (absββ«π’((πβπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2))) | ||
Theorem | fourierdlem88 44995* | Given a piecewise continuous function πΉ, a continuous function πΎ and a continuous function π, the function πΊ is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β πΉ:ββΆβ) & β’ (π β π β ran π) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ (π β π β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) & β’ (π β π β β) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) & β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ πΌ = (β D πΉ) & β’ ((π β§ π β (0..^π)) β (πΌ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) & β’ (π β πΆ β ((πΌ βΎ (-β(,)π)) limβ π)) & β’ (π β π· β ((πΌ βΎ (π(,)+β)) limβ π)) β β’ (π β πΊ β πΏ1) | ||
Theorem | fourierdlem89 44996* | Given a piecewise continuous function and changing the interval and the partition, the limit at the lower bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ (π β πΆ β β) & β’ (π β π· β (πΆ(,)+β)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π» = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ π = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) & β’ (π β π½ β (0..^π)) & β’ π = ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) & β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (πβ(πΈβπ₯))}, β, < )) & β’ π = (π β (0..^π) β¦ π ) β β’ (π β if((πβ(πΈβ(πβπ½))) = (πβ(πΌβ(πβπ½))), (πβ(πΌβ(πβπ½))), (πΉβ(πβ(πΈβ(πβπ½))))) β ((πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) limβ (πβπ½))) | ||
Theorem | fourierdlem90 44997* | Given a piecewise continuous function, it is still continuous with respect to an open interval of the moved partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ (π β πΆ β β) & β’ (π β π· β (πΆ(,)+β)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π» = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ πΏ = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) & β’ (π β π½ β (0..^π)) & β’ π = ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) & β’ πΊ = (πΉ βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) & β’ π = (π¦ β (((πΏβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) β¦ (πΊβ(π¦ β π))) & β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}, β, < )) β β’ (π β (πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) β (((πβπ½)(,)(πβ(π½ + 1)))βcnββ)) | ||
Theorem | fourierdlem91 44998* | Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ (π β πΆ β β) & β’ (π β π· β (πΆ(,)+β)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π» = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ π = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) & β’ (π β π½ β (0..^π)) & β’ π = ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) & β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (πβ(πΈβπ₯))}, β, < )) & β’ π = (π β (0..^π) β¦ πΏ) β β’ (π β if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), (πΉβ(πΈβ(πβ(π½ + 1))))) β ((πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) limβ (πβ(π½ + 1)))) | ||
Theorem | fourierdlem92 44999* | The integral of a piecewise continuous periodic function πΉ is unchanged if the domain is shifted by its period π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ π = (π β (0...π) β¦ ((πβπ) + π)) & β’ π» = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (π΄ + π) β§ (πβπ) = (π΅ + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β β’ (π β β«((π΄ + π)[,](π΅ + π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | fourierdlem93 45000* | Integral by substitution (the domain is shifted by π) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π» = (π β (0...π) β¦ ((πβπ) β π)) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β π β β) & β’ (π β πΉ:(-Ο[,]Ο)βΆβ) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β β’ (π β β«(-Ο[,]Ο)(πΉβπ‘) dπ‘ = β«((-Ο β π)[,](Ο β π))(πΉβ(π + π )) dπ ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |