Home | Metamath
Proof Explorer Theorem List (p. 440 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvnmptdivc 43901* | Function-builder for iterated derivative, division rule for constant divisor. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β π) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π β§ π β (0...π)) β π΅ β β) & β’ ((π β§ π β (0...π)) β ((π Dπ (π₯ β π β¦ π΄))βπ) = (π₯ β π β¦ π΅)) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) & β’ (π β π β β0) β β’ ((π β§ π β (0...π)) β ((π Dπ (π₯ β π β¦ (π΄ / πΆ)))βπ) = (π₯ β π β¦ (π΅ / πΆ))) | ||
Theorem | dvdsn1add 43902 | If πΎ divides π but πΎ does not divide π, then πΎ does not divide (π + π). (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((Β¬ πΎ β₯ π β§ πΎ β₯ π) β Β¬ πΎ β₯ (π + π))) | ||
Theorem | dvxpaek 43903* | Derivative of the polynomial (π₯ + π΄)βπΎ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β πΎ β β) β β’ (π β (π D (π₯ β π β¦ ((π₯ + π΄)βπΎ))) = (π₯ β π β¦ (πΎ Β· ((π₯ + π΄)β(πΎ β 1))))) | ||
Theorem | dvnmptconst 43904* | The π-th derivative of a constant function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β π β β) β β’ (π β ((π Dπ (π₯ β π β¦ π΄))βπ) = (π₯ β π β¦ 0)) | ||
Theorem | dvnxpaek 43905* | The π-th derivative of the polynomial (π₯ + π΄)βπΎ. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π΄ β β) & β’ (π β πΎ β β0) & β’ πΉ = (π₯ β π β¦ ((π₯ + π΄)βπΎ)) β β’ ((π β§ π β β0) β ((π Dπ πΉ)βπ) = (π₯ β π β¦ if(πΎ < π, 0, (((!βπΎ) / (!β(πΎ β π))) Β· ((π₯ + π΄)β(πΎ β π)))))) | ||
Theorem | dvnmul 43906* | Function-builder for the π-th derivative, product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β β) & β’ (π β π β β0) & β’ πΉ = (π₯ β π β¦ π΄) & β’ πΊ = (π₯ β π β¦ π΅) & β’ ((π β§ π β (0...π)) β ((π Dπ πΉ)βπ):πβΆβ) & β’ ((π β§ π β (0...π)) β ((π Dπ πΊ)βπ):πβΆβ) & β’ πΆ = (π β (0...π) β¦ ((π Dπ πΉ)βπ)) & β’ π· = (π β (0...π) β¦ ((π Dπ πΊ)βπ)) β β’ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) | ||
Theorem | dvmptfprodlem 43907* | Induction step for dvmptfprod 43908. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ β²ππ & β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ (π β π· β Fin) & β’ (π β πΈ β V) & β’ (π β Β¬ πΈ β π·) & β’ (π β (π· βͺ {πΈ}) β πΌ) & β’ (π β π β {β, β}) & β’ (((π β§ π₯ β π) β§ π β π·) β πΆ β β) & β’ (π β (π D (π₯ β π β¦ βπ β π· π΄)) = (π₯ β π β¦ Ξ£π β π· (πΆ Β· βπ β (π· β {π})π΄))) & β’ ((π β§ π₯ β π) β πΊ β β) & β’ (π β (π D (π₯ β π β¦ πΉ)) = (π₯ β π β¦ πΊ)) & β’ (π = πΈ β π΄ = πΉ) & β’ (π = πΈ β πΆ = πΊ) β β’ (π β (π D (π₯ β π β¦ βπ β (π· βͺ {πΈ})π΄)) = (π₯ β π β¦ Ξ£π β (π· βͺ {πΈ})(πΆ Β· βπ β ((π· βͺ {πΈ}) β {π})π΄))) | ||
Theorem | dvmptfprod 43908* | Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β π β {β, β}) & β’ (π β π β π½) & β’ (π β πΌ β Fin) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΅ β β) & β’ ((π β§ π β πΌ) β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π = π β π΅ = πΆ) β β’ (π β (π D (π₯ β π β¦ βπ β πΌ π΄)) = (π₯ β π β¦ Ξ£π β πΌ (πΆ Β· βπ β (πΌ β {π})π΄))) | ||
Theorem | dvnprodlem1 43909* | π· is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ πΆ = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ (π β π½ β β0) & β’ π· = (π β ((πΆβ(π βͺ {π}))βπ½) β¦ β¨(π½ β (πβπ)), (π βΎ π )β©) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β Β¬ π β π ) & β’ (π β (π βͺ {π}) β π) β β’ (π β π·:((πΆβ(π βͺ {π}))βπ½)β1-1-ontoββͺ π β (0...π½)({π} Γ ((πΆβπ )βπ))) | ||
Theorem | dvnprodlem2 43910* | Induction step for dvnprodlem2 43910. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β Fin) & β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) & β’ (π β π β β0) & β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) & β’ πΆ = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ (π β π β π) & β’ (π β π β (π β π )) & β’ (π β βπ β (0...π)((π Dπ (π₯ β π β¦ βπ‘ β π ((π»βπ‘)βπ₯)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ )βπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) & β’ (π β π½ β (0...π)) & β’ π· = (π β ((πΆβ(π βͺ {π}))βπ½) β¦ β¨(π½ β (πβπ)), (π βΎ π )β©) β β’ (π β ((π Dπ (π₯ β π β¦ βπ‘ β (π βͺ {π})((π»βπ‘)βπ₯)))βπ½) = (π₯ β π β¦ Ξ£π β ((πΆβ(π βͺ {π}))βπ½)(((!βπ½) / βπ‘ β (π βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) | ||
Theorem | dvnprodlem3 43911* | The multinomial formula for the π-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β Fin) & β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) & β’ (π β π β β0) & β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) & β’ πΉ = (π₯ β π β¦ βπ‘ β π ((π»βπ‘)βπ₯)) & β’ π· = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) β β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) | ||
Theorem | dvnprod 43912* | The multinomial formula for the π-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β {β, β}) & β’ (π β π β ((TopOpenββfld) βΎt π)) & β’ (π β π β Fin) & β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) & β’ (π β π β β0) & β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) & β’ πΉ = (π₯ β π β¦ βπ‘ β π ((π»βπ‘)βπ₯)) & β’ πΆ = (π β β0 β¦ {π β ((0...π) βm π) β£ Ξ£π‘ β π (πβπ‘) = π}) β β’ (π β ((π Dπ πΉ)βπ) = (π₯ β π β¦ Ξ£π β (πΆβπ)(((!βπ) / βπ‘ β π (!β(πβπ‘))) Β· βπ‘ β π (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) | ||
Theorem | itgsin0pilem1 43913* | Calculation of the integral for sine on the (0,Ο) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΆ = (π‘ β (0[,]Ο) β¦ -(cosβπ‘)) β β’ β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 | ||
Theorem | ibliccsinexp 43914* | sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄[,]π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsin0pi 43915 | Calculation of the integral for sine on the (0,Ο) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β«(0(,)Ο)(sinβπ₯) dπ₯ = 2 | ||
Theorem | iblioosinexp 43916* | sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β (π₯ β (π΄(,)π΅) β¦ ((sinβπ₯)βπ)) β πΏ1) | ||
Theorem | itgsinexplem1 43917* | Integration by parts is applied to integrate sin^(N+1). (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΉ = (π₯ β β β¦ ((sinβπ₯)βπ)) & β’ πΊ = (π₯ β β β¦ -(cosβπ₯)) & β’ π» = (π₯ β β β¦ ((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯))) & β’ πΌ = (π₯ β β β¦ (((sinβπ₯)βπ) Β· (sinβπ₯))) & β’ πΏ = (π₯ β β β¦ (((π Β· ((sinβπ₯)β(π β 1))) Β· (cosβπ₯)) Β· -(cosβπ₯))) & β’ π = (π₯ β β β¦ (((cosβπ₯)β2) Β· ((sinβπ₯)β(π β 1)))) & β’ (π β π β β) β β’ (π β β«(0(,)Ο)(((sinβπ₯)βπ) Β· (sinβπ₯)) dπ₯ = (π Β· β«(0(,)Ο)(((cosβπ₯)β2) Β· ((sinβπ₯)β(π β 1))) dπ₯)) | ||
Theorem | itgsinexp 43918* | A recursive formula for the integral of sin^N on the interval (0,Ο) . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) & β’ (π β π β (β€β₯β2)) β β’ (π β (πΌβπ) = (((π β 1) / π) Β· (πΌβ(π β 2)))) | ||
Theorem | iblconstmpt 43919* | A constant function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β dom vol β§ (volβπ΄) β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β πΏ1) | ||
Theorem | itgeq1d 43920* | Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ = π΅) β β’ (π β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) | ||
Theorem | mbfres2cn 43921 | Measurability of a piecewise function: if πΉ is measurable on subsets π΅ and πΆ of its domain, and these pieces make up all of π΄, then πΉ is measurable on the whole domain. Similar to mbfres2 24931 but here the theorem is extended to complex-valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β (πΉ βΎ π΅) β MblFn) & β’ (π β (πΉ βΎ πΆ) β MblFn) & β’ (π β (π΅ βͺ πΆ) = π΄) β β’ (π β πΉ β MblFn) | ||
Theorem | vol0 43922 | The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (volββ ) = 0 | ||
Theorem | ditgeqiooicc 43923* | A function πΉ on an open interval, has the same directed integral as its extension πΊ on the closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ:(π΄(,)π΅)βΆβ) β β’ (π β β¨[π΄ β π΅](πΉβπ₯) dπ₯ = β¨[π΄ β π΅](πΊβπ₯) dπ₯) | ||
Theorem | volge0 43924 | The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β dom vol β 0 β€ (volβπ΄)) | ||
Theorem | cnbdibl 43925* | A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β dom vol) & β’ (π β (volβπ΄) β β) & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β βπ₯ β β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) β β’ (π β πΉ β πΏ1) | ||
Theorem | snmbl 43926 | A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β {π΄} β dom vol) | ||
Theorem | ditgeq3d 43927* | Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β€ π΅) & β’ ((π β§ π₯ β (π΄(,)π΅)) β π· = πΈ) β β’ (π β β¨[π΄ β π΅]π· dπ₯ = β¨[π΄ β π΅]πΈ dπ₯) | ||
Theorem | iblempty 43928 | The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β β πΏ1 | ||
Theorem | iblsplit 43929* | The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π β¦ πΆ) β πΏ1) | ||
Theorem | volsn 43930 | A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β (volβ{π΄}) = 0) | ||
Theorem | itgvol0 43931* | If the domani is negligible, the function is integrable and the integral is 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β§ β«π΄π΅ dπ₯ = 0)) | ||
Theorem | itgcoscmulx 43932* | Exercise: the integral of π₯ β¦ cosππ₯ on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ πΆ) & β’ (π β π΄ β 0) β β’ (π β β«(π΅(,)πΆ)(cosβ(π΄ Β· π₯)) dπ₯ = (((sinβ(π΄ Β· πΆ)) β (sinβ(π΄ Β· π΅))) / π΄)) | ||
Theorem | iblsplitf 43933* | A version of iblsplit 43929 using bound-variable hypotheses instead of distinct variable conditions". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π β¦ πΆ) β πΏ1) | ||
Theorem | ibliooicc 43934* | If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π₯ β (π΄(,)π΅) β¦ πΆ) β πΏ1) & β’ ((π β§ π₯ β (π΄[,]π΅)) β πΆ β β) β β’ (π β (π₯ β (π΄[,]π΅) β¦ πΆ) β πΏ1) | ||
Theorem | volioc 43935 | The measure of a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄(,]π΅)) = (π΅ β π΄)) | ||
Theorem | iblspltprt 43936* | If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π‘π & β’ (π β π β β€) & β’ (π β π β (β€β₯β(π + 1))) & β’ ((π β§ π β (π...π)) β (πβπ) β β) & β’ ((π β§ π β (π..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π‘ β ((πβπ)[,](πβπ))) β π΄ β β) & β’ ((π β§ π β (π..^π)) β (π‘ β ((πβπ)[,](πβ(π + 1))) β¦ π΄) β πΏ1) β β’ (π β (π‘ β ((πβπ)[,](πβπ)) β¦ π΄) β πΏ1) | ||
Theorem | itgsincmulx 43937* | Exercise: the integral of π₯ β¦ sinππ₯ on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ πΆ) β β’ (π β β«(π΅(,)πΆ)(sinβ(π΄ Β· π₯)) dπ₯ = (((cosβ(π΄ Β· π΅)) β (cosβ(π΄ Β· πΆ))) / π΄)) | ||
Theorem | itgsubsticclem 43938* | lemma for itgsubsticc 43939. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π’ β (πΎ[,]πΏ) β¦ πΆ) & β’ πΊ = (π’ β β β¦ if(π’ β (πΎ[,]πΏ), (πΉβπ’), if(π’ < πΎ, (πΉβπΎ), (πΉβπΏ)))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(πΎ[,]πΏ))) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β πΉ β ((πΎ[,]πΏ)βcnββ)) & β’ (π β πΎ β β) & β’ (π β πΏ β β) & β’ (π β πΎ β€ πΏ) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgsubsticc 43939* | Integration by u-substitution. The main difference with respect to itgsubst 25335 is that here we consider the range of π΄(π₯) to be in the closed interval (πΎ[,]πΏ). If π΄(π₯) is a continuous, differentiable function from [π, π] to (π, π), whose derivative is continuous and integrable, and πΆ(π’) is a continuous function on (π, π), then the integral of πΆ(π’) from πΎ = π΄(π) to πΏ = π΄(π) is equal to the integral of πΆ(π΄(π₯)) D π΄(π₯) from π to π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) & β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnβ(πΎ[,]πΏ))) & β’ (π β (π’ β (πΎ[,]πΏ) β¦ πΆ) β ((πΎ[,]πΏ)βcnββ)) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β (((π(,)π)βcnββ) β© πΏ1)) & β’ (π β (β D (π₯ β (π[,]π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) & β’ (π’ = π΄ β πΆ = πΈ) & β’ (π₯ = π β π΄ = πΎ) & β’ (π₯ = π β π΄ = πΏ) & β’ (π β πΎ β β) & β’ (π β πΏ β β) β β’ (π β β¨[πΎ β πΏ]πΆ dπ’ = β¨[π β π](πΈ Β· π΅) dπ₯) | ||
Theorem | itgioocnicc 43940* | The integral of a piecewise continuous function πΉ on an open interval is equal to the integral of the continuous function πΊ, in the corresponding closed interval. πΊ is equal to πΉ on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:dom πΉβΆβ) & β’ (π β (πΉ βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) & β’ (π β (π΄[,]π΅) β dom πΉ) & β’ (π β π β ((πΉ βΎ (π΄(,)π΅)) limβ π΄)) & β’ (π β πΏ β ((πΉ βΎ (π΄(,)π΅)) limβ π΅)) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) β β’ (π β (πΊ β πΏ1 β§ β«(π΄[,]π΅)(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯)) | ||
Theorem | iblcncfioo 43941 | A continuous function πΉ on an open interval (π΄(,)π΅) with a finite right limit π in π΄ and a finite left limit πΏ in π΅ is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β πΉ β πΏ1) | ||
Theorem | itgspltprt 43942* | The β« integral splits on a given partition π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β€) & β’ (π β π β (β€β₯β(π + 1))) & β’ (π β π:(π...π)βΆβ) & β’ ((π β§ π β (π..^π)) β (πβπ) < (πβ(π + 1))) & β’ ((π β§ π‘ β ((πβπ)[,](πβπ))) β π΄ β β) & β’ ((π β§ π β (π..^π)) β (π‘ β ((πβπ)[,](πβ(π + 1))) β¦ π΄) β πΏ1) β β’ (π β β«((πβπ)[,](πβπ))π΄ dπ‘ = Ξ£π β (π..^π)β«((πβπ)[,](πβ(π + 1)))π΄ dπ‘) | ||
Theorem | itgiccshift 43943* | The integral of a function, πΉ stays the same if its closed interval domain is shifted by π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) & β’ (π β π β β+) & β’ πΊ = (π₯ β ((π΄ + π)[,](π΅ + π)) β¦ (πΉβ(π₯ β π))) β β’ (π β β«((π΄ + π)[,](π΅ + π))(πΊβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | itgperiod 43944* | The integral of a periodic function, with period π stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β β+) & β’ (π β πΉ:ββΆβ) & β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ (π β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) β β’ (π β β«((π΄ + π)[,](π΅ + π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) | ||
Theorem | itgsbtaddcnst 43945* | Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β β) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β β¨[(π΄ β π) β (π΅ β π)](πΉβ(π + π )) dπ = β¨[π΄ β π΅](πΉβπ‘) dπ‘) | ||
Theorem | volico 43946 | The measure of left-closed, right-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄[,)π΅)) = if(π΄ < π΅, (π΅ β π΄), 0)) | ||
Theorem | sublevolico 43947 | The Lebesgue measure of a left-closed, right-open interval is greater than or equal to the difference of the two bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΅ β π΄) β€ (volβ(π΄[,)π΅))) | ||
Theorem | dmvolss 43948 | Lebesgue measurable sets are subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ dom vol β π« β | ||
Theorem | ismbl3 43949* | The predicate "π΄ is Lebesgue-measurable". Similar to ismbl2 24813, but here +π is used, and the precondition (vol*βπ₯) β β can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β dom vol β (π΄ β β β§ βπ₯ β π« β((vol*β(π₯ β© π΄)) +π (vol*β(π₯ β π΄))) β€ (vol*βπ₯))) | ||
Theorem | volioof 43950 | The function that assigns the Lebesgue measure to open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (vol β (,)):(β* Γ β*)βΆ(0[,]+β) | ||
Theorem | ovolsplit 43951 | The Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts, using addition for extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) β β’ (π β (vol*βπ΄) β€ ((vol*β(π΄ β© π΅)) +π (vol*β(π΄ β π΅)))) | ||
Theorem | fvvolioof 43952 | The function value of the Lebesgue measure of an open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β* Γ β*)) & β’ (π β π β π΄) β β’ (π β (((vol β (,)) β πΉ)βπ) = (volβ((1st β(πΉβπ))(,)(2nd β(πΉβπ))))) | ||
Theorem | volioore 43953 | The measure of an open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄(,)π΅)) = if(π΄ β€ π΅, (π΅ β π΄), 0)) | ||
Theorem | fvvolicof 43954 | The function value of the Lebesgue measure of a left-closed right-open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β* Γ β*)) & β’ (π β π β π΄) β β’ (π β (((vol β [,)) β πΉ)βπ) = (volβ((1st β(πΉβπ))[,)(2nd β(πΉβπ))))) | ||
Theorem | voliooico 43955 | An open interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (volβ(π΄(,)π΅)) = (volβ(π΄[,)π΅))) | ||
Theorem | ismbl4 43956* | The predicate "π΄ is Lebesgue-measurable". Similar to ismbl 24812, but here +π is used, and the precondition (vol*βπ₯) β β can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β dom vol β (π΄ β β β§ βπ₯ β π« β(vol*βπ₯) = ((vol*β(π₯ β© π΄)) +π (vol*β(π₯ β π΄))))) | ||
Theorem | volioofmpt 43957* | ((vol β (,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆ(β* Γ β*)) β β’ (π β ((vol β (,)) β πΉ) = (π₯ β π΄ β¦ (volβ((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯)))))) | ||
Theorem | volicoff 43958 | ((vol β [,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β Γ β*)) β β’ (π β ((vol β [,)) β πΉ):π΄βΆ(0[,]+β)) | ||
Theorem | voliooicof 43959 | The Lebesgue measure of open intervals is the same as the Lebesgue measure of left-closed right-open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β Γ β)) β β’ (π β ((vol β (,)) β πΉ) = ((vol β [,)) β πΉ)) | ||
Theorem | volicofmpt 43960* | ((vol β [,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆ(β Γ β*)) β β’ (π β ((vol β [,)) β πΉ) = (π₯ β π΄ β¦ (volβ((1st β(πΉβπ₯))[,)(2nd β(πΉβπ₯)))))) | ||
Theorem | volicc 43961 | The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄[,]π΅)) = (π΅ β π΄)) | ||
Theorem | voliccico 43962 | A closed interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (volβ(π΄[,]π΅)) = (volβ(π΄[,)π΅))) | ||
Theorem | mbfdmssre 43963 | The domain of a measurable function is a subset of the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (πΉ β MblFn β dom πΉ β β) | ||
Theorem | stoweidlem1 43964 | Lemma for stoweid 44026. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 14058. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π· β β+) & β’ (π β π΄ β β+) & β’ (π β 0 β€ π΄) & β’ (π β π΄ β€ 1) & β’ (π β π· β€ π΄) β β’ (π β ((1 β (π΄βπ))β(πΎβπ)) β€ (1 / ((πΎ Β· π·)βπ))) | ||
Theorem | stoweidlem2 43965* | lemma for stoweid 44026: here we prove that the subalgebra of continuous functions, which contains constant functions, is closed under scaling. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ (π β πΈ β β) & β’ (π β πΉ β π΄) β β’ (π β (π‘ β π β¦ (πΈ Β· (πΉβπ‘))) β π΄) | ||
Theorem | stoweidlem3 43966* | Lemma for stoweid 44026: if π΄ is positive and all π terms of a finite product are larger than π΄, then the finite product is larger than π΄βπ. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππΉ & β’ β²ππ & β’ π = seq1( Β· , πΉ) & β’ (π β π β β) & β’ (π β πΉ:(1...π)βΆβ) & β’ ((π β§ π β (1...π)) β π΄ < (πΉβπ)) & β’ (π β π΄ β β+) β β’ (π β (π΄βπ) < (πβπ)) | ||
Theorem | stoweidlem4 43967* | Lemma for stoweid 44026: a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) β β’ ((π β§ π΅ β β) β (π‘ β π β¦ π΅) β π΄) | ||
Theorem | stoweidlem5 43968* | There exists a Ξ΄ as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: 0 < Ξ΄ < 1 , p >= Ξ΄ on π β π. Here π· is used to represent Ξ΄ in the paper and π to represent π β π in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ π· = if(πΆ β€ (1 / 2), πΆ, (1 / 2)) & β’ (π β π:πβΆβ) & β’ (π β π β π) & β’ (π β πΆ β β+) & β’ (π β βπ‘ β π πΆ β€ (πβπ‘)) β β’ (π β βπ(π β β+ β§ π < 1 β§ βπ‘ β π π β€ (πβπ‘))) | ||
Theorem | stoweidlem6 43969* | Lemma for stoweid 44026: two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘ π = πΉ & β’ β²π‘ π = πΊ & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) Β· (πΊβπ‘))) β π΄) | ||
Theorem | stoweidlem7 43970* | This lemma is used to prove that qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91, (at the top of page 91), is such that qn < Ξ΅ on π β π, and qn > 1 - Ξ΅ on π. Here it is proven that, for π large enough, 1-(k*Ξ΄/2)^n > 1 - Ξ΅ , and 1/(k*Ξ΄)^n < Ξ΅. The variable π΄ is used to represent (k*Ξ΄) in the paper, and π΅ is used to represent (k*Ξ΄/2). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ πΉ = (π β β0 β¦ ((1 / π΄)βπ)) & β’ πΊ = (π β β0 β¦ (π΅βπ)) & β’ (π β π΄ β β) & β’ (π β 1 < π΄) & β’ (π β π΅ β β+) & β’ (π β π΅ < 1) & β’ (π β πΈ β β+) β β’ (π β βπ β β ((1 β πΈ) < (1 β (π΅βπ)) β§ (1 / (π΄βπ)) < πΈ)) | ||
Theorem | stoweidlem8 43971* | Lemma for stoweid 44026: two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ β²π‘πΉ & β’ β²π‘πΊ β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) + (πΊβπ‘))) β π΄) | ||
Theorem | stoweidlem9 43972* | Lemma for stoweid 44026: here the Stone Weierstrass theorem is proven for the trivial case, T is the empty set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ (π β π = β ) & β’ (π β (π‘ β π β¦ 1) β π΄) β β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) | ||
Theorem | stoweidlem10 43973 | Lemma for stoweid 44026. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90, this lemma is an application of Bernoulli's inequality. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ ((π΄ β β β§ π β β0 β§ π΄ β€ 1) β (1 β (π Β· π΄)) β€ ((1 β π΄)βπ)) | ||
Theorem | stoweidlem11 43974* | This lemma is used to prove that there is a function π as in the proof of [BrosowskiDeutsh] p. 92 (at the top of page 92): this lemma proves that g(t) < ( j + 1 / 3 ) * Ξ΅. Here πΈ is used to represent Ξ΅ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ (π β π β β) & β’ (π β π‘ β π) & β’ (π β π β (1...π)) & β’ ((π β§ π β (0...π)) β (πβπ):πβΆβ) & β’ ((π β§ π β (0...π)) β ((πβπ)βπ‘) β€ 1) & β’ ((π β§ π β (π...π)) β ((πβπ)βπ‘) < (πΈ / π)) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) < ((π + (1 / 3)) Β· πΈ)) | ||
Theorem | stoweidlem12 43975* | Lemma for stoweid 44026. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) & β’ (π β π:πβΆβ) & β’ (π β π β β0) & β’ (π β πΎ β β0) β β’ ((π β§ π‘ β π) β (πβπ‘) = ((1 β ((πβπ‘)βπ))β(πΎβπ))) | ||
Theorem | stoweidlem13 43976 | Lemma for stoweid 44026. This lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon, in the last step of the proof in [BrosowskiDeutsh] p. 92. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ (π β πΈ β β+) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β ((π β (4 / 3)) Β· πΈ) < π) & β’ (π β π β€ ((π β (1 / 3)) Β· πΈ)) & β’ (π β ((π β (4 / 3)) Β· πΈ) < π) & β’ (π β π < ((π + (1 / 3)) Β· πΈ)) β β’ (π β (absβ(π β π)) < (2 Β· πΈ)) | ||
Theorem | stoweidlem14 43977* | There exists a π as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: π is an integer and 1 < k * Ξ΄ < 2. π· is used to represent Ξ΄ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π΄ = {π β β β£ (1 / π·) < π} & β’ (π β π· β β+) & β’ (π β π· < 1) β β’ (π β βπ β β (1 < (π Β· π·) β§ ((π Β· π·) / 2) < 1)) | ||
Theorem | stoweidlem15 43978* | This lemma is used to prove the existence of a function π as in Lemma 1 from [BrosowskiDeutsh] p. 90: π is in the subalgebra, such that 0 β€ p β€ 1, p_(t0) = 0, and p > 0 on T - U. Here (πΊβπΌ) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ (π β πΊ:(1...π)βΆπ) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ (((π β§ πΌ β (1...π)) β§ π β π) β (((πΊβπΌ)βπ) β β β§ 0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1)) | ||
Theorem | stoweidlem16 43979* | Lemma for stoweid 44026. The subset π of functions in the algebra π΄, with values in [ 0 , 1 ], is closed under multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π» = (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) β β’ ((π β§ π β π β§ π β π) β π» β π) | ||
Theorem | stoweidlem17 43980* | This lemma proves that the function π (as defined in [BrosowskiDeutsh] p. 91, at the end of page 91) belongs to the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ (π β π β β) & β’ (π β π:(0...π)βΆπ΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β πΈ β β) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ (π β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) | ||
Theorem | stoweidlem18 43981* | This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 92 when A is empty, the trivial case. Here D is used to denote the set A of Lemma 2, because the variable A is used for the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π· & β’ β²π‘π & β’ πΉ = (π‘ β π β¦ 1) & β’ π = βͺ π½ & β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) & β’ (π β π΅ β (Clsdβπ½)) & β’ (π β πΈ β β+) & β’ (π β π· = β ) β β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) | ||
Theorem | stoweidlem19 43982* | If a set of real functions is closed under multiplication and it contains constants, then it is closed under finite exponentiation. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β πΉ β π΄) & β’ (π β π β β0) β β’ (π β (π‘ β π β¦ ((πΉβπ‘)βπ)) β π΄) | ||
Theorem | stoweidlem20 43983* | If a set A of real functions from a common domain T is closed under the sum of two functions, then it is closed under the sum of a finite number of functions, indexed by G. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ πΉ = (π‘ β π β¦ Ξ£π β (1...π)((πΊβπ)βπ‘)) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ (π β πΉ β π΄) | ||
Theorem | stoweidlem21 43984* | Once the Stone Weierstrass theorem has been proven for approximating nonnegative functions, then this lemma is used to extend the result to functions with (possibly) negative values. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΊ & β’ β²π‘π» & β’ β²π‘π & β’ β²π‘π & β’ πΊ = (π‘ β π β¦ ((π»βπ‘) + π)) & β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β βπ β π΄ π:πβΆβ) & β’ (π β π» β π΄) & β’ (π β βπ‘ β π (absβ((π»βπ‘) β ((πΉβπ‘) β π))) < πΈ) β β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) | ||
Theorem | stoweidlem22 43985* | If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘πΉ & β’ β²π‘πΊ & β’ π» = (π‘ β π β¦ ((πΉβπ‘) β (πΊβπ‘))) & β’ πΌ = (π‘ β π β¦ -1) & β’ πΏ = (π‘ β π β¦ ((πΌβπ‘) Β· (πΊβπ‘))) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) β (πΊβπ‘))) β π΄) | ||
Theorem | stoweidlem23 43986* | This lemma is used to prove the existence of a function pt as in the beginning of Lemma 1 [BrosowskiDeutsh] p. 90: for all t in T - U, there exists a function p in the subalgebra, such that pt ( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘πΊ & β’ π» = (π‘ β π β¦ ((πΊβπ‘) β (πΊβπ))) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΊ β π΄) & β’ (π β (πΊβπ) β (πΊβπ)) β β’ (π β (π» β π΄ β§ (π»βπ) β (π»βπ) β§ (π»βπ) = 0)) | ||
Theorem | stoweidlem24 43987* | This lemma proves that for π sufficiently large, qn( t ) > ( 1 - epsilon ), for all π‘ in π: see Lemma 1 [BrosowskiDeutsh] p. 90, (at the bottom of page 90). π is used to represent qn in the paper, π to represent π in the paper, πΎ to represent π, π· to represent Ξ΄, and πΈ to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} & β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) & β’ (π β π:πβΆβ) & β’ (π β π β β0) & β’ (π β πΎ β β0) & β’ (π β π· β β+) & β’ (π β πΈ β β+) & β’ (π β (1 β πΈ) < (1 β (((πΎ Β· π·) / 2)βπ))) & β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) β β’ ((π β§ π‘ β π) β (1 β πΈ) < (πβπ‘)) | ||
Theorem | stoweidlem25 43988* | This lemma proves that for n sufficiently large, qn( t ) < Ξ΅, for all π‘ in π β π: see Lemma 1 [BrosowskiDeutsh] p. 91 (at the top of page 91). π is used to represent qn in the paper, π to represent n in the paper, πΎ to represent k, π· to represent Ξ΄, π to represent p, and πΈ to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) & β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π· β β+) & β’ (π β π:πβΆβ) & β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) & β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) & β’ (π β πΈ β β+) & β’ (π β (1 / ((πΎ Β· π·)βπ)) < πΈ) β β’ ((π β§ π‘ β (π β π)) β (πβπ‘) < πΈ) | ||
Theorem | stoweidlem26 43989* | This lemma is used to prove that there is a function π as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * Ξ΅. Here πΏ is used to represnt j in the paper, π· is used to represent A in the paper, π is used to represent t, and πΈ is used to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²ππ & β’ β²π‘π & β’ π· = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) & β’ π΅ = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) & β’ (π β π β β) & β’ (π β π β V) & β’ (π β πΏ β (1...π)) & β’ (π β π β ((π·βπΏ) β (π·β(πΏ β 1)))) & β’ (π β πΉ:πβΆβ) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) & β’ ((π β§ π β (0...π)) β (πβπ):πβΆβ) & β’ ((π β§ π β (0...π) β§ π‘ β π) β 0 β€ ((πβπ)βπ‘)) & β’ ((π β§ π β (0...π) β§ π‘ β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ‘)) β β’ (π β ((πΏ β (4 / 3)) Β· πΈ) < ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ)) | ||
Theorem | stoweidlem27 43990* | This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Here (πβπ) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ πΊ = (π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) & β’ (π β π β V) & β’ (π β π β β) & β’ (π β π Fn ran πΊ) & β’ (π β ran πΊ β V) & β’ ((π β§ π β ran πΊ) β (πβπ) β π) & β’ (π β πΉ:(1...π)β1-1-ontoβran πΊ) & β’ (π β (π β π) β βͺ π) & β’ β²π‘π & β’ β²π€π & β’ β²βπ β β’ (π β βπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) | ||
Theorem | stoweidlem28 43991* | There exists a Ξ΄ as in Lemma 1 [BrosowskiDeutsh] p. 90: 0 < delta < 1 and p >= delta on π β π. Here π is used to represent Ξ΄ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ (π β π½ β Comp) & β’ (π β π β (π½ Cn πΎ)) & β’ (π β βπ‘ β (π β π)0 < (πβπ‘)) & β’ (π β π β π½) β β’ (π β βπ(π β β+ β§ π < 1 β§ βπ‘ β (π β π)π β€ (πβπ‘))) | ||
Theorem | stoweidlem29 43992* | When the hypothesis for the extreme value theorem hold, then the inf of the range of the function belongs to the range, it is real and it a lower bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.) (Revised by AV, 13-Sep-2020.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ π = βͺ π½ & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π β β ) β β’ (π β (inf(ran πΉ, β, < ) β ran πΉ β§ inf(ran πΉ, β, < ) β β β§ βπ‘ β π inf(ran πΉ, β, < ) β€ (πΉβπ‘))) | ||
Theorem | stoweidlem30 43993* | This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (πΊβπ) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = (π‘ β π β¦ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ ((π β§ π β π) β (πβπ) = ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ))) | ||
Theorem | stoweidlem31 43994* | This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that π is a finite subset of π, π₯ indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all π ranging in the finite indexing set, 0 β€ xi β€ 1, xi < Ξ΅ / m on V(ti), and xi > 1 - Ξ΅ / m on π΅. Here M is used to represent m in the paper, πΈ is used to represent Ξ΅ in the paper, vi is used to represent V(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²βπ & β’ β²π‘π & β’ β²π€π & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} & β’ πΊ = (π€ β π β¦ {β β π΄ β£ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < (πΈ / π) β§ βπ‘ β (π β π)(1 β (πΈ / π)) < (ββπ‘))}) & β’ (π β π β π) & β’ (π β π β β) & β’ (π β π£:(1...π)β1-1-ontoβπ ) & β’ (π β πΈ β β+) & β’ (π β π΅ β (π β π)) & β’ (π β π β V) & β’ (π β π΄ β V) & β’ (π β ran πΊ β Fin) β β’ (π β βπ₯(π₯:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π₯βπ)βπ‘)))) | ||
Theorem | stoweidlem32 43995* | If a set A of real functions from a common domain T is a subalgebra and it contains constants, then it is closed under the sum of a finite number of functions, indexed by G and finally scaled by a real Y. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ π = (π‘ β π β¦ (π Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) & β’ πΉ = (π‘ β π β¦ Ξ£π β (1...π)((πΊβπ)βπ‘)) & β’ π» = (π‘ β π β¦ π) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ π β π΄) β π:πβΆβ) β β’ (π β π β π΄) | ||
Theorem | stoweidlem33 43996* | If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘πΊ & β’ β²π‘π & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) β (πΊβπ‘))) β π΄) | ||
Theorem | stoweidlem34 43997* | This lemma proves that for all π‘ in π there is a π as in the proof of [BrosowskiDeutsh] p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * Ξ΅ < f(t) <= (j-1/3) * Ξ΅ , g(t) < (j+1/3) * Ξ΅, and g(t) > (j-4/3) * Ξ΅. Here πΈ is used to represent Ξ΅ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²ππ & β’ β²π‘π & β’ π· = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) & β’ π΅ = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) & β’ π½ = (π‘ β π β¦ {π β (1...π) β£ π‘ β (π·βπ)}) & β’ (π β π β β) & β’ (π β π β V) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π‘ β π) β 0 β€ (πΉβπ‘)) & β’ ((π β§ π‘ β π) β (πΉβπ‘) < ((π β 1) Β· πΈ)) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) & β’ ((π β§ π β (0...π)) β (πβπ):πβΆβ) & β’ ((π β§ π β (0...π) β§ π‘ β π) β 0 β€ ((πβπ)βπ‘)) & β’ ((π β§ π β (0...π) β§ π‘ β π) β ((πβπ)βπ‘) β€ 1) & β’ ((π β§ π β (0...π) β§ π‘ β (π·βπ)) β ((πβπ)βπ‘) < (πΈ / π)) & β’ ((π β§ π β (0...π) β§ π‘ β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ‘)) β β’ (π β βπ‘ β π βπ β β ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘)))) | ||
Theorem | stoweidlem35 43998* | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Here (πβπ) is used to represent p_(ti) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π€π & β’ β²βπ & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} & β’ πΊ = (π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) & β’ (π β π΄ β V) & β’ (π β π β Fin) & β’ (π β π β π) & β’ (π β (π β π) β βͺ π) & β’ (π β (π β π) β β ) β β’ (π β βπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) | ||
Theorem | stoweidlem36 43999* | This lemma is used to prove the existence of a function pt as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function p in the subalgebra, such that pt ( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Z is used for t0 , S is used for t e. T - U , h is used for pt . G is used for (ht)^2 and the final h is a normalized version of G ( divided by its norm, see the variable N ). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²βπ & β’ β²π‘π» & β’ β²π‘πΉ & β’ β²π‘πΊ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = βͺ π½ & β’ πΊ = (π‘ β π β¦ ((πΉβπ‘) Β· (πΉβπ‘))) & β’ π = sup(ran πΊ, β, < ) & β’ π» = (π‘ β π β¦ ((πΊβπ‘) / π)) & β’ (π β π½ β Comp) & β’ (π β π΄ β (π½ Cn πΎ)) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΉ β π΄) & β’ (π β (πΉβπ) β (πΉβπ)) & β’ (π β (πΉβπ) = 0) β β’ (π β ββ(β β π β§ 0 < (ββπ))) | ||
Theorem | stoweidlem37 44000* | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, (πΊβπ) is used for p_(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = (π‘ β π β¦ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ (π β π β π) β β’ (π β (πβπ) = 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |