![]() |
Metamath
Proof Explorer Theorem List (p. 452 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | stirlinglem13 45101* | π΅ is decreasing and has a lower bound, then it converges. Since π΅ is logπ΄, in another theorem it is proven that π΄ converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) β β’ βπ β β π΅ β π | ||
Theorem | stirlinglem14 45102* | The sequence π΄ converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for Ο& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) β β’ βπ β β+ π΄ β π | ||
Theorem | stirlinglem15 45103* | The Stirling's formula is proven using a number of local definitions. The main theorem stirling 45104 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ π = (π β β0 β¦ ((ββ((2 Β· Ο) Β· π)) Β· ((π / e)βπ))) & β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π· = (π β β β¦ (π΄β(2 Β· π))) & β’ πΈ = (π β β β¦ ((ββ(2 Β· π)) Β· ((π / e)βπ))) & β’ π = (π β β β¦ ((((2β(4 Β· π)) Β· ((!βπ)β4)) / ((!β(2 Β· π))β2)) / ((2 Β· π) + 1))) & β’ πΉ = (π β β β¦ (((π΄βπ)β4) / ((π·βπ)β2))) & β’ π» = (π β β β¦ ((πβ2) / (π Β· ((2 Β· π) + 1)))) & β’ (π β πΆ β β+) & β’ (π β π΄ β πΆ) β β’ (π β (π β β β¦ ((!βπ) / (πβπ))) β 1) | ||
Theorem | stirling 45104 | Stirling's approximation formula for π factorial. The proof follows two major steps: first it is proven that π and π factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for Ο it is proven that the unknown constant is the square root of Ο and then the exact Stirling's formula is established. This is Metamath 100 proof #90. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (π β β0 β¦ ((ββ((2 Β· Ο) Β· π)) Β· ((π / e)βπ))) β β’ (π β β β¦ ((!βπ) / (πβπ))) β 1 | ||
Theorem | stirlingr 45105 | Stirling's approximation formula for π factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 45104 is proven for convergence in the topology of complex numbers. The variable π is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (π β β0 β¦ ((ββ((2 Β· Ο) Β· π)) Β· ((π / e)βπ))) & β’ π = (βπ‘β(topGenβran (,))) β β’ (π β β β¦ ((!βπ) / (πβπ)))π 1 | ||
Theorem | dirkerval 45106* | The Nth Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) β β’ (π β β β (π·βπ) = (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) | ||
Theorem | dirker2re 45107 | The Dirichlet Kernel value is a real if the argument is not a multiple of Ο . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (((π β β β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0) β ((sinβ((π + (1 / 2)) Β· π)) / ((2 Β· Ο) Β· (sinβ(π / 2)))) β β) | ||
Theorem | dirkerdenne0 45108 | The Dirichlet Kernel denominator is never 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π β β β§ Β¬ (π mod (2 Β· Ο)) = 0) β ((2 Β· Ο) Β· (sinβ(π / 2))) β 0) | ||
Theorem | dirkerval2 45109* | The Nth Dirichlet Kernel evaluated at a specific point π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) β β’ ((π β β β§ π β β) β ((π·βπ)βπ) = if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π)) / ((2 Β· Ο) Β· (sinβ(π / 2)))))) | ||
Theorem | dirkerre 45110* | The Dirichlet Kernel at any point evaluates to a real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) β β’ ((π β β β§ π β β) β ((π·βπ)βπ) β β) | ||
Theorem | dirkerper 45111* | the Dirichlet Kernel has period 2Ο. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ π = (2 Β· Ο) β β’ ((π β β β§ π₯ β β) β ((π·βπ)β(π₯ + π)) = ((π·βπ)βπ₯)) | ||
Theorem | dirkerf 45112* | For any natural number π, the Dirichlet Kernel (π·βπ) is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) β β’ (π β β β (π·βπ):ββΆβ) | ||
Theorem | dirkertrigeqlem1 45113* | Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (πΎ β β β Ξ£π β (1...(2 Β· πΎ))(cosβ(π Β· Ο)) = 0) | ||
Theorem | dirkertrigeqlem2 45114* | Trigonomic equality lemma for the Dirichlet Kernel trigonomic equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β (sinβπ΄) β 0) & β’ (π β π β β) β β’ (π β (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π΄))) / Ο) = ((sinβ((π + (1 / 2)) Β· π΄)) / ((2 Β· Ο) Β· (sinβ(π΄ / 2))))) | ||
Theorem | dirkertrigeqlem3 45115* | 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 45116* | 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 45117* | 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 45118* | 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 45119* | 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 45120* | 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 45121* | 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 45122* | 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 45123 | A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ (π β πΌ β (0..^π)) & β’ (π β π β ((πβπΌ)[,](πβ(πΌ + 1)))) β β’ (π β π β (π΄[,]π΅)) | ||
Theorem | fourierdlem2 45124* | Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) β β’ (π β β β (π β (πβπ) β (π β (β βm (0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) | ||
Theorem | fourierdlem3 45125* | Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β ((-Ο[,]Ο) βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) β β’ (π β β β (π β (πβπ) β (π β ((-Ο[,]Ο) βm (0...π)) β§ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) | ||
Theorem | fourierdlem4 45126* | πΈ is a function that maps any point to a periodic corresponding point in (π΄, π΅]. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) β β’ (π β πΈ:ββΆ(π΄(,]π΅)) | ||
Theorem | fourierdlem5 45127* | π is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π₯ β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π₯))) β β’ (π β β β π:(-Ο[,]Ο)βΆβ) | ||
Theorem | fourierdlem6 45128 | π is in the periodic partition, when the considered interval is centered at π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β πΌ β β€) & β’ (π β π½ β β€) & β’ (π β πΌ < π½) & β’ (π β (π + (πΌ Β· π)) β (π΄[,]π΅)) & β’ (π β (π + (π½ Β· π)) β (π΄[,]π΅)) β β’ (π β π½ = (πΌ + 1)) | ||
Theorem | fourierdlem7 45129* | The difference between the periodic sawtooth function and the identity function is decreasing. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) β β’ (π β ((πΈβπ) β π) β€ ((πΈβπ) β π)) | ||
Theorem | fourierdlem8 45130 | A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ (π β πΌ β (0..^π)) β β’ (π β ((πβπΌ)[,](πβ(πΌ + 1))) β (π΄[,]π΅)) | ||
Theorem | fourierdlem9 45131* | π» is a complex function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) β β’ (π β π»:(-Ο[,]Ο)βΆβ) | ||
Theorem | fourierdlem10 45132 | Condition on the bounds of a nonempty subinterval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΆ < π·) & β’ (π β (πΆ(,)π·) β (π΄(,)π΅)) β β’ (π β (π΄ β€ πΆ β§ π· β€ π΅)) | ||
Theorem | fourierdlem11 45133* | 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 45134* | 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 45135* | Value of π in terms of value of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (π΄ + π) β§ (πβπ) = (π΅ + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΌ β (0...π)) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) β β’ (π β ((πβπΌ) = ((πβπΌ) β π) β§ (πβπΌ) = (π + (πβπΌ)))) | ||
Theorem | fourierdlem14 45136* | 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 45137* | 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 45138* | 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 45139* | The defined πΏ is actually a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ πΏ = (π₯ β (π΄(,]π΅) β¦ if(π₯ = π΅, π΄, π₯)) β β’ (π β πΏ:(π΄(,]π΅)βΆ(π΄[,]π΅)) | ||
Theorem | fourierdlem18 45140* | The function π is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) β β’ (π β π β ((-Ο[,]Ο)βcnββ)) | ||
Theorem | fourierdlem19 45141* | If two elements of π· have the same periodic image in (π΄(,]π΅) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β π β β) & β’ π· = {π¦ β ((π΄ + π)(,](π΅ + π)) β£ βπ β β€ (π¦ + (π Β· π)) β πΆ} & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β π β π·) & β’ (π β π β π·) & β’ (π β (πΈβπ) = (πΈβπ)) β β’ (π β Β¬ π < π) | ||
Theorem | fourierdlem20 45142* | 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 45143* | 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 45144* | 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 45145* | If πΉ is continuous and π is constant, then (πΉβ(π + π )) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ ((π β§ π β π΅) β (π + π ) β π΄) β β’ (π β (π β π΅ β¦ (πΉβ(π + π ))) β (π΅βcnββ)) | ||
Theorem | fourierdlem24 45146 | A sufficient condition for module being nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β ((-Ο[,]Ο) β {0}) β (π΄ mod (2 Β· Ο)) β 0) | ||
Theorem | fourierdlem25 45147* | 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 45148* | Periodic image of a point π that's in the period that begins with the point π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ (π β π β β) & β’ (π β (πΈβπ) = π΅) & β’ (π β π β (π(,](π + π))) β β’ (π β (πΈβπ) = (π΄ + (π β π))) | ||
Theorem | fourierdlem27 45149 | A partition open interval is a subset of the partitioned open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π:(0...π)βΆ(π΄[,]π΅)) & β’ (π β πΌ β (0..^π)) β β’ (π β ((πβπΌ)(,)(πβ(πΌ + 1))) β (π΄(,)π΅)) | ||
Theorem | fourierdlem28 45150* | Derivative of (πΉβ(π + π )). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ π· = (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))) & β’ (π β π·:((π + π΄)(,)(π + π΅))βΆβ) β β’ (π β (β D (π β (π΄(,)π΅) β¦ (πΉβ(π + π )))) = (π β (π΄(,)π΅) β¦ (π·β(π + π )))) | ||
Theorem | fourierdlem29 45151* | 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 45152* | 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 45153* | 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 45154 | 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 45155 | 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 45156* | A partition is one to one. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) β β’ (π β π:(0...π)β1-1ββ) | ||
Theorem | fourierdlem35 45157 | There is a single point in (π΄(,]π΅) that's distant from π a multiple integer of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β πΌ β β€) & β’ (π β π½ β β€) & β’ (π β (π + (πΌ Β· π)) β (π΄(,]π΅)) & β’ (π β (π + (π½ Β· π)) β (π΄(,]π΅)) β β’ (π β πΌ = π½) | ||
Theorem | fourierdlem36 45158* | πΉ is an isomorphism. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β Fin) & β’ (π β π΄ β β) & β’ πΉ = (β©ππ Isom < , < ((0...π), π΄)) & β’ π = ((β―βπ΄) β 1) β β’ (π β πΉ Isom < , < ((0...π), π΄)) | ||
Theorem | fourierdlem37 45159* | πΌ 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 45160* | 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 45161* | 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 45162* | π» 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 45163* | 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 45164* | 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 45165 | πΎ is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) β β’ πΎ:(-Ο[,]Ο)βΆβ | ||
Theorem | fourierdlem44 45166 | A condition for having (sinβ(π΄ / 2)) nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β (-Ο[,]Ο) β§ π΄ β 0) β (sinβ(π΄ / 2)) β 0) | ||
Theorem | fourierdlem46 45167* | 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 45168* | 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 45169* | 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 45170* | 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 45171* | 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 45172* | π 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 45173* | d16:d17,d18:jca |- ( ph -> ( ( S 0) β€ π΄ β§ π΄ β€ (π 0 ) ) ) . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β Fin) & β’ π = ((β―βπ) β 1) & β’ π = (β©ππ Isom < , < ((0...π), π)) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β (π΄[,]π΅)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β ((π:(0...π)βΆ(π΄[,]π΅) β§ (πβ0) = π΄) β§ (πβπ) = π΅)) | ||
Theorem | fourierdlem53 45174* | The limit of πΉ(π ) at (π + π·) is the limit of πΉ(π + π ) at π·. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ πΊ = (π β π΄ β¦ (πΉβ(π + π ))) & β’ ((π β§ π β π΄) β (π + π ) β π΅) & β’ (π β π΅ β β) & β’ ((π β§ π β π΄) β π β π·) & β’ (π β πΆ β ((πΉ βΎ π΅) limβ (π + π·))) & β’ (π β π· β β) β β’ (π β πΆ β (πΊ limβ π·)) | ||
Theorem | fourierdlem54 45175* | 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 45176* | π is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) β β’ (π β π:(-Ο[,]Ο)βΆβ) | ||
Theorem | fourierdlem56 45177* | 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 45178* | 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 45179* | 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 45180* | The derivative of π» is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β Β¬ 0 β (π΄(,)π΅)) & β’ (π β (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))) β (((π + π΄)(,)(π + π΅))βcnββ)) & β’ (π β πΆ β β) & β’ π» = (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β πΆ) / π )) β β’ (π β (β D π») β ((π΄(,)π΅)βcnββ)) | ||
Theorem | fourierdlem60 45181* | 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 45182* | 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 45183 | The function πΎ is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (π¦ β (-Ο[,]Ο) β¦ if(π¦ = 0, 1, (π¦ / (2 Β· (sinβ(π¦ / 2)))))) β β’ πΎ β ((-Ο[,]Ο)βcnββ) | ||
Theorem | fourierdlem63 45184* | 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 45185* | 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 45186* | 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 45187* | 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 45188* | πΊ 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 45189* | 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 45190* | 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 45191* | 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 45192* | 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 45193* | 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 45194* | 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 45195* | 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 45196* | 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 45197* | 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 45198* | 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 45199* | πΊ 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 45200* | πΈ 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)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |