Home | Metamath
Proof Explorer Theorem List (p. 379 of 402) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-26569) |
Hilbert Space Explorer
(26570-28092) |
Users' Mathboxes
(28093-40162) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | stoweidlem1 37801 | Lemma for stoweid 37865. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 12404. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem2 37802* | lemma for stoweid 37865: 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 37803* | Lemma for stoweid 37865: if is positive and all terms of a finite product are larger than , then the finite product is larger than A^M. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem4 37804* | Lemma for stoweid 37865: a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem5 37805* | 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.) |
Theorem | stoweidlem6 37806* | Lemma for stoweid 37865: two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem7 37807* | This lemma is used to prove that q_{n} as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91, (at the top of page 91), is such that q_{n} < ε on , and q_{n} > 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.) |
Theorem | stoweidlem8 37808* | Lemma for stoweid 37865: two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem9 37809* | Lemma for stoweid 37865: here the Stone Weierstrass theorem is proven for the trivial case, T is the empty set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem10 37810 | Lemma for stoweid 37865. 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.) |
Theorem | stoweidlem11 37811* | 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.) |
Theorem | stoweidlem12 37812* | Lemma for stoweid 37865. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem13 37813 | Lemma for stoweid 37865. 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.) |
Theorem | stoweidlem14 37814* | 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.) |
Theorem | stoweidlem15 37815* | 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_{(t}_0) = 0, and p > 0 on T - U. Here is used to represent p_{(t}_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem16 37816* | Lemma for stoweid 37865. The subset of functions in the algebra , with values in [ 0 , 1 ], is closed under multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem17 37817* | 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.) |
Theorem | stoweidlem18 37818* | 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.) |
Theorem | stoweidlem19 37819* | 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.) |
Theorem | stoweidlem20 37820* | 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.) |
Theorem | stoweidlem21 37821* | 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.) |
Theorem | stoweidlem22 37822* | 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 | stoweidlem23 37823* | This lemma is used to prove the existence of a function p_{t} 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 p_{t} ( t_{0} ) = 0 , p_{t} ( t ) > 0, and 0 <= p_{t} <= 1. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem24 37824* | This lemma proves that for sufficiently large, q_{n}( t ) > ( 1 - epsilon ), for all in : see Lemma 1 [BrosowskiDeutsh] p. 90, (at the bottom of page 90). is used to represent q_{n} in the paper, to represent in the paper, to represent , to represent δ, and to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem25 37825* | This lemma proves that for n sufficiently large, q_{n}( t ) < ε, for all in : see Lemma 1 [BrosowskiDeutsh] p. 91 (at the top of page 91). is used to represent q_{n} 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.) |
Theorem | stoweidlem26 37826* | 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.) |
Theorem | stoweidlem27 37827* | 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_{(t}_0) = 0, and p > 0 on T - U. Here is used to represent p_{(t}_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem28 37828* | 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.) |
Theorem | stoweidlem29 37829* | 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.) |
inf inf inf | ||
Theorem | stoweidlem29OLD 37830* | 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.) Obsolete version of stoweidlem29 37829 as of 13-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | stoweidlem30 37831* | 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_{(t}_0) = 0, and p > 0 on T - U. Z is used for t_{0}, P is used for p, is used for p_{(t}_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem31 37832* | 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 ≤ x_{i} ≤ 1, x_{i} < ε / m on V(t_{i}), and x_{i} > 1 - ε / m on . Here M is used to represent m in the paper, is used to represent ε in the paper, v_{i} is used to represent V(t_{i}). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem32 37833* | 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.) |
Theorem | stoweidlem33 37834* | 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 37835* | 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.) |
Theorem | stoweidlem35 37836* | 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_{(t}_0) = 0, and p > 0 on T - U. Here is used to represent p_{(t}_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem36 37837* | This lemma is used to prove the existence of a function p_{t} 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 p_{t} ( t_{0} ) = 0 , p_{t} ( t ) > 0, and 0 <= p_{t} <= 1. Z is used for t_{0} , S is used for t e. T - U , h is used for p_{t} . G is used for (h_{t})^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.) |
Theorem | stoweidlem37 37838* | 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_{(t}_0) = 0, and p > 0 on T - U. Z is used for t_{0}, P is used for p, is used for p_{(t}_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem38 37839* | 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_{(t}_0) = 0, and p > 0 on T - U. Z is used for t_{0}, P is used for p, is used for p_{(t}_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem39 37840* | 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 ≤ x_{i} ≤ 1, x_{i} < ε / m on V(t_{i}), and x_{i} > 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 v_{i} is used to represent V(t_{i}). is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem40 37841* | This lemma proves that q_{n} is in the subalgebra, as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90. Q is used to represent q_{n} 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.) |
Theorem | stoweidlem41 37842* | 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 - q_{n"};. Here is used to represent ε in the paper, and to represent q_{n} in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem42 37843* | 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.) |
Theorem | stoweidlem43 37844* | This lemma is used to prove the existence of a function p_{t} 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_{t} in the subalgebra, such that p_{t}( t_{0} ) = 0 , p_{t} ( t ) > 0, and 0 <= p_{t} <= 1. Hera Z is used for t_{0} , S is used for t e. T - U , h is used for p_{t}. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem44 37845* | 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_{(t}_0) = 0, and p > 0 on T - U. Z is used to represent t_{0} in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem45 37846* | This lemma proves that, given an appropriate (in another theorem we prove such a exists), there exists a function q_{n} as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 ( at the top of page 91): 0 <= q_{n} <= 1 , q_{n} < ε on T \ U, and q_{n} > 1 - ε on . We use y to represent the final q_{n} 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.) |
Theorem | stoweidlem46 37847* | 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.) |
Theorem | stoweidlem47 37848* | Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem48 37849* | 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.) |
Theorem | stoweidlem49 37850* | There exists a function q_{n} as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 (at the top of page 91): 0 <= q_{n} <= 1 , q_{n} < ε on , and q_{n} > 1 - ε on . Here y is used to represent the final q_{n} 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.) |
Theorem | stoweidlem50 37851* | 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.) |
Theorem | stoweidlem51 37852* | 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.) |
Theorem | stoweidlem52 37853* | There exists a neighborood V as in Lemma 1 of [BrosowskiDeutsh] p. 90. Here Z is used to represent t_{0} in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem53 37854* | 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_{(t}_0) = 0, and p > 0 on T - U. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem54 37855* | 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.) |
Theorem | stoweidlem55 37856* | 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_{(t}_0) = 0, and p > 0 on T - U. Here Z is used to represent t_{0} in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem56 37857* | This theorem proves Lemma 1 in [BrosowskiDeutsh] p. 90. Here is used to represent t_{0} in the paper, is used to represent in the paper, and is used to represent ε (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem57 37858* | 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.) |
Theorem | stoweidlem58 37859* | 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.) |
Theorem | stoweidlem59 37860* | This lemma proves that there exists a function as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: x_{j} is in the subalgebra, 0 <= x_{j} <= 1, x_{j} < ε / n on A_{j} (meaning A in the paper), x_{j} > 1 - \epslon / n on B_{j}. 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.) |
Theorem | stoweidlem60 37861* | 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.) |
Theorem | stoweidlem61 37862* | 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.) |
Theorem | stoweidlem62 37863* | 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 | ||
Theorem | stoweidlem62OLD 37864* | 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.) Obsolete version of stoweidlem62 37863 as of 13-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | stoweid 37865* | 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.) |
Theorem | stowei 37866* | 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 37865: often times it will be better to use stoweid 37865 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | wallispilem1 37867* | is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | wallispilem2 37868* | 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.) |
Theorem | wallispilem3 37869* | I maps to real values (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | wallispilem4 37870* | maps to explicit expression for the ratio of two consecutive values of . (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | wallispilem5 37871* | The sequence converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | wallispi 37872* | Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | wallispi2lem1 37873 | 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.) |
Theorem | wallispi2lem2 37874 | 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.) |
Theorem | wallispi2 37875 | An alternative version of Wallis' formula for π ; this second formula uses factorials and it is later used to proof Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem1 37876 | A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | stirlinglem2 37877 | maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |