Home Metamath Proof ExplorerTheorem 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)

Theorem List for Metamath Proof Explorer - 37801-37900   *Has distinct variable group(s)
TypeLabelDescription
Statement

21.30.12  Stone Weierstrass theorem - real version

Theoremstoweidlem1 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.)

Theoremstoweidlem2 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.)

Theoremstoweidlem3 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.)

Theoremstoweidlem4 37804* Lemma for stoweid 37865: a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Theoremstoweidlem5 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.)

Theoremstoweidlem6 37806* Lemma for stoweid 37865: two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Theoremstoweidlem7 37807* 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.)

Theoremstoweidlem8 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.)

Theoremstoweidlem9 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.)

Theoremstoweidlem10 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.)

Theoremstoweidlem11 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.)

Theoremstoweidlem12 37812* Lemma for stoweid 37865. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Theoremstoweidlem13 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.)

Theoremstoweidlem14 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.)

Theoremstoweidlem15 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.)

Theoremstoweidlem16 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.)

Theoremstoweidlem17 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.)

Theoremstoweidlem18 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.)

Theoremstoweidlem19 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.)

Theoremstoweidlem20 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.)

Theoremstoweidlem21 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.)

Theoremstoweidlem22 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.)

Theoremstoweidlem23 37823* 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.)

Theoremstoweidlem24 37824* 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.)

Theoremstoweidlem25 37825* 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.)

Theoremstoweidlem26 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.)

Theoremstoweidlem27 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.)

Theoremstoweidlem28 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.)

Theoremstoweidlem29 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

Theoremstoweidlem29OLD 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.)

Theoremstoweidlem30 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 t0, P is used for p, is used for p(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Theoremstoweidlem31 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 ≤ 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.)

Theoremstoweidlem32 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.)

Theoremstoweidlem33 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.)

Theoremstoweidlem34 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.)

Theoremstoweidlem35 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.)

Theoremstoweidlem36 37837* 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.)

Theoremstoweidlem37 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 t0, P is used for p, is used for p(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Theoremstoweidlem38 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 t0, P is used for p, is used for p(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Theoremstoweidlem39 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 ≤ 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.)

Theoremstoweidlem40 37841* 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.)

Theoremstoweidlem41 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 - qn";. Here is used to represent ε in the paper, and to represent qn in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Theoremstoweidlem42 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.)

Theoremstoweidlem43 37844* 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.)

Theoremstoweidlem44 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 t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Theoremstoweidlem45 37846* 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.)

Theoremstoweidlem46 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.)

Theoremstoweidlem47 37848* Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Theoremstoweidlem48 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.)

Theoremstoweidlem49 37850* 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.)

Theoremstoweidlem50 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.)

Theoremstoweidlem51 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.)

Theoremstoweidlem52 37853* There exists a neighborood 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.)

Theoremstoweidlem53 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.)

Theoremstoweidlem54 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.)

Theoremstoweidlem55 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 t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Theoremstoweidlem56 37857* 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.)

Theoremstoweidlem57 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.)

Theoremstoweidlem58 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.)

Theoremstoweidlem59 37860* 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 - \epslon / 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.)

Theoremstoweidlem60 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.)

Theoremstoweidlem61 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.)

Theoremstoweidlem62 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

Theoremstoweidlem62OLD 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.)

Theoremstoweid 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.)

Theoremstowei 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.)

21.30.13  Wallis' product for π

Theoremwallispilem1 37867* is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Theoremwallispilem2 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.)

Theoremwallispilem3 37869* I maps to real values (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Theoremwallispilem4 37870* maps to explicit expression for the ratio of two consecutive values of . (Contributed by Glauco Siliprandi, 30-Jun-2017.)

Theoremwallispilem5 37871* The sequence converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.)

Theoremwallispi 37872* Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Theoremwallispi2lem1 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.)

Theoremwallispi2lem2 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.)

Theoremwallispi2 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.)

21.30.14  Stirling's approximation formula for ` n ` factorial

Theoremstirlinglem1 37876 A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.)

Theoremstirlinglem2 37877 maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)