Home | Metamath
Proof Explorer Theorem List (p. 441 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | stoweidlem7 44001* | 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 44002* | Lemma for stoweid 44057: two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) & β’ β²π‘πΉ & β’ β²π‘πΊ β β’ ((π β§ πΉ β π΄ β§ πΊ β π΄) β (π‘ β π β¦ ((πΉβπ‘) + (πΊβπ‘))) β π΄) | ||
Theorem | stoweidlem9 44003* | Lemma for stoweid 44057: 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 44004 | Lemma for stoweid 44057. 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 44005* | 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 44006* | Lemma for stoweid 44057. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = (π‘ β π β¦ ((1 β ((πβπ‘)βπ))β(πΎβπ))) & β’ (π β π:πβΆβ) & β’ (π β π β β0) & β’ (π β πΎ β β0) β β’ ((π β§ π‘ β π) β (πβπ‘) = ((1 β ((πβπ‘)βπ))β(πΎβπ))) | ||
Theorem | stoweidlem13 44007 | Lemma for stoweid 44057. 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 44008* | 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 44009* | 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 44010* | Lemma for stoweid 44057. 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 44011* | 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 44012* | 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 44013* | 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 44014* | 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 44015* | 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 44016* | 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 44017* | 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 44018* | 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 44019* | 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 44020* | 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 44021* | 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 44022* | 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 44023* | 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 44024* | 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 44025* | 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 44026* | 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 44027* | 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 44028* | 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 44029* | 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 44030* | 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 44031* | 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 44032* | 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 44033* | 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 44034* | 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 44035* | 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 44036* | 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 44037* | 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 44038* | 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 44039* | 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 44040* | 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 44041* | 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 44042* | 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 44043* | 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 44044* | 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 44045* | 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 44046* | 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 44047* | 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 44048* | 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 44049* | 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 44050* | 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 44051* | 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 44052* | 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 44053* | 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 44054* | 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 44055* | 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 44056* | 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 44057* | 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 44058* | 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 44057: often times it will be better to use stoweid 44057 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 44059* | πΌ is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) & β’ (π β π β β0) β β’ (π β (πΌβ(π + 1)) β€ (πΌβπ)) | ||
Theorem | wallispilem2 44060* | 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 44061* | I maps to real values. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΌ = (π β β0 β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) β β’ (π β β0 β (πΌβπ) β β+) | ||
Theorem | wallispilem4 44062* | πΉ 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 44063* | 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 44064* | 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 44065 | 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 44066 | 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 44067 | 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 44068 | 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 44069 | π΄ maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) β β’ (π β β β (π΄βπ) β β+) | ||
Theorem | stirlinglem3 44070 | 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 44071* | 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 44072* | 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 44073* | 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 44074* | 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 44075 | If π΄ converges to πΆ, then πΉ converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππ΄ & β’ β²ππ· & β’ π· = (π β β β¦ (π΄β(2 Β· π))) & β’ (π β π΄:ββΆβ+) & β’ πΉ = (π β β β¦ (((π΄βπ)β4) / ((π·βπ)β2))) & β’ πΏ = (π β β β¦ ((π΄βπ)β4)) & β’ π = (π β β β¦ ((π·βπ)β2)) & β’ ((π β§ π β β) β (π·βπ) β β+) & β’ (π β πΆ β β+) & β’ (π β π΄ β πΆ) β β’ (π β πΉ β (πΆβ2)) | ||
Theorem | stirlinglem9 44076* | ((π΅βπ) β (π΅β(π + 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 44077* | 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 44078* | π΅ is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ πΎ = (π β β β¦ ((1 / ((2 Β· π) + 1)) Β· ((1 / ((2 Β· π) + 1))β(2 Β· π)))) β β’ (π β β β (π΅β(π + 1)) < (π΅βπ)) | ||
Theorem | stirlinglem12 44079* | The sequence π΅ is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) & β’ πΉ = (π β β β¦ (1 / (π Β· (π + 1)))) β β’ (π β β β ((π΅β1) β (1 / 4)) β€ (π΅βπ)) | ||
Theorem | stirlinglem13 44080* | π΅ is decreasing and has a lower bound, then it converges. Since π΅ is logπ΄, in another theorem it is proven that π΄ converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) β β’ βπ β β π΅ β π | ||
Theorem | stirlinglem14 44081* | The sequence π΄ converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for Ο& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π΅ = (π β β β¦ (logβ(π΄βπ))) β β’ βπ β β+ π΄ β π | ||
Theorem | stirlinglem15 44082* | The Stirling's formula is proven using a number of local definitions. The main theorem stirling 44083 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ π = (π β β0 β¦ ((ββ((2 Β· Ο) Β· π)) Β· ((π / e)βπ))) & β’ π΄ = (π β β β¦ ((!βπ) / ((ββ(2 Β· π)) Β· ((π / e)βπ)))) & β’ π· = (π β β β¦ (π΄β(2 Β· π))) & β’ πΈ = (π β β β¦ ((ββ(2 Β· π)) Β· ((π / e)βπ))) & β’ π = (π β β β¦ ((((2β(4 Β· π)) Β· ((!βπ)β4)) / ((!β(2 Β· π))β2)) / ((2 Β· π) + 1))) & β’ πΉ = (π β β β¦ (((π΄βπ)β4) / ((π·βπ)β2))) & β’ π» = (π β β β¦ ((πβ2) / (π Β· ((2 Β· π) + 1)))) & β’ (π β πΆ β β+) & β’ (π β π΄ β πΆ) β β’ (π β (π β β β¦ ((!βπ) / (πβπ))) β 1) | ||
Theorem | stirling 44083 | Stirling's approximation formula for π factorial. The proof follows two major steps: first it is proven that π and π factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for Ο it is proven that the unknown constant is the square root of Ο and then the exact Stirling's formula is established. This is Metamath 100 proof #90. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (π β β0 β¦ ((ββ((2 Β· Ο) Β· π)) Β· ((π / e)βπ))) β β’ (π β β β¦ ((!βπ) / (πβπ))) β 1 | ||
Theorem | stirlingr 44084 | Stirling's approximation formula for π factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 44083 is proven for convergence in the topology of complex numbers. The variable π is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (π β β0 β¦ ((ββ((2 Β· Ο) Β· π)) Β· ((π / e)βπ))) & β’ π = (βπ‘β(topGenβran (,))) β β’ (π β β β¦ ((!βπ) / (πβπ)))π 1 | ||
Theorem | dirkerval 44085* | The Nth Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) β β’ (π β β β (π·βπ) = (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) | ||
Theorem | dirker2re 44086 | The Dirichlet Kernel value is a real if the argument is not a multiple of Ο . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (((π β β β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0) β ((sinβ((π + (1 / 2)) Β· π)) / ((2 Β· Ο) Β· (sinβ(π / 2)))) β β) | ||
Theorem | dirkerdenne0 44087 | The Dirichlet Kernel denominator is never 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π β β β§ Β¬ (π mod (2 Β· Ο)) = 0) β ((2 Β· Ο) Β· (sinβ(π / 2))) β 0) | ||
Theorem | dirkerval2 44088* | The Nth Dirichlet Kernel evaluated at a specific point π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) β β’ ((π β β β§ π β β) β ((π·βπ)βπ) = if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π)) / ((2 Β· Ο) Β· (sinβ(π / 2)))))) | ||
Theorem | dirkerre 44089* | The Dirichlet Kernel at any point evaluates to a real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) β β’ ((π β β β§ π β β) β ((π·βπ)βπ) β β) | ||
Theorem | dirkerper 44090* | the Dirichlet Kernel has period 2Ο. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ π = (2 Β· Ο) β β’ ((π β β β§ π₯ β β) β ((π·βπ)β(π₯ + π)) = ((π·βπ)βπ₯)) | ||
Theorem | dirkerf 44091* | For any natural number π, the Dirichlet Kernel (π·βπ) is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) β β’ (π β β β (π·βπ):ββΆβ) | ||
Theorem | dirkertrigeqlem1 44092* | Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (πΎ β β β Ξ£π β (1...(2 Β· πΎ))(cosβ(π Β· Ο)) = 0) | ||
Theorem | dirkertrigeqlem2 44093* | Trigonomic equality lemma for the Dirichlet Kernel trigonomic equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β (sinβπ΄) β 0) & β’ (π β π β β) β β’ (π β (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π΄))) / Ο) = ((sinβ((π + (1 / 2)) Β· π΄)) / ((2 Β· Ο) Β· (sinβ(π΄ / 2))))) | ||
Theorem | dirkertrigeqlem3 44094* | Trigonometric equality lemma for the Dirichlet Kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of Ο. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β πΎ β β€) & β’ π΄ = (((2 Β· πΎ) + 1) Β· Ο) β β’ (π β (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π΄))) / Ο) = ((sinβ((π + (1 / 2)) Β· π΄)) / ((2 Β· Ο) Β· (sinβ(π΄ / 2))))) | ||
Theorem | dirkertrigeq 44095* | Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β· (sinβ(π / 2))))))) & β’ (π β π β β) & β’ πΉ = (π·βπ) & β’ π» = (π β β β¦ (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) β β’ (π β πΉ = π») | ||
Theorem | dirkeritg 44096* | The definite integral of the Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π₯ β β β¦ if((π₯ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π₯)) / ((2 Β· Ο) Β· (sinβ(π₯ / 2))))))) & β’ (π β π β β) & β’ πΉ = (π·βπ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ (((π₯ / 2) + Ξ£π β (1...π)((sinβ(π Β· π₯)) / π)) / Ο)) β β’ (π β β«(π΄(,)π΅)(πΉβπ₯) dπ₯ = ((πΊβπ΅) β (πΊβπ΄))) | ||
Theorem | dirkercncflem1 44097* | If π is a multiple of Ο then it belongs to an open inerval (π΄(,)π΅) such that for any other point π¦ in the interval, cos y/2 and sin y/2 are nonzero. Such an interval is needed to apply De L'Hopital theorem. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π΄ = (π β Ο) & β’ π΅ = (π + Ο) & β’ (π β π β β) & β’ (π β (π mod (2 Β· Ο)) = 0) β β’ (π β (π β (π΄(,)π΅) β§ βπ¦ β ((π΄(,)π΅) β {π})((sinβ(π¦ / 2)) β 0 β§ (cosβ(π¦ / 2)) β 0))) | ||
Theorem | dirkercncflem2 44098* | Lemma used to prove that the Dirichlet Kernel is continuous at π points that are multiples of (2 Β· Ο). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ πΉ = (π¦ β ((π΄(,)π΅) β {π}) β¦ (sinβ((π + (1 / 2)) Β· π¦))) & β’ πΊ = (π¦ β ((π΄(,)π΅) β {π}) β¦ ((2 Β· Ο) Β· (sinβ(π¦ / 2)))) & β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (sinβ(π¦ / 2)) β 0) & β’ π» = (π¦ β ((π΄(,)π΅) β {π}) β¦ ((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π¦)))) & β’ πΌ = (π¦ β ((π΄(,)π΅) β {π}) β¦ (Ο Β· (cosβ(π¦ / 2)))) & β’ πΏ = (π€ β (π΄(,)π΅) β¦ (((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π€))) / (Ο Β· (cosβ(π€ / 2))))) & β’ (π β π β β) & β’ (π β π β (π΄(,)π΅)) & β’ (π β (π mod (2 Β· Ο)) = 0) & β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (cosβ(π¦ / 2)) β 0) β β’ (π β ((π·βπ)βπ) β (((π·βπ) βΎ ((π΄(,)π΅) β {π})) limβ π)) | ||
Theorem | dirkercncflem3 44099* | The Dirichlet Kernel is continuous at π points that are multiples of (2 Β· Ο). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ π΄ = (π β Ο) & β’ π΅ = (π + Ο) & β’ πΉ = (π¦ β (π΄(,)π΅) β¦ ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))) & β’ πΊ = (π¦ β (π΄(,)π΅) β¦ ((2 Β· Ο) Β· (sinβ(π¦ / 2)))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π mod (2 Β· Ο)) = 0) β β’ (π β ((π·βπ)βπ) β ((π·βπ) limβ π)) | ||
Theorem | dirkercncflem4 44100* | The Dirichlet Kernel is continuos at points that are not multiple of 2 Ο . This is the easier condition, for the proof of the continuity of the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β· (sinβ(π¦ / 2))))))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π mod (2 Β· Ο)) β 0) & β’ π΄ = (ββ(π / (2 Β· Ο))) & β’ π΅ = (π΄ + 1) & β’ πΆ = (π΄ Β· (2 Β· Ο)) & β’ πΈ = (π΅ Β· (2 Β· Ο)) β β’ (π β (π·βπ) β (((topGenβran (,)) CnP (topGenβran (,)))βπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |