![]() |
Metamath
Proof Explorer Theorem List (p. 451 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmvolss 45001 | Lebesgue measurable sets are subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ dom vol β π« β | ||
Theorem | ismbl3 45002* | The predicate "π΄ is Lebesgue-measurable". Similar to ismbl2 25277, 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 45003 | The function that assigns the Lebesgue measure to open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (vol β (,)):(β* Γ β*)βΆ(0[,]+β) | ||
Theorem | ovolsplit 45004 | 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 45005 | 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 45006 | The measure of an open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ ((π΄ β β β§ π΅ β β) β (volβ(π΄(,)π΅)) = if(π΄ β€ π΅, (π΅ β π΄), 0)) | ||
Theorem | fvvolicof 45007 | 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 45008 | 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 45009* | The predicate "π΄ is Lebesgue-measurable". Similar to ismbl 25276, 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 45010* | ((vol β (,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆ(β* Γ β*)) β β’ (π β ((vol β (,)) β πΉ) = (π₯ β π΄ β¦ (volβ((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯)))))) | ||
Theorem | volicoff 45011 | ((vol β [,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΉ:π΄βΆ(β Γ β*)) β β’ (π β ((vol β [,)) β πΉ):π΄βΆ(0[,]+β)) | ||
Theorem | voliooicof 45012 | 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 45013* | ((vol β [,)) β πΉ) expressed in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯πΉ & β’ (π β πΉ:π΄βΆ(β Γ β*)) β β’ (π β ((vol β [,)) β πΉ) = (π₯ β π΄ β¦ (volβ((1st β(πΉβπ₯))[,)(2nd β(πΉβπ₯)))))) | ||
Theorem | volicc 45014 | The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (volβ(π΄[,]π΅)) = (π΅ β π΄)) | ||
Theorem | voliccico 45015 | 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 45016 | The domain of a measurable function is a subset of the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (πΉ β MblFn β dom πΉ β β) | ||
Theorem | stoweidlem1 45017 | Lemma for stoweid 45079. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 14197. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π· β β+) & β’ (π β π΄ β β+) & β’ (π β 0 β€ π΄) & β’ (π β π΄ β€ 1) & β’ (π β π· β€ π΄) β β’ (π β ((1 β (π΄βπ))β(πΎβπ)) β€ (1 / ((πΎ Β· π·)βπ))) | ||
Theorem | stoweidlem2 45018* | lemma for stoweid 45079: 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 45019* | Lemma for stoweid 45079: 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 45020* | Lemma for stoweid 45079: a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) β β’ ((π β§ π΅ β β) β (π‘ β π β¦ π΅) β π΄) | ||
Theorem | stoweidlem5 45021* | 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 45022* | Lemma for stoweid 45079: two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘ π = πΉ & β’ β²π‘ π = πΊ & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) Β· (πΊβπ‘))) β π΄) | ||
Theorem | stoweidlem7 45023* | 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 45024* | Lemma for stoweid 45079: two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ β²π‘πΉ & β’ β²π‘πΊ β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) + (πΊβπ‘))) β π΄) | ||
Theorem | stoweidlem9 45025* | Lemma for stoweid 45079: 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 45026 | Lemma for stoweid 45079. 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 45027* | 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 45028* | Lemma for stoweid 45079. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) & β’ (π β π:πβΆβ) & β’ (π β π β β0) & β’ (π β πΎ β β0) β β’ ((π β§ π‘ β π) β (πβπ‘) = ((1 β ((πβπ‘)βπ))β(πΎβπ))) | ||
Theorem | stoweidlem13 45029 | Lemma for stoweid 45079. 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 45030* | 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 45031* | 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 45032* | Lemma for stoweid 45079. 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 45033* | 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 45034* | 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 45035* | 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 45036* | 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 45037* | 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 45038* | 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 45039* | 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 45040* | 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 45041* | 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 45042* | 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 45043* | 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 45044* | 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 45045* | 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 45046* | 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 45047* | 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 45048* | 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 45049* | 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 45050* | 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 45051* | 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 45052* | 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 45053* | 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) | ||
Theorem | stoweidlem38 45054* | 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 β€ (πβπ) β§ (πβπ) β€ 1)) | ||
Theorem | stoweidlem39 45055* | 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 i ranging in the finite indexing set, 0 β€ xi β€ 1, xi < Ξ΅ / m on V(ti), and xi > 1 - Ξ΅ / m on π΅. Here π· is used to represent A in the paper's Lemma 2 (because π΄ is used for the subalgebra), π is used to represent m in the paper, πΈ is used to represent Ξ΅, and vi is used to represent V(ti). π is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²βπ & β’ β²π‘π & β’ β²π€π & β’ π = (π β π΅) & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} & β’ (π β π β (π« π β© Fin)) & β’ (π β π· β βͺ π) & β’ (π β π· β β ) & β’ (π β πΈ β β+) & β’ (π β π΅ β π) & β’ (π β π β V) & β’ (π β π΄ β V) β β’ (π β βπ β β βπ£(π£:(1...π)βΆπ β§ π· β βͺ ran π£ β§ βπ₯(π₯:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (π£βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π₯βπ)βπ‘))))) | ||
Theorem | stoweidlem40 45056* | This lemma proves that qn is in the subalgebra, as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90. Q is used to represent qn in the paper, N is used to represent n in the paper, and M is used to represent k^n in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))βπ)) & β’ πΉ = (π‘ β π β¦ (1 β ((πβπ‘)βπ))) & β’ πΊ = (π‘ β π β¦ 1) & β’ π» = (π‘ β π β¦ ((πβπ‘)βπ)) & β’ (π β π β π΄) & β’ (π β π:πβΆβ) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β π β β) & β’ (π β π β β) β β’ (π β π β π΄) | ||
Theorem | stoweidlem41 45057* | This lemma is used to prove that there exists x as in Lemma 1 of [BrosowskiDeutsh] p. 90: 0 <= x(t) <= 1 for all t in T, x(t) < epsilon for all t in V, x(t) > 1 - epsilon for all t in T \ U. Here we prove the very last step of the proof of Lemma 1: "The result follows from taking x = 1 - qn";. Here πΈ is used to represent Ξ΅ in the paper, and π¦ to represent qn in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ π = (π‘ β π β¦ (1 β (π¦βπ‘))) & β’ πΉ = (π‘ β π β¦ 1) & β’ π β π & β’ (π β π¦ β π΄) & β’ (π β π¦:πβΆβ) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π€ β β) β (π‘ β π β¦ π€) β π΄) & β’ (π β πΈ β β+) & β’ (π β βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)) & β’ (π β βπ‘ β π (1 β πΈ) < (π¦βπ‘)) & β’ (π β βπ‘ β (π β π)(π¦βπ‘) < πΈ) β β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π (π₯βπ‘) < πΈ β§ βπ‘ β (π β π)(1 β πΈ) < (π₯βπ‘))) | ||
Theorem | stoweidlem42 45058* | This lemma is used to prove that π₯ built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x > 1 - Ξ΅ on B. Here π is used to represent π₯ in the paper, and E is used to represent Ξ΅ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ β²π‘π & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β (1...π)) β βπ‘ β π΅ (1 β (πΈ / π)) < ((πβπ)βπ‘)) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) & β’ ((π β§ π β π) β π:πβΆβ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) & β’ (π β π β V) & β’ (π β π΅ β π) β β’ (π β βπ‘ β π΅ (1 β πΈ) < (πβπ‘)) | ||
Theorem | stoweidlem43 45059* | 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 pt in the subalgebra, such that pt( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Hera Z is used for t0 , S is used for t e. T - U , h is used for pt. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ β²βπ & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = βͺ π½ & β’ (π β π½ β Comp) & β’ (π β π΄ β (π½ Cn πΎ)) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β π β π) & β’ (π β π β (π β π)) β β’ (π β ββ(β β π β§ 0 < (ββπ))) | ||
Theorem | stoweidlem44 45060* | 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 to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = (π‘ β π β¦ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ) & β’ (π β βπ‘ β (π β π)βπ β (1...π)0 < ((πΊβπ)βπ‘)) & β’ π = βͺ π½ & β’ (π β π΄ β (π½ Cn πΎ)) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β π β π) β β’ (π β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) | ||
Theorem | stoweidlem45 45061* | This lemma proves that, given an appropriate πΎ (in another theorem we prove such a πΎ exists), there exists a function qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 ( at the top of page 91): 0 <= qn <= 1 , qn < Ξ΅ on T \ U, and qn > 1 - Ξ΅ on π. We use y to represent the final qn in the paper (the one with n large enough), π to represent π in the paper, πΎ to represent π, π· to represent Ξ΄, πΈ to represent Ξ΅, and π to represent π. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} & β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) & β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π· β β+) & β’ (π β π· < 1) & β’ (π β π β π΄) & β’ (π β π:πβΆβ) & β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) & β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β πΈ β β+) & β’ (π β (1 β πΈ) < (1 β (((πΎ Β· π·) / 2)βπ))) & β’ (π β (1 / ((πΎ Β· π·)βπ)) < πΈ) β β’ (π β βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ)) | ||
Theorem | stoweidlem46 45062* | This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, are a cover of T \ U. Using this lemma, in a later theorem we will prove that a finite subcover exists. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²βπ & β’ β²ππ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} & β’ π = βͺ π½ & β’ (π β π½ β Comp) & β’ (π β π΄ β (π½ Cn πΎ)) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β π β π) & β’ (π β π β V) β β’ (π β (π β π) β βͺ π) | ||
Theorem | stoweidlem47 45063* | Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ β²π‘π & β’ π = βͺ π½ & β’ πΊ = (π Γ {-π}) & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Top) & β’ πΆ = (π½ Cn πΎ) & β’ (π β πΉ β πΆ) & β’ (π β π β β) β β’ (π β (π‘ β π β¦ ((πΉβπ‘) β π)) β πΆ) | ||
Theorem | stoweidlem48 45064* | This lemma is used to prove that π₯ built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x < Ξ΅ on π΄. Here π is used to represent π₯ in the paper, πΈ is used to represent Ξ΅ in the paper, and π· is used to represent π΄ in the paper (because π΄ is always used to represent the subalgebra). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ (π β π:(1...π)βΆπ) & β’ (π β π· β βͺ ran π) & β’ (π β π· β π) & β’ ((π β§ π β (1...π)) β βπ‘ β (πβπ)((πβπ)βπ‘) < πΈ) & β’ (π β π β V) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ (π β πΈ β β+) β β’ (π β βπ‘ β π· (πβπ‘) < πΈ) | ||
Theorem | stoweidlem49 45065* | There exists a function qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 (at the top of page 91): 0 <= qn <= 1 , qn < Ξ΅ on π β π, and qn > 1 - Ξ΅ on π. Here y is used to represent the final qn in the paper (the one with n large enough), π represents π in the paper, πΎ represents π, π· represents Ξ΄, πΈ represents Ξ΅, and π represents π. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} & β’ (π β π· β β+) & β’ (π β π· < 1) & β’ (π β π β π΄) & β’ (π β π:πβΆβ) & β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) & β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ (π β πΈ β β+) β β’ (π β βπ¦ β π΄ (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β§ βπ‘ β π (1 β πΈ) < (π¦βπ‘) β§ βπ‘ β (π β π)(π¦βπ‘) < πΈ)) | ||
Theorem | stoweidlem50 45066* | This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, contain a finite subcover of T \ U. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π½ β Comp) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β π β π) β β’ (π β βπ’(π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) | ||
Theorem | stoweidlem51 45067* | There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here π· is used to represent π΄ in the paper, because here π΄ is used for the subalgebra of functions. πΈ is used to represent Ξ΅ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ β²π€π & β’ β²π€π & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π€ β π) β π€ β π) & β’ (π β π· β βͺ ran π) & β’ (π β π· β π) & β’ (π β π΅ β π) & β’ ((π β§ π β (1...π)) β βπ‘ β (πβπ)((πβπ)βπ‘) < (πΈ / π)) & β’ ((π β§ π β (1...π)) β βπ‘ β π΅ (1 β (πΈ / π)) < ((πβπ)βπ‘)) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ (π β π β V) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) | ||
Theorem | stoweidlem52 45068* | There exists a neighborhood V as in Lemma 1 of [BrosowskiDeutsh] p. 90. Here Z is used to represent t0 in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {π‘ β π β£ (πβπ‘) < (π· / 2)} & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) & β’ (π β π· β β+) & β’ (π β π· < 1) & β’ (π β π β π½) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) & β’ (π β (πβπ) = 0) & β’ (π β βπ‘ β (π β π)π· β€ (πβπ‘)) β β’ (π β βπ£ β π½ ((π β π£ β§ π£ β π) β§ βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π£ (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) | ||
Theorem | stoweidlem53 45069* | This lemma is used to prove the existence of a function π as in Lemma 1 of [BrosowskiDeutsh] p. 90: π is in the subalgebra, such that 0 β€ π β€ 1, p_(t0) = 0, and 0 < π on π β π. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π½ β Comp) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β (π β π) β β ) & β’ (π β π β π) β β’ (π β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) | ||
Theorem | stoweidlem54 45070* | There exists a function π₯ as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here π· is used to represent π΄ in the paper, because here π΄ is used for the subalgebra of functions. πΈ is used to represent Ξ΅ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ β²π¦π & β’ β²π€π & β’ π = βͺ π½ & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π β π΄) β π:πβΆβ) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ (π β π΅ β π) & β’ (π β π· β βͺ ran π) & β’ (π β π· β π) & β’ (π β βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) & β’ (π β π β V) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) | ||
Theorem | stoweidlem55 45071* | This lemma proves the existence of a function p as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Here Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β π β π) & β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} & β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} β β’ (π β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) | ||
Theorem | stoweidlem56 45072* | This theorem proves Lemma 1 in [BrosowskiDeutsh] p. 90. Here π is used to represent t0 in the paper, π£ is used to represent π in the paper, and π is used to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π¦ β β) β (π‘ β π β¦ π¦) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π β π½) & β’ (π β π β π) β β’ (π β βπ£ β π½ ((π β π£ β§ π£ β π) β§ βπ β β+ βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π£ (π₯βπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (π₯βπ‘)))) | ||
Theorem | stoweidlem57 45073* | There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. In this theorem, it is proven the non-trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π· & β’ β²π‘π & β’ β²π‘π & β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} & β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ π = (π β π΅) & β’ (π β π½ β Comp) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π΅ β (Clsdβπ½)) & β’ (π β π· β (Clsdβπ½)) & β’ (π β (π΅ β© π·) = β ) & β’ (π β π· β β ) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) | ||
Theorem | stoweidlem58 45074* | This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘π· & β’ β²π‘π & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π½ β Comp) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β π΅ β (Clsdβπ½)) & β’ (π β π· β (Clsdβπ½)) & β’ (π β (π΅ β© π·) = β ) & β’ π = (π β π΅) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) | ||
Theorem | stoweidlem59 45075* | This lemma proves that there exists a function π₯ as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: xj is in the subalgebra, 0 <= xj <= 1, xj < Ξ΅ / n on Aj (meaning A in the paper), xj > 1 - \epsilon / n on Bj. Here π· is used to represent A in the paper (because A is used for the subalgebra of functions), πΈ is used to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ π· = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) & β’ π΅ = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) & β’ π = {π¦ β π΄ β£ βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)} & β’ π» = (π β (0...π) β¦ {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) & β’ (π β π½ β Comp) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π¦ β β) β (π‘ β π β¦ π¦) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β πΉ β πΆ) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) & β’ (π β π β β) β β’ (π β βπ₯(π₯:(0...π)βΆπ΄ β§ βπ β (0...π)(βπ‘ β π (0 β€ ((π₯βπ)βπ‘) β§ ((π₯βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < ((π₯βπ)βπ‘)))) | ||
Theorem | stoweidlem60 45076* | This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all π‘ in π, there is a π such that (j-4/3)*Ξ΅ < f(t) <= (j-1/3)*Ξ΅ and (j-4/3)*Ξ΅ < g(t) < (j+1/3)*Ξ΅. Here πΉ is used to represent f in the paper, and πΈ is used to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ π· = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) & β’ π΅ = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) & β’ (π β π½ β Comp) & β’ (π β π β β ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π¦ β β) β (π‘ β π β¦ π¦) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β πΉ β πΆ) & β’ (π β βπ‘ β π 0 β€ (πΉβπ‘)) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ β π΄ βπ‘ β π βπ β β ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) | ||
Theorem | stoweidlem61 45077* | This lemma proves that there exists a function π as in the proof in [BrosowskiDeutsh] p. 92: π is in the subalgebra, and for all π‘ in π, abs( f(t) - g(t) ) < 2*Ξ΅. Here πΉ is used to represent f in the paper, and πΈ is used to represent Ξ΅. For this lemma there's the further assumption that the function πΉ to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ π = βͺ π½ & β’ (π β π β β ) & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β πΉ β πΆ) & β’ (π β βπ‘ β π 0 β€ (πΉβπ‘)) & β’ (π β πΈ β β+) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < (2 Β· πΈ)) | ||
Theorem | stoweidlem62 45078* | This theorem proves the Stone Weierstrass theorem for the non-trivial case in which T is nonempty. The proof follows [BrosowskiDeutsh] p. 89 (through page 92). (Contributed by Glauco Siliprandi, 20-Apr-2017.) (Revised by AV, 13-Sep-2020.) |
β’ β²π‘πΉ & β’ β²ππ & β’ β²π‘π & β’ π» = (π‘ β π β¦ ((πΉβπ‘) β inf(ran πΉ, β, < ))) & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ (π β π½ β Comp) & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) & β’ (π β πΉ β πΆ) & β’ (π β πΈ β β+) & β’ (π β π β β ) & β’ (π β πΈ < (1 / 3)) β β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) | ||
Theorem | stoweid 45079* | This theorem proves the Stone-Weierstrass theorem for real-valued functions: let π½ be a compact topology on π, and πΆ be the set of real continuous functions on π. Assume that π΄ is a subalgebra of πΆ (closed under addition and multiplication of functions) containing constant functions and discriminating points (if π and π‘ are distinct points in π, then there exists a function β in π΄ such that h(r) is distinct from h(t) ). Then, for any continuous function πΉ and for any positive real πΈ, there exists a function π in the subalgebra π΄, such that π approximates πΉ up to πΈ (πΈ represents the usual Ξ΅ value). As a classical example, given any a, b reals, the closed interval π = [π, π] could be taken, along with the subalgebra π΄ of real polynomials on π, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [π, π]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π‘πΉ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β π΄ β πΆ) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) & β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β ββ β π΄ (ββπ) β (ββπ‘)) & β’ (π β πΉ β πΆ) & β’ (π β πΈ β β+) β β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) | ||
Theorem | stowei 45080* | This theorem proves the Stone-Weierstrass theorem for real-valued functions: let π½ be a compact topology on π, and πΆ be the set of real continuous functions on π. Assume that π΄ is a subalgebra of πΆ (closed under addition and multiplication of functions) containing constant functions and discriminating points (if π and π‘ are distinct points in π, then there exists a function β in π΄ such that h(r) is distinct from h(t) ). Then, for any continuous function πΉ and for any positive real πΈ, there exists a function π in the subalgebra π΄, such that π approximates πΉ up to πΈ (πΈ represents the usual Ξ΅ value). As a classical example, given any a, b reals, the closed interval π = [π, π] could be taken, along with the subalgebra π΄ of real polynomials on π, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [π, π]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. The deduction version of this theorem is stoweid 45079: often times it will be better to use stoweid 45079 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ πΎ = (topGenβran (,)) & β’ π½ β Comp & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ π΄ β πΆ & β’ ((π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ ((π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) & β’ (π₯ β β β (π‘ β π β¦ π₯) β π΄) & β’ ((π β π β§ π‘ β π β§ π β π‘) β ββ β π΄ (ββπ) β (ββπ‘)) & β’ πΉ β πΆ & β’ πΈ β β+ β β’ βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ | ||
Theorem | wallispilem1 45081* | πΌ is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) & β’ (π β π β β0) β β’ (π β (πΌβ(π + 1)) β€ (πΌβπ)) | ||
Theorem | wallispilem2 45082* | A first set of properties for the sequence πΌ that will be used in the proof of the Wallis product formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) β β’ ((πΌβ0) = Ο β§ (πΌβ1) = 2 β§ (π β (β€β₯β2) β (πΌβπ) = (((π β 1) / π) Β· (πΌβ(π β 2))))) | ||
Theorem | wallispilem3 45083* | I maps to real values. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) β β’ (π β β0 β (πΌβπ) β β+) | ||
Theorem | wallispilem4 45084* | πΉ maps to explicit expression for the ratio of two consecutive values of πΌ. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ πΉ = (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1)))) & β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ§)βπ) dπ§) & β’ πΊ = (π β β β¦ ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) & β’ π» = (π β β β¦ ((Ο / 2) Β· (1 / (seq1( Β· , πΉ)βπ)))) β β’ πΊ = π» | ||
Theorem | wallispilem5 45085* | The sequence π» converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ πΉ = (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1)))) & β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) & β’ πΊ = (π β β β¦ ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) & β’ π» = (π β β β¦ ((Ο / 2) Β· (1 / (seq1( Β· , πΉ)βπ)))) & β’ πΏ = (π β β β¦ (((2 Β· π) + 1) / (2 Β· π))) β β’ π» β 1 | ||
Theorem | wallispi 45086* | Wallis' formula for Ο : Wallis' product converges to Ο / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΉ = (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1)))) & β’ π = (π β β β¦ (seq1( Β· , πΉ)βπ)) β β’ π β (Ο / 2) | ||
Theorem | wallispi2lem1 45087 | An intermediate step between the first version of the Wallis' formula for Ο and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ (π β β β (seq1( Β· , (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1)))))βπ) = ((1 / ((2 Β· π) + 1)) Β· (seq1( Β· , (π β β β¦ (((2 Β· π)β4) / (((2 Β· π) Β· ((2 Β· π) β 1))β2))))βπ))) | ||
Theorem | wallispi2lem2 45088 | Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for Ο . (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ (π β β β (seq1( Β· , (π β β β¦ (((2 Β· π)β4) / (((2 Β· π) Β· ((2 Β· π) β 1))β2))))βπ) = (((2β(4 Β· π)) Β· ((!βπ)β4)) / ((!β(2 Β· π))β2))) | ||
Theorem | wallispi2 45089 | An alternative version of Wallis' formula for Ο ; this second formula uses factorials and it is later used to prove Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (π β β β¦ ((((2β(4 Β· π)) Β· ((!βπ)β4)) / ((!β(2 Β· π))β2)) / ((2 Β· π) + 1))) β β’ π β (Ο / 2) | ||
Theorem | stirlinglem1 45090 | A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ π» = (π β β β¦ ((πβ2) / (π Β· ((2 Β· π) + 1)))) & β’ πΉ = (π β β β¦ (1 β (1 / ((2 Β· π) + 1)))) & β’ πΊ = (π β β β¦ (1 / ((2 Β· π) + 1))) & β’ πΏ = (π β β β¦ (1 / π)) β β’ π» β (1 / 2) | ||
Theorem | stirlinglem2 45091 | π΄ maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) β β’ (π β β β (π΄βπ) β β+) | ||
Theorem | stirlinglem3 45092 | Long but simple algebraic transformations are applied to show that π, the Wallis formula for Ο , can be expressed in terms of π΄, the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the π΄, in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π· = (π β β β¦ (π΄β(2 Β· π))) & β’ πΈ = (π β β β¦ ((ββ(2 Β· π)) Β· ((π / e)βπ))) & β’ π = (π β β β¦ ((((2β(4 Β· π)) Β· ((!βπ)β4)) / ((!β(2 Β· π))β2)) / ((2 Β· π) + 1))) β β’ π = (π β β β¦ ((((π΄βπ)β4) / ((π·βπ)β2)) Β· ((πβ2) / (π Β· ((2 Β· π) + 1))))) | ||
Theorem | stirlinglem4 45093* | Algebraic manipulation of ((π΅ n ) - ( B (π + 1))). It will be used in other theorems to show that π΅ is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ π½ = (π β β β¦ ((((1 + (2 Β· π)) / 2) Β· (logβ((π + 1) / π))) β 1)) β β’ (π β β β ((π΅βπ) β (π΅β(π + 1))) = (π½βπ)) | ||
Theorem | stirlinglem5 45094* | If π is between 0 and 1, then a series (without alternating negative and positive terms) is given that converges to log((1+T)/(1-T)). (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π· = (π β β β¦ ((-1β(π β 1)) Β· ((πβπ) / π))) & β’ πΈ = (π β β β¦ ((πβπ) / π)) & β’ πΉ = (π β β β¦ (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π))) & β’ π» = (π β β0 β¦ (2 Β· ((1 / ((2 Β· π) + 1)) Β· (πβ((2 Β· π) + 1))))) & β’ πΊ = (π β β0 β¦ ((2 Β· π) + 1)) & β’ (π β π β β+) & β’ (π β (absβπ) < 1) β β’ (π β seq0( + , π») β (logβ((1 + π) / (1 β π)))) | ||
Theorem | stirlinglem6 45095* | A series that converges to log((π + 1) / π). (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π» = (π β β0 β¦ (2 Β· ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β((2 Β· π) + 1))))) β β’ (π β β β seq0( + , π») β (logβ((π + 1) / π))) | ||
Theorem | stirlinglem7 45096* | Algebraic manipulation of the formula for J(n). (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π½ = (π β β β¦ ((((1 + (2 Β· π)) / 2) Β· (logβ((π + 1) / π))) β 1)) & β’ πΎ = (π β β β¦ ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β(2 Β· π)))) & β’ π» = (π β β0 β¦ (2 Β· ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β((2 Β· π) + 1))))) β β’ (π β β β seq1( + , πΎ) β (π½βπ)) | ||
Theorem | stirlinglem8 45097 | If π΄ converges to πΆ, then πΉ converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππ΄ & β’ β²ππ· & β’ π· = (π β β β¦ (π΄β(2 Β· π))) & β’ (π β π΄:ββΆβ+) & β’ πΉ = (π β β β¦ (((π΄βπ)β4) / ((π·βπ)β2))) & β’ πΏ = (π β β β¦ ((π΄βπ)β4)) & β’ π = (π β β β¦ ((π·βπ)β2)) & β’ ((π β§ π β β) β (π·βπ) β β+) & β’ (π β πΆ β β+) & β’ (π β π΄ β πΆ) β β’ (π β πΉ β (πΆβ2)) | ||
Theorem | stirlinglem9 45098* | ((π΅βπ) β (π΅β(π + 1))) is expressed as a limit of a series. This result will be used both to prove that π΅ is decreasing and to prove that π΅ is bounded (below). It will follow that π΅ converges in the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ π½ = (π β β β¦ ((((1 + (2 Β· π)) / 2) Β· (logβ((π + 1) / π))) β 1)) & β’ πΎ = (π β β β¦ ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β(2 Β· π)))) β β’ (π β β β seq1( + , πΎ) β ((π΅βπ) β (π΅β(π + 1)))) | ||
Theorem | stirlinglem10 45099* | A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole π΅ sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ πΎ = (π β β β¦ ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β(2 Β· π)))) & β’ πΏ = (π β β β¦ ((1 / (((2 Β· π) + 1)β2))βπ)) β β’ (π β β β ((π΅βπ) β (π΅β(π + 1))) β€ ((1 / 4) Β· (1 / (π Β· (π + 1))))) | ||
Theorem | stirlinglem11 45100* | π΅ is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ πΎ = (π β β β¦ ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β(2 Β· π)))) β β’ (π β β β (π΅β(π + 1)) < (π΅βπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |