![]() |
Metamath
Proof Explorer Theorem List (p. 450 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fourierdlem79 44901* | πΈ 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 44902* | 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 44903* | 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 44904* | 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 44905* | 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 44906* | 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 44907* | 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 44908* | 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 44909* | 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 44910* | 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 44911* | 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 44912* | 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 44913* | 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 44914* | 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 44915* | 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π ) | ||
Theorem | fourierdlem94 44916* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) β β ) & β’ ((π β§ π β (0..^π)) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) β β ) β β’ (π β (((πΉ βΎ (-β(,)π)) limβ π) β β β§ ((πΉ βΎ (π(,)+β)) limβ π) β β )) | ||
Theorem | fourierdlem95 44917* | Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β π β ran π) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) & β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) & β’ πΌ = (β D πΉ) & β’ ((π β§ π β (0..^π)) β (πΌ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) & β’ (π β π΅ β ((πΌ βΎ (-β(,)π)) limβ π)) & β’ (π β πΆ β ((πΌ βΎ (π(,)+β)) limβ π)) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ (π β π β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ (π β π΄ β dom vol) & β’ (π β π΄ β ((-Ο[,]Ο) β {0})) & β’ πΈ = (π β β β¦ (β«π΄(πΊβπ ) dπ / Ο)) & β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) & β’ (π β π β β) & β’ ((π β§ π β π΄) β if(0 < π , π, π) = π) & β’ ((π β§ π β β) β β«π΄((π·βπ)βπ ) dπ = (1 / 2)) β β’ ((π β§ π β β) β ((πΈβπ) + (π / 2)) = β«π΄((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) | ||
Theorem | fourierdlem96 44918* | limit for πΉ at the lower bound of an interval for the moved partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ (π β πΆ β β) & β’ (π β π· β (πΆ(,)+β)) & β’ (π β π½ β (0..^((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1))) & β’ π = (β©ππ Isom < , < ((0...((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ ββ β β€ (π¦ + (β Β· π)) β ran π}))) β β’ (π β if(((π’ β (π΄(,]π΅) β¦ if(π’ = π΅, π΄, π’))β((π£ β β β¦ (π£ + ((ββ((π΅ β π£) / π)) Β· π)))β(πβπ½))) = (πβ((π¦ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ ((π’ β (π΄(,]π΅) β¦ if(π’ = π΅, π΄, π’))β((π£ β β β¦ (π£ + ((ββ((π΅ β π£) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ½))), ((π β (0..^π) β¦ π )β((π¦ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ ((π’ β (π΄(,]π΅) β¦ if(π’ = π΅, π΄, π’))β((π£ β β β¦ (π£ + ((ββ((π΅ β π£) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ½))), (πΉβ((π’ β (π΄(,]π΅) β¦ if(π’ = π΅, π΄, π’))β((π£ β β β¦ (π£ + ((ββ((π΅ β π£) / π)) Β· π)))β(πβπ½))))) β ((πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) limβ (πβπ½))) | ||
Theorem | fourierdlem97 44919* | πΉ is continuous on the intervals induced by the moved partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ πΊ = (β D πΉ) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π΅ β β) & β’ (π β π΄ β β) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ (π β πΆ β β) & β’ (π β π· β (πΆ(,)+β)) & β’ (π β π½ β (0..^((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1))) & β’ π = (β©ππ Isom < , < ((0...((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ ββ β β€ (π¦ + (β Β· π)) β ran π}))) & β’ π» = (π β β β¦ if(π β dom πΊ, (πΊβπ ), 0)) β β’ (π β (πΊ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) β (((πβπ½)(,)(πβ(π½ + 1)))βcnββ)) | ||
Theorem | fourierdlem98 44920* | πΉ is continuous on the intervals induced by the moved partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ (π β πΆ β β) & β’ (π β π· β (πΆ(,)+β)) & β’ (π β π½ β (0..^((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1))) & β’ π = (β©ππ Isom < , < ((0...((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ ββ β β€ (π¦ + (β Β· π)) β ran π}))) β β’ (π β (πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) β (((πβπ½)(,)(πβ(π½ + 1)))βcnββ)) | ||
Theorem | fourierdlem99 44921* | limit for πΉ at the upper bound of an interval for the moved partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ (π β πΆ β β) & β’ (π β π· β (πΆ(,)+β)) & β’ (π β π½ β (0..^((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1))) & β’ π = (β©ππ Isom < , < ((0...((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ ββ β β€ (π¦ + (β Β· π)) β ran π}))) β β’ (π β if(((π£ β β β¦ (π£ + ((ββ((π΅ β π£) / π)) Β· π)))β(πβ(π½ + 1))) = (πβ(((π¦ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ ((π’ β (π΄(,]π΅) β¦ if(π’ = π΅, π΄, π’))β((π£ β β β¦ (π£ + ((ββ((π΅ β π£) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ½)) + 1)), ((π β (0..^π) β¦ πΏ)β((π¦ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ ((π’ β (π΄(,]π΅) β¦ if(π’ = π΅, π΄, π’))β((π£ β β β¦ (π£ + ((ββ((π΅ β π£) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ½))), (πΉβ((π£ β β β¦ (π£ + ((ββ((π΅ β π£) / π)) Β· π)))β(πβ(π½ + 1))))) β ((πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) limβ (πβ(π½ + 1)))) | ||
Theorem | fourierdlem100 44922* | A piecewise continuous function is integrable on any closed interval. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ (π β πΆ β β) & β’ (π β π· β (πΆ(,)+β)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = ((β―βπ») β 1) & β’ π» = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) & β’ π = (β©ππ Isom < , < ((0...π), π»)) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ π½ = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) & β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (π½β(πΈβπ₯))}, β, < )) β β’ (π β (π₯ β (πΆ[,]π·) β¦ (πΉβπ₯)) β πΏ1) | ||
Theorem | fourierdlem101 44923* | Integral by substitution for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ πΊ = (π‘ β (-Ο[,]Ο) β¦ ((πΉβπ‘) Β· ((π·βπ)β(π‘ β π)))) & β’ (π β π β (πβπ)) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΉ:(-Ο[,]Ο)βΆβ) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β β’ (π β β«(-Ο[,]Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘ = β«((-Ο β π)[,](Ο β π))((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) | ||
Theorem | fourierdlem102 44924* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ (π β ((-Ο(,)Ο) β dom πΊ) β Fin) & β’ (π β πΊ β (dom πΊβcnββ)) & β’ ((π β§ π₯ β ((-Ο[,)Ο) β dom πΊ)) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ ((π β§ π₯ β ((-Ο(,]Ο) β dom πΊ)) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((Ο β π₯) / π)) Β· π))) & β’ π» = ({-Ο, Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β dom πΊ)) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) β β’ (π β (((πΉ βΎ (-β(,)π)) limβ π) β β β§ ((πΉ βΎ (π(,)+β)) limβ π) β β )) | ||
Theorem | fourierdlem103 44925* | The half lower part of the integral equal to the fourier partial sum, converges to half the left limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β π β ran π) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β βπ€ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ‘)) β€ π€) & β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β βπ§ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ((β D πΉ)βπ‘)) β€ π§) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) & β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) & β’ π = (π β β β¦ β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) & β’ πΈ = (π β β β¦ (β«(-Ο(,)0)(πΊβπ ) dπ / Ο)) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ (π β π β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ (π β π΄ β (((β D πΉ) βΎ (-β(,)π)) limβ π)) & β’ (π β π΅ β (((β D πΉ) βΎ (π(,)+β)) limβ π)) & β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) & β’ π = (π βΎ (-Ο[,]π)) & β’ π = ({-Ο, π} βͺ (ran π β© (-Ο(,)π))) & β’ π = ((β―βπ) β 1) & β’ π½ = (β©ππ Isom < , < ((0...π), π)) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ πΆ = (β©π β (0..^π)((π½βπ)(,)(π½β(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) & β’ (π β (((((π β§ π β β+) β§ π β (-Ο(,)0)) β§ π β β) β§ (absββ«(π(,)0)((πβπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2)) β§ (absββ«(-Ο(,)π)((πβπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2))) β β’ (π β π β (π / 2)) | ||
Theorem | fourierdlem104 44926* | The half upper part of the integral equal to the fourier partial sum, converges to half the right limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β π β ran π) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β βπ€ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ‘)) β€ π€) & β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β βπ§ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ((β D πΉ)βπ‘)) β€ π§) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) & β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) & β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) & β’ π = (π β (-Ο[,]Ο) β¦ (sinβ((π + (1 / 2)) Β· π ))) & β’ πΊ = (π β (-Ο[,]Ο) β¦ ((πβπ ) Β· (πβπ ))) & β’ π = (π β β β¦ β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) & β’ πΈ = (π β β β¦ (β«(0(,)Ο)(πΊβπ ) dπ / Ο)) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ (π β π β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ (π β π΄ β (((β D πΉ) βΎ (-β(,)π)) limβ π)) & β’ (π β π΅ β (((β D πΉ) βΎ (π(,)+β)) limβ π)) & β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) & β’ π = (π βΎ (π[,]Ο)) & β’ π = ({π, Ο} βͺ (ran π β© (π(,)Ο))) & β’ π = ((β―βπ) β 1) & β’ π½ = (β©ππ Isom < , < ((0...π), π)) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) & β’ πΆ = (β©π β (0..^π)((π½βπ)(,)(π½β(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) & β’ (π β (((((π β§ π β β+) β§ π β (0(,)Ο)) β§ π β β) β§ (absββ«(0(,)π)((πβπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2)) β§ (absββ«(π(,)Ο)((πβπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2))) β β’ (π β π β (π / 2)) | ||
Theorem | fourierdlem105 44927* | A piecewise continuous function is integrable on any closed interval. (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 | fourierdlem106 44928* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ (π β ((-Ο(,)Ο) β dom πΊ) β Fin) & β’ (π β πΊ β (dom πΊβcnββ)) & β’ ((π β§ π₯ β ((-Ο[,)Ο) β dom πΊ)) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ ((π β§ π₯ β ((-Ο(,]Ο) β dom πΊ)) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ (π β π β β) β β’ (π β (((πΉ βΎ (-β(,)π)) limβ π) β β β§ ((πΉ βΎ (π(,)+β)) limβ π) β β )) | ||
Theorem | fourierdlem107 44929* | The integral of a piecewise continuous periodic function πΉ is unchanged if the domain is shifted by any positive value π. This lemma generalizes fourierdlem92 44914 where the integral was shifted by the exact period. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ π = (π΅ β π΄) & β’ (π β π β β+) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (π΄ β π) β§ (πβπ) = π΄) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π» = ({(π΄ β π), π΄} βͺ {π¦ β ((π΄ β π)[,]π΄) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ π = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) & β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (πβ(πΈβπ₯))}, β, < )) β β’ (π β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | fourierdlem108 44930* | The integral of a piecewise continuous periodic function πΉ is unchanged if the domain is shifted by any positive value π. This lemma generalizes fourierdlem92 44914 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ π = (π΅ β π΄) & β’ (π β π β β+) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β β’ (π β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | fourierdlem109 44931* | The integral of a piecewise continuous periodic function πΉ is unchanged if the domain is shifted by any value π. This lemma generalizes fourierdlem92 44914 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π» = ({(π΄ β π), (π΅ β π)} βͺ {π₯ β ((π΄ β π)[,](π΅ β π)) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) & β’ π½ = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) & β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (π½β(πΈβπ₯))}, β, < )) β β’ (π β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | fourierdlem110 44932* | The integral of a piecewise continuous periodic function πΉ is unchanged if the domain is shifted by any value π. This lemma generalizes fourierdlem92 44914 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ π = (π΅ β π΄) & β’ (π β π β β) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β β’ (π β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | fourierdlem111 44933* | The fourier partial sum for πΉ is the sum of two integrals, with the same integrand involving πΉ and the Dirichlet Kernel π·, but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ‘) Β· (cosβ(π Β· π‘))) dπ‘ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ‘) Β· (sinβ(π Β· π‘))) dπ‘ / Ο)) & β’ π = (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) & β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ (π β π β β) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = (π₯ β β β¦ ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯))) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ π = (2 Β· Ο) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = (-Ο β π) β§ (πβπ) = (Ο β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ π = (π β (0...π) β¦ ((πβπ) β π)) β β’ ((π β§ π β β) β (πβπ) = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )) | ||
Theorem | fourierdlem112 44934* | Here abbreviations (local definitions) are introduced to prove the fourier 44941 theorem. (πβπ) is the mth partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ π = ((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1) & β’ π = (β©ππ Isom < , < ((0...π), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) & β’ (π β π β β) & β’ (π β π β ran π) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β πΆ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) & β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) & β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ (π β πΈ β (((β D πΉ) βΎ (-β(,)π)) limβ π)) & β’ (π β πΌ β (((β D πΉ) βΎ (π(,)+β)) limβ π)) & β’ (π β πΏ β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) & β’ π = (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) & β’ π = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) & β’ (π β βπ€ β β βπ‘ β β (absβ(πΉβπ‘)) β€ π€) & β’ (π β βπ§ β β βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) & β’ (π β π β β) β β’ (π β (seq1( + , π) β (((πΏ + π ) / 2) β ((π΄β0) / 2)) β§ (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π ) / 2))) | ||
Theorem | fourierdlem113 44935* | Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ (π β π β β) & β’ (π β πΏ β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ (π β π β β) & β’ (π β π β (πβπ)) & β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) & β’ ((π β§ π β (0..^π)) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) β β ) & β’ ((π β§ π β (0..^π)) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) β β ) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) & β’ π = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((Ο β π₯) / π)) Β· π))) & β’ (π β (πΈβπ) β ran π) β β’ (π β (seq1( + , π) β (((πΏ + π ) / 2) β ((π΄β0) / 2)) β§ (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π ) / 2))) | ||
Theorem | fourierdlem114 44936* | Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ (π β ((-Ο(,)Ο) β dom πΊ) β Fin) & β’ (π β πΊ β (dom πΊβcnββ)) & β’ ((π β§ π₯ β ((-Ο[,)Ο) β dom πΊ)) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ ((π β§ π₯ β ((-Ο(,]Ο) β dom πΊ)) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ (π β π β β) & β’ (π β πΏ β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) & β’ π = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) & β’ π = (π β β β¦ {π β (β βm (0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) & β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((Ο β π₯) / π)) Β· π))) & β’ π» = ({-Ο, Ο, (πΈβπ)} βͺ ((-Ο[,]Ο) β dom πΊ)) & β’ π = ((β―βπ») β 1) & β’ π = (β©ππ Isom < , < ((0...π), π»)) β β’ (π β (seq1( + , π) β (((πΏ + π ) / 2) β ((π΄β0) / 2)) β§ (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π ) / 2))) | ||
Theorem | fourierdlem115 44937* | Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ (π β ((-Ο(,)Ο) β dom πΊ) β Fin) & β’ (π β πΊ β (dom πΊβcnββ)) & β’ ((π β§ π₯ β ((-Ο[,)Ο) β dom πΊ)) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ ((π β§ π₯ β ((-Ο(,]Ο) β dom πΊ)) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ (π β π β β) & β’ (π β πΏ β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) & β’ π = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β β’ (π β (seq1( + , π) β (((πΏ + π ) / 2) β ((π΄β0) / 2)) β§ (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π ) / 2))) | ||
Theorem | fourierd 44938* | Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 44942. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 44943 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 44948. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ (π β ((-Ο(,)Ο) β dom πΊ) β Fin) & β’ (π β πΊ β (dom πΊβcnββ)) & β’ ((π β§ π₯ β ((-Ο[,)Ο) β dom πΊ)) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ ((π β§ π₯ β ((-Ο(,]Ο) β dom πΊ)) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ (π β π β β) & β’ (π β πΏ β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) β β’ (π β (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π ) / 2)) | ||
Theorem | fourierclimd 44939* | Fourier series convergence, for piecewise smooth functions. See fourierd 44938 for the analogous Ξ£ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ (π β ((-Ο(,)Ο) β dom πΊ) β Fin) & β’ (π β πΊ β (dom πΊβcnββ)) & β’ ((π β§ π₯ β ((-Ο[,)Ο) β dom πΊ)) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ ((π β§ π₯ β ((-Ο(,]Ο) β dom πΊ)) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ (π β π β β) & β’ (π β πΏ β ((πΉ βΎ (-β(,)π)) limβ π)) & β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) & β’ π = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β β’ (π β seq1( + , π) β (((πΏ + π ) / 2) β ((π΄β0) / 2))) | ||
Theorem | fourierclim 44940* | Fourier series convergence, for piecewise smooth functions. See fourier 44941 for the analogous Ξ£ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ:ββΆβ & β’ π = (2 Β· Ο) & β’ (π₯ β β β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ ((-Ο(,)Ο) β dom πΊ) β Fin & β’ πΊ β (dom πΊβcnββ) & β’ (π₯ β ((-Ο[,)Ο) β dom πΊ) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ (π₯ β ((-Ο(,]Ο) β dom πΊ) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ π β β & β’ πΏ β ((πΉ βΎ (-β(,)π)) limβ π) & β’ π β ((πΉ βΎ (π(,)+β)) limβ π) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) & β’ π = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β β’ seq1( + , π) β (((πΏ + π ) / 2) β ((π΄β0) / 2)) | ||
Theorem | fourier 44941* | Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 44942. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 44943 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 44948. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ:ββΆβ & β’ π = (2 Β· Ο) & β’ (π₯ β β β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ ((-Ο(,)Ο) β dom πΊ) β Fin & β’ πΊ β (dom πΊβcnββ) & β’ (π₯ β ((-Ο[,)Ο) β dom πΊ) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ (π₯ β ((-Ο(,]Ο) β dom πΊ) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ π β β & β’ πΏ β ((πΉ βΎ (-β(,)π)) limβ π) & β’ π β ((πΉ βΎ (π(,)+β)) limβ π) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) β β’ (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π ) / 2) | ||
Theorem | fouriercnp 44942* | If πΉ is continuous at the point π, then its Fourier series at π, converges to (πΉβπ). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ (π β ((-Ο(,)Ο) β dom πΊ) β Fin) & β’ (π β πΊ β (dom πΊβcnββ)) & β’ ((π β§ π₯ β ((-Ο[,)Ο) β dom πΊ)) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ ((π β§ π₯ β ((-Ο(,]Ο) β dom πΊ)) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ π½ = (topGenβran (,)) & β’ (π β πΉ β ((π½ CnP π½)βπ)) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) β β’ (π β (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (πΉβπ)) | ||
Theorem | fourier2 44943* | Fourier series convergence, for a piecewise smooth function. Here it is also proven the existence of the left and right limits of πΉ at any given point π. See fourierd 44938 for a comparison. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ (π β ((-Ο(,)Ο) β dom πΊ) β Fin) & β’ (π β πΊ β (dom πΊβcnββ)) & β’ ((π β§ π₯ β ((-Ο[,)Ο) β dom πΊ)) β ((πΊ βΎ (π₯(,)+β)) limβ π₯) β β ) & β’ ((π β§ π₯ β ((-Ο(,]Ο) β dom πΊ)) β ((πΊ βΎ (-β(,)π₯)) limβ π₯) β β ) & β’ (π β π β β) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) β β’ (π β βπ β ((πΉ βΎ (-β(,)π)) limβ π)βπ β ((πΉ βΎ (π(,)+β)) limβ π)(((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((π + π) / 2)) | ||
Theorem | sqwvfoura 44944* | Fourier coefficients for the square wave function. Since the square function is an odd function, there is no contribution from the π΄ coefficients. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (2 Β· Ο) & β’ πΉ = (π₯ β β β¦ if((π₯ mod π) < Ο, 1, -1)) & β’ (π β π β β0) β β’ (π β (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο) = 0) | ||
Theorem | sqwvfourb 44945* | Fourier series π΅ coefficients for the square wave function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (2 Β· Ο) & β’ πΉ = (π₯ β β β¦ if((π₯ mod π) < Ο, 1, -1)) & β’ (π β π β β) β β’ (π β (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο) = if(2 β₯ π, 0, (4 / (π Β· Ο)))) | ||
Theorem | fourierswlem 44946* | The Fourier series for the square wave πΉ converges to π, a simpler expression for this special case. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (2 Β· Ο) & β’ πΉ = (π₯ β β β¦ if((π₯ mod π) < Ο, 1, -1)) & β’ π β β & β’ π = if((π mod Ο) = 0, 0, (πΉβπ)) β β’ π = ((if((π mod π) β (0(,]Ο), 1, -1) + (πΉβπ)) / 2) | ||
Theorem | fouriersw 44947* | Fourier series convergence, for the square wave function. Where πΉ is discontinuous, the series converges to 0, the average value of the left and the right limits. Notice that πΉ is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π = (2 Β· Ο) & β’ πΉ = (π₯ β β β¦ if((π₯ mod π) < Ο, 1, -1)) & β’ π β β & β’ π = (π β β β¦ ((sinβ(((2 Β· π) β 1) Β· π)) / ((2 Β· π) β 1))) & β’ π = if((π mod Ο) = 0, 0, (πΉβπ)) β β’ (((4 / Ο) Β· Ξ£π β β ((sinβ(((2 Β· π) β 1) Β· π)) / ((2 Β· π) β 1))) = π β§ seq1( + , π) β ((Ο / 4) Β· π)) | ||
Theorem | fouriercn 44948* | If the derivative of πΉ is continuous, then the Fourier series for πΉ converges to πΉ everywhere and the hypothesis are simpler than those for the more general case of a piecewise smooth function (see fourierd 44938 for a comparison). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ π = (2 Β· Ο) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ (π β (β D πΉ) β (ββcnββ)) & β’ πΊ = ((β D πΉ) βΎ (-Ο(,)Ο)) & β’ (π β π β β) & β’ π΄ = (π β β0 β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) & β’ π΅ = (π β β β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) β β’ (π β (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (πΉβπ)) | ||
Theorem | elaa2lem 44949* | Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 44950. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 1-Oct-2020.) |
β’ (π β π΄ β πΈ) & β’ (π β π΄ β 0) & β’ (π β πΊ β (Polyββ€)) & β’ (π β πΊ β 0π) & β’ (π β (πΊβπ΄) = 0) & β’ π = inf({π β β0 β£ ((coeffβπΊ)βπ) β 0}, β, < ) & β’ πΌ = (π β β0 β¦ ((coeffβπΊ)β(π + π))) & β’ πΉ = (π§ β β β¦ Ξ£π β (0...((degβπΊ) β π))((πΌβπ) Β· (π§βπ))) β β’ (π β βπ β (Polyββ€)(((coeffβπ)β0) β 0 β§ (πβπ΄) = 0)) | ||
Theorem | elaa2 44950* | Elementhood in the set of nonzero algebraic numbers: when π΄ is nonzero, the polynomial π can be chosen with a nonzero constant term. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Proof shortened by AV, 1-Oct-2020.) |
β’ (π΄ β (πΈ β {0}) β (π΄ β β β§ βπ β (Polyββ€)(((coeffβπ)β0) β 0 β§ (πβπ΄) = 0))) | ||
Theorem | etransclem1 44951* | π» is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ (π β π½ β (0...π)) β β’ (π β (π»βπ½):πβΆβ) | ||
Theorem | etransclem2 44952* | Derivative of πΊ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯πΉ & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π β (0...(π + 1))) β ((β Dπ πΉ)βπ):ββΆβ) & β’ πΊ = (π₯ β β β¦ Ξ£π β (0...π )(((β Dπ πΉ)βπ)βπ₯)) β β’ (π β (β D πΊ) = (π₯ β β β¦ Ξ£π β (0...π )(((β Dπ πΉ)β(π + 1))βπ₯))) | ||
Theorem | etransclem3 44953 | The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β πΆ:(0...π)βΆ(0...π)) & β’ (π β π½ β (0...π)) & β’ (π β πΎ β β€) β β’ (π β if(π < (πΆβπ½), 0, (((!βπ) / (!β(π β (πΆβπ½)))) Β· ((πΎ β π½)β(π β (πΆβπ½))))) β β€) | ||
Theorem | etransclem4 44954* | πΉ expressed as a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π΄ β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ π» = (π β (0...π) β¦ (π₯ β π΄ β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ πΈ = (π₯ β π΄ β¦ βπ β (0...π)((π»βπ)βπ₯)) β β’ (π β πΉ = πΈ) | ||
Theorem | etransclem5 44955* | A change of bound variable, often used in proofs for etransc 44999. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) = (π β (0...π) β¦ (π¦ β π β¦ ((π¦ β π)βif(π = 0, (π β 1), π)))) | ||
Theorem | etransclem6 44956* | A change of bound variable, often used in proofs for etransc 44999. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) = (π¦ β β β¦ ((π¦β(π β 1)) Β· βπ β (1...π)((π¦ β π)βπ))) | ||
Theorem | etransclem7 44957* | The given product is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β πΆ:(0...π)βΆ(0...π)) & β’ (π β π½ β (0...π)) β β’ (π β βπ β (1...π)if(π < (πΆβπ), 0, (((!βπ) / (!β(π β (πΆβπ)))) Β· ((π½ β π)β(π β (πΆβπ))))) β β€) | ||
Theorem | etransclem8 44958* | πΉ is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) β β’ (π β πΉ:πβΆβ) | ||
Theorem | etransclem9 44959 | If πΎ divides π but πΎ does not divide π then π + π cannot be zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β πΎ β β€) & β’ (π β πΎ β 0) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β Β¬ πΎ β₯ π) & β’ (π β πΎ β₯ π) β β’ (π β (π + π) β 0) | ||
Theorem | etransclem10 44960 | The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ (π β πΆ:(0...π)βΆ(0...π)) & β’ (π β π½ β β€) β β’ (π β if((π β 1) < (πΆβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πΆβ0)))) Β· (π½β((π β 1) β (πΆβ0))))) β β€) | ||
Theorem | etransclem11 44961* | A change of bound variable, often used in proofs for etransc 44999. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) | ||
Theorem | etransclem12 44962* | πΆ applied to π. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) & β’ (π β π β β0) β β’ (π β (πΆβπ) = {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) | ||
Theorem | etransclem13 44963* | πΉ applied to π. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β π) β β’ (π β (πΉβπ) = βπ β (0...π)((π β π)βif(π = 0, (π β 1), π))) | ||
Theorem | etransclem14 44964* | Value of the term π, when π½ = 0 and (πΆβ0) = π β 1 (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ (π β πΆ:(0...π)βΆ(0...π)) & β’ π = (((!βπ) / βπ β (0...π)(!β(πΆβπ))) Β· (if((π β 1) < (πΆβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πΆβ0)))) Β· (π½β((π β 1) β (πΆβ0))))) Β· βπ β (1...π)if(π < (πΆβπ), 0, (((!βπ) / (!β(π β (πΆβπ)))) Β· ((π½ β π)β(π β (πΆβπ))))))) & β’ (π β π½ = 0) & β’ (π β (πΆβ0) = (π β 1)) β β’ (π β π = (((!βπ) / βπ β (0...π)(!β(πΆβπ))) Β· ((!β(π β 1)) Β· βπ β (1...π)if(π < (πΆβπ), 0, (((!βπ) / (!β(π β (πΆβπ)))) Β· (-πβ(π β (πΆβπ)))))))) | ||
Theorem | etransclem15 44965* | Value of the term π, when π½ = 0 and (πΆβ0) = π β 1 (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β πΆ:(0...π)βΆ(0...π)) & β’ π = (((!βπ) / βπ β (0...π)(!β(πΆβπ))) Β· (if((π β 1) < (πΆβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πΆβ0)))) Β· (π½β((π β 1) β (πΆβ0))))) Β· βπ β (1...π)if(π < (πΆβπ), 0, (((!βπ) / (!β(π β (πΆβπ)))) Β· ((π½ β π)β(π β (πΆβπ))))))) & β’ (π β π½ = 0) & β’ (π β (πΆβ0) β (π β 1)) β β’ (π β π = 0) | ||
Theorem | etransclem16 44966* | Every element in the range of πΆ is a finite set. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) & β’ (π β π β β0) β β’ (π β (πΆβπ) β Fin) | ||
Theorem | etransclem17 44967* | The π-th derivative of π». (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ (π β π½ β (0...π)) & β’ (π β π β β0) β β’ (π β ((π Dπ (π»βπ½))βπ) = (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)))))) | ||
Theorem | etransclem18 44968* | The given function is integrable. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β β β {β, β}) & β’ (π β β β ((TopOpenββfld) βΎt β)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π₯ β (π΄(,)π΅) β¦ ((eβπ-π₯) Β· (πΉβπ₯))) β πΏ1) | ||
Theorem | etransclem19 44969* | The π-th derivative of π» is 0 if π is large enough. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ (π β π½ β (0...π)) & β’ (π β π β β€) & β’ (π β if(π½ = 0, (π β 1), π) < π) β β’ (π β ((π Dπ (π»βπ½))βπ) = (π₯ β π β¦ 0)) | ||
Theorem | etransclem20 44970* | π» is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ (π β π½ β (0...π)) & β’ (π β π β β0) β β’ (π β ((π Dπ (π»βπ½))βπ):πβΆβ) | ||
Theorem | etransclem21 44971* | The π-th derivative of π» applied to π. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ (π β π½ β (0...π)) & β’ (π β π β β0) & β’ (π β π β π) β β’ (π β (((π Dπ (π»βπ½))βπ)βπ) = if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π β π½)β(if(π½ = 0, (π β 1), π) β π))))) | ||
Theorem | etransclem22 44972* | The π-th derivative of π» is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ (π β π½ β (0...π)) & β’ (π β π β β0) β β’ (π β ((π Dπ (π»βπ½))βπ) β (πβcnββ)) | ||
Theorem | etransclem23 44973* | This is the claim proof in [Juillerat] p. 14 (but in our proof, Stirling's approximation is not used). (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄:β0βΆβ€) & β’ πΏ = Ξ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) & β’ πΎ = (πΏ / (!β(π β 1))) & β’ (π β π β β) & β’ (π β π β β) & β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· (((πβ(π + 1))β(π β 1)) / (!β(π β 1)))) < 1) β β’ (π β (absβπΎ) < 1) | ||
Theorem | etransclem24 44974* | π divides the I -th derivative of πΉ applied to π½. when π½ = 0 and πΌ is not equal to π β 1. This is the second part of case 2 proven in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ (π β πΌ β β0) & β’ (π β πΌ β (π β 1)) & β’ (π β π½ = 0) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) & β’ (π β π· β (πΆβπΌ)) β β’ (π β π β₯ ((((!βπΌ) / βπ β (0...π)(!β(π·βπ))) Β· (if((π β 1) < (π·β0), 0, (((!β(π β 1)) / (!β((π β 1) β (π·β0)))) Β· (π½β((π β 1) β (π·β0))))) Β· βπ β (1...π)if(π < (π·βπ), 0, (((!βπ) / (!β(π β (π·βπ)))) Β· ((π½ β π)β(π β (π·βπ))))))) / (!β(π β 1)))) | ||
Theorem | etransclem25 44975* | π factorial divides the π-th derivative of πΉ applied to π½. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β πΆ:(0...π)βΆ(0...π)) & β’ (π β Ξ£π β (0...π)(πΆβπ) = π) & β’ π = (((!βπ) / βπ β (0...π)(!β(πΆβπ))) Β· (if((π β 1) < (πΆβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πΆβ0)))) Β· (π½β((π β 1) β (πΆβ0))))) Β· βπ β (1...π)if(π < (πΆβπ), 0, (((!βπ) / (!β(π β (πΆβπ)))) Β· ((π½ β π)β(π β (πΆβπ))))))) & β’ (π β π½ β (1...π)) β β’ (π β (!βπ) β₯ π) | ||
Theorem | etransclem26 44976* | Every term in the sum of the π-th derivative of πΉ applied to π½ is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π½ β β€) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) & β’ (π β π· β (πΆβπ)) β β’ (π β (((!βπ) / βπ β (0...π)(!β(π·βπ))) Β· (if((π β 1) < (π·β0), 0, (((!β(π β 1)) / (!β((π β 1) β (π·β0)))) Β· (π½β((π β 1) β (π·β0))))) Β· βπ β (1...π)if(π < (π·βπ), 0, (((!βπ) / (!β(π β (π·βπ)))) Β· ((π½ β π)β(π β (π·βπ))))))) β β€) | ||
Theorem | etransclem27 44977* | The π-th derivative of πΉ applied to π½ is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ (π β πΆ β Fin) & β’ (π β πΆ:dom πΆβΆ(β0 βm (0...π))) & β’ πΊ = (π₯ β π β¦ Ξ£π β dom πΆβπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ₯)) & β’ (π β π½ β π) & β’ (π β π½ β β€) β β’ (π β (πΊβπ½) β β€) | ||
Theorem | etransclem28 44978* | (π β 1) factorial divides the π-th derivative of πΉ applied to π½. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ (π β π β β0) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) & β’ (π β π· β (πΆβπ)) & β’ (π β π½ β (0...π)) & β’ π = (((!βπ) / βπ β (0...π)(!β(π·βπ))) Β· (if((π β 1) < (π·β0), 0, (((!β(π β 1)) / (!β((π β 1) β (π·β0)))) Β· (π½β((π β 1) β (π·β0))))) Β· βπ β (1...π)if(π < (π·βπ), 0, (((!βπ) / (!β(π β (π·βπ)))) Β· ((π½ β π)β(π β (π·βπ))))))) β β’ (π β (!β(π β 1)) β₯ π) | ||
Theorem | etransclem29 44979* | The π-th derivative of πΉ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β β0) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) & β’ πΈ = (π₯ β π β¦ βπ β (0...π)((π»βπ)βπ₯)) β β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ β (0...π)(!β(πβπ))) Β· βπ β (0...π)(((π Dπ (π»βπ))β(πβπ))βπ₯)))) | ||
Theorem | etransclem30 44980* | The π-th derivative of πΉ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β β0) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) β β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ β (0...π)(!β(πβπ))) Β· βπ β (0...π)(((π Dπ (π»βπ))β(πβπ))βπ₯)))) | ||
Theorem | etransclem31 44981* | The π-th derivative of π» applied to π. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β β0) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) & β’ (π β π β π) β β’ (π β (((π Dπ πΉ)βπ)βπ) = Ξ£π β (πΆβπ)(((!βπ) / βπ β (0...π)(!β(πβπ))) Β· (if((π β 1) < (πβ0), 0, (((!β(π β 1)) / (!β((π β 1) β (πβ0)))) Β· (πβ((π β 1) β (πβ0))))) Β· βπ β (1...π)if(π < (πβπ), 0, (((!βπ) / (!β(π β (πβπ)))) Β· ((π β π)β(π β (πβπ)))))))) | ||
Theorem | etransclem32 44982* | This is the proof for the last equation in the proof of the derivative calculated in [Juillerat] p. 12, just after equation *(6) . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β β0) & β’ (π β ((π Β· π) + (π β 1)) < π) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) β β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ 0)) | ||
Theorem | etransclem33 44983* | πΉ is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β β0) β β’ (π β ((π Dπ πΉ)βπ):πβΆβ) | ||
Theorem | etransclem34 44984* | The π-th derivative of πΉ is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β β0) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) β β’ (π β ((π Dπ πΉ)βπ) β (πβcnββ)) | ||
Theorem | etransclem35 44985* | π does not divide the P-1 -th derivative of πΉ applied to 0. This is case 2 of the proof in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) & β’ π· = (π β (0...π) β¦ if(π = 0, (π β 1), 0)) β β’ (π β (((β Dπ πΉ)β(π β 1))β0) = ((!β(π β 1)) Β· (βπ β (1...π)-πβπ))) | ||
Theorem | etransclem36 44986* | The π-th derivative of πΉ applied to π½ is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β β0) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ (π β π½ β π) & β’ (π β π½ β β€) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) β β’ (π β (((π Dπ πΉ)βπ)βπ½) β β€) | ||
Theorem | etransclem37 44987* | (π β 1) factorial divides the π-th derivative of πΉ applied to π½. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β β0) & β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) & β’ (π β π½ β (0...π)) & β’ (π β π½ β π) β β’ (π β (!β(π β 1)) β₯ (((π Dπ πΉ)βπ)βπ½)) | ||
Theorem | etransclem38 44988* | π divides the I -th derivative of πΉ applied to π½. if it is not the case that πΌ = π β 1 and π½ = 0. This is case 1 and the second part of case 2 proven in in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β πΌ β β0) & β’ (π β π½ β (0...π)) & β’ (π β Β¬ (πΌ = (π β 1) β§ π½ = 0)) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) β β’ (π β π β₯ ((((β Dπ πΉ)βπΌ)βπ½) / (!β(π β 1)))) | ||
Theorem | etransclem39 44989* | πΊ is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ πΊ = (π₯ β β β¦ Ξ£π β (0...π )(((β Dπ πΉ)βπ)βπ₯)) β β’ (π β πΊ:ββΆβ) | ||
Theorem | etransclem40 44990* | The π-th derivative of πΉ is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β β0) β β’ (π β ((π Dπ πΉ)βπ) β (πβcnββ)) | ||
Theorem | etransclem41 44991* | π does not divide the P-1 -th derivative of πΉ applied to 0. This is the first part of case 2: proven in in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β0) & β’ (π β π β β) & β’ (π β (!βπ) < π) & β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) β β’ (π β Β¬ π β₯ ((((β Dπ πΉ)β(π β 1))β0) / (!β(π β 1)))) | ||
Theorem | etransclem42 44992* | The π-th derivative of πΉ applied to π½ is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π β β0) & β’ (π β π½ β π) & β’ (π β π½ β β€) β β’ (π β (((π Dπ πΉ)βπ)βπ½) β β€) | ||
Theorem | etransclem43 44993* | πΊ is a continuous function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ πΊ = (π₯ β π β¦ Ξ£π β (0...π )(((π Dπ πΉ)βπ)βπ₯)) β β’ (π β πΊ β (πβcnββ)) | ||
Theorem | etransclem44 44994* | The given finite sum is nonzero. This is the claim proved after equation (7) in [Juillerat] p. 12 . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄:β0βΆβ€) & β’ (π β (π΄β0) β 0) & β’ (π β π β β0) & β’ (π β π β β) & β’ (π β (absβ(π΄β0)) < π) & β’ (π β (!βπ) < π) & β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ πΎ = (Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β Dπ πΉ)β(2nd βπ))β(1st βπ))) / (!β(π β 1))) β β’ (π β πΎ β 0) | ||
Theorem | etransclem45 44995* | πΎ is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ (π β π΄:β0βΆβ€) & β’ πΎ = (Ξ£π β ((0...π) Γ (0...π ))((π΄β(1st βπ)) Β· (((β Dπ πΉ)β(2nd βπ))β(1st βπ))) / (!β(π β 1))) β β’ (π β πΎ β β€) | ||
Theorem | etransclem46 44996* | This is the proof for equation *(7) in [Juillerat] p. 12. The proven equality will lead to a contradiction, because the left-hand side goes to 0 for large π, but the right-hand side is a nonzero integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β ((Polyββ€) β {0π})) & β’ (π β (πβe) = 0) & β’ π΄ = (coeffβπ) & β’ π = (degβπ) & β’ (π β β β β) & β’ (π β β β {β, β}) & β’ (π β β β ((TopOpenββfld) βΎt β)) & β’ (π β π β β) & β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ πΏ = Ξ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) & β’ π = ((π Β· π) + (π β 1)) & β’ πΊ = (π₯ β β β¦ Ξ£π β (0...π )(((β Dπ πΉ)βπ)βπ₯)) & β’ π = (π₯ β (0[,]π) β¦ -((eβπ-π₯) Β· (πΊβπ₯))) β β’ (π β (πΏ / (!β(π β 1))) = (-Ξ£π β ((0...π) Γ (0...π ))((π΄β(1st βπ)) Β· (((β Dπ πΉ)β(2nd βπ))β(1st βπ))) / (!β(π β 1)))) | ||
Theorem | etransclem47 44997* | e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β ((Polyββ€) β {0π})) & β’ (π β (πβe) = 0) & β’ π΄ = (coeffβπ) & β’ (π β (π΄β0) β 0) & β’ π = (degβπ) & β’ (π β π β β) & β’ (π β (absβ(π΄β0)) < π) & β’ (π β (!βπ) < π) & β’ (π β (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· (((πβ(π + 1))β(π β 1)) / (!β(π β 1)))) < 1) & β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) & β’ πΏ = Ξ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) & β’ πΎ = (πΏ / (!β(π β 1))) β β’ (π β βπ β β€ (π β 0 β§ (absβπ) < 1)) | ||
Theorem | etransclem48 44998* | e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. In this lemma, a large enough prime π is chosen: it will be used by subsequent lemmas. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 28-Sep-2020.) |
β’ (π β π β ((Polyββ€) β {0π})) & β’ (π β (πβe) = 0) & β’ π΄ = (coeffβπ) & β’ (π β (π΄β0) β 0) & β’ π = (degβπ) & β’ πΆ = Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) & β’ π = (π β β0 β¦ (πΆ Β· (((πβ(π + 1))βπ) / (!βπ)))) & β’ πΌ = inf({π β β0 β£ βπ β (β€β₯βπ)(absβ(πβπ)) < 1}, β, < ) & β’ π = sup({(absβ(π΄β0)), (!βπ), πΌ}, β*, < ) β β’ (π β βπ β β€ (π β 0 β§ (absβπ) < 1)) | ||
Theorem | etransc 44999 | e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Proof shortened by AV, 28-Sep-2020.) |
β’ e β (β β πΈ) | ||
Theorem | rrxtopn 45000* | The topology of the generalized real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β πΌ β π) β β’ (π β (TopOpenβ(β^βπΌ)) = (MetOpenβ(π β (Baseβ(β^βπΌ)), π β (Baseβ(β^βπΌ)) β¦ (ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |