Home | Metamath
Proof Explorer Theorem List (p. 242 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | aaliou3lem4 24101* | Lemma for aaliou3 24106. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
Theorem | aaliou3lem5 24102* | Lemma for aaliou3 24106. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
Theorem | aaliou3lem6 24103* | Lemma for aaliou3 24106. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
Theorem | aaliou3lem7 24104* | Lemma for aaliou3 24106. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
Theorem | aaliou3lem9 24105* | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
Theorem | aaliou3 24106 | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 23-Nov-2014.) |
Syntax | ctayl 24107 | Taylor polynomial of a function. |
Tayl | ||
Syntax | cana 24108 | The class of analytic functions. |
Ana | ||
Definition | df-tayl 24109* | Define the Taylor polynomial or Taylor series of a function. TODO-AV: can/should be replaced by NN0*. (Contributed by Mario Carneiro, 30-Dec-2016.) |
Tayl ℂfld tsums | ||
Definition | df-ana 24110* | Define the set of analytic functions, which are functions such that the Taylor series of the function at each point converges to the function in some neighborhood of the point. (Contributed by Mario Carneiro, 31-Dec-2016.) |
Ana ℂfld ↾t Tayl | ||
Theorem | taylfvallem1 24111* | Lemma for taylfval 24113. (Contributed by Mario Carneiro, 30-Dec-2016.) |
Theorem | taylfvallem 24112* | Lemma for taylfval 24113. (Contributed by Mario Carneiro, 30-Dec-2016.) |
ℂfld tsums | ||
Theorem | taylfval 24113* |
Define the Taylor polynomial of a function. The constant Tayl is a
function of five arguments: is the base set with respect to
evaluate the derivatives (generally or ), is
the
function we are approximating, at point , to order . The
result is a polynomial function of .
This "extended" version of taylpfval 24119 additionally handles the case , in which case this is not a polynomial but an infinite series, the Taylor series of the function. (Contributed by Mario Carneiro, 30-Dec-2016.) |
Tayl ℂfld tsums | ||
Theorem | eltayl 24114* | Value of the Taylor series as a relation (elementhood in the domain here expresses that the series is convergent). (Contributed by Mario Carneiro, 30-Dec-2016.) |
Tayl ℂfld tsums | ||
Theorem | taylf 24115* | The Taylor series defines a function on a subset of the complex numbers. (Contributed by Mario Carneiro, 30-Dec-2016.) |
Tayl | ||
Theorem | tayl0 24116* | The Taylor series is always defined at the basepoint, with value equal to the value of the function. (Contributed by Mario Carneiro, 30-Dec-2016.) |
Tayl | ||
Theorem | taylplem1 24117* | Lemma for taylpfval 24119 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.) |
Theorem | taylplem2 24118* | Lemma for taylpfval 24119 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.) |
Theorem | taylpfval 24119* | Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: is the base set with respect to evaluate the derivatives (generally or ), is the function we are approximating, at point , to order . The result is a polynomial function of . (Contributed by Mario Carneiro, 31-Dec-2016.) |
Tayl | ||
Theorem | taylpf 24120 | The Taylor polynomial is a function on the complex numbers (even if the base set of the original function is the reals). (Contributed by Mario Carneiro, 31-Dec-2016.) |
Tayl | ||
Theorem | taylpval 24121* | Value of the Taylor polynomial. (Contributed by Mario Carneiro, 31-Dec-2016.) |
Tayl | ||
Theorem | taylply2 24122* | The Taylor polynomial is a polynomial of degree (at most) . This version of taylply 24123 shows that the coefficients of are in a subring of the complex numbers. (Contributed by Mario Carneiro, 1-Jan-2017.) |
Tayl SubRingℂfld Poly deg | ||
Theorem | taylply 24123 | The Taylor polynomial is a polynomial of degree (at most) . (Contributed by Mario Carneiro, 31-Dec-2016.) |
Tayl Poly deg | ||
Theorem | dvtaylp 24124 | The derivative of the Taylor polynomial is the Taylor polynomial of the derivative of the function. (Contributed by Mario Carneiro, 31-Dec-2016.) |
Tayl Tayl | ||
Theorem | dvntaylp 24125 | The -th derivative of the Taylor polynomial is the Taylor polynomial of the -th derivative of the function. (Contributed by Mario Carneiro, 1-Jan-2017.) |
Tayl Tayl | ||
Theorem | dvntaylp0 24126 | The first derivatives of the Taylor polynomial at match the derivatives of the function from which it is derived. (Contributed by Mario Carneiro, 1-Jan-2017.) |
Tayl | ||
Theorem | taylthlem1 24127* | Lemma for taylth 24129. This is the main part of Taylor's theorem, except for the induction step, which is supposed to be proven using L'Hôpital's rule. However, since our proof of L'Hôpital assumes that , we can only do this part generically, and for taylth 24129 itself we must restrict to . (Contributed by Mario Carneiro, 1-Jan-2017.) |
Tayl ..^ lim lim lim | ||
Theorem | taylthlem2 24128* | Lemma for taylth 24129. (Contributed by Mario Carneiro, 1-Jan-2017.) |
Tayl ..^ lim lim | ||
Theorem | taylth 24129* | Taylor's theorem. The Taylor polynomial of a -times differentiable function is such that the error term goes to zero faster than . This is Metamath 100 proof #35. (Contributed by Mario Carneiro, 1-Jan-2017.) |
Tayl lim | ||
Syntax | culm 24130 | Extend class notation to include the uniform convergence predicate. |
Definition | df-ulm 24131* | Define the uniform convergence of a sequence of functions. Here if is a sequence of functions defined on and is a function on , and for every there is a such that the functions for are all uniformly within of on the domain . Compare with df-clim 14219. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | ulmrel 24132 | The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | ulmscl 24133 | Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | ulmval 24134* | Express the predicate: The sequence of functions converges uniformly to on . (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | ulmcl 24135 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | ulmf 24136* | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | ulmpm 24137 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | ulmf2 24138 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 18-Mar-2015.) |
Theorem | ulm2 24139* | Simplify ulmval 24134 when and are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | ulmi 24140* | The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.) |
Theorem | ulmclm 24141* | A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.) |
Theorem | ulmres 24142 | A sequence of functions converges iff the tail of the sequence converges (for any finite cutoff). (Contributed by Mario Carneiro, 24-Mar-2015.) |
Theorem | ulmshftlem 24143* | Lemma for ulmshft 24144. (Contributed by Mario Carneiro, 24-Mar-2015.) |
Theorem | ulmshft 24144* | A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.) |
Theorem | ulm0 24145 | Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.) |
Theorem | ulmuni 24146 | An sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.) |
Theorem | ulmdm 24147 | Two ways to express that a function has a limit. (The expression is sometimes useful as a shorthand for "the unique limit of the function "). (Contributed by Mario Carneiro, 5-Jul-2017.) |
Theorem | ulmcaulem 24148* | Lemma for ulmcau 24149 and ulmcau2 24150: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 14095. (Contributed by Mario Carneiro, 1-Mar-2015.) |
Theorem | ulmcau 24149* | A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every there is a such that for all the functions and are uniformly within of each other on . This is the four-quantifier version, see ulmcau2 24150 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.) |
Theorem | ulmcau2 24150* | A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every there is a such that for all the functions and are uniformly within of each other on . (Contributed by Mario Carneiro, 1-Mar-2015.) |
Theorem | ulmss 24151* | A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.) |
Theorem | ulmbdd 24152* | A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.) |
Theorem | ulmcn 24153 | A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.) |
Theorem | ulmdvlem1 24154* | Lemma for ulmdv 24157. (Contributed by Mario Carneiro, 3-Mar-2015.) |
Theorem | ulmdvlem2 24155* | Lemma for ulmdv 24157. (Contributed by Mario Carneiro, 8-May-2015.) |
Theorem | ulmdvlem3 24156* | Lemma for ulmdv 24157. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
Theorem | ulmdv 24157* | If is a sequence of differentiable functions on which converge pointwise to , and the derivatives of converge uniformly to , then is differentiable with derivative . (Contributed by Mario Carneiro, 27-Feb-2015.) |
Theorem | mtest 24158* | The Weierstrass M-test. If is a sequence of functions which are uniformly bounded by the convergent sequence , then the series generated by the sequence converges uniformly. (Contributed by Mario Carneiro, 3-Mar-2015.) |
Theorem | mtestbdd 24159* | Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017.) |
Theorem | mbfulm 24160 | A uniform limit of measurable functions is measurable. (This is just a corollary of the fact that a pointwise limit of measurable functions is measurable, see mbflim 23435.) (Contributed by Mario Carneiro, 18-Mar-2015.) |
MblFn MblFn | ||
Theorem | iblulm 24161 | A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.) |
Theorem | itgulm 24162* | A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.) |
Theorem | itgulm2 24163* | A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.) |
Theorem | pserval 24164* | Value of the function that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | pserval2 24165* | Value of the function that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | psergf 24166* | The sequence of terms in the infinite sequence defining a power series for fixed . (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | radcnvlem1 24167* | Lemma for radcnvlt1 24172, radcnvle 24174. If is a point closer to zero than and the power series converges at , then it converges absolutely at , even if the terms in the sequence are multiplied by . (Contributed by Mario Carneiro, 31-Mar-2015.) |
Theorem | radcnvlem2 24168* | Lemma for radcnvlt1 24172, radcnvle 24174. If is a point closer to zero than and the power series converges at , then it converges absolutely at . (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | radcnvlem3 24169* | Lemma for radcnvlt1 24172, radcnvle 24174. If is a point closer to zero than and the power series converges at , then it converges at . (Contributed by Mario Carneiro, 31-Mar-2015.) |
Theorem | radcnv0 24170* | Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | radcnvcl 24171* | The radius of convergence of an infinite series is a nonnegative extended real number. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | radcnvlt1 24172* | If is within the open disk of radius centered at zero, then the infinite series converges absolutely at , and also converges when the series is multiplied by . (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | radcnvlt2 24173* | If is within the open disk of radius centered at zero, then the infinite series converges at . (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | radcnvle 24174* | If is a convergent point of the infinite series, then is within the closed disk of radius centered at zero. Or, by contraposition, the series diverges at any point strictly more than from the origin. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | dvradcnv 24175* | The radius of convergence of the (formal) derivative of the power series is at least as large as the radius of convergence of . (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015.) |
Theorem | pserulm 24176* | If is a region contained in a circle of radius , then the sequence of partial sums of the infinite series converges uniformly on . (Contributed by Mario Carneiro, 26-Feb-2015.) |
Theorem | psercn2 24177* | Since by pserulm 24176 the series converges uniformly, it is also continuous by ulmcn 24153. (Contributed by Mario Carneiro, 3-Mar-2015.) |
Theorem | psercnlem2 24178* | Lemma for psercn 24180. (Contributed by Mario Carneiro, 18-Mar-2015.) |
Theorem | psercnlem1 24179* | Lemma for psercn 24180. (Contributed by Mario Carneiro, 18-Mar-2015.) |
Theorem | psercn 24180* | An infinite series converges to a continuous function on the open disk of radius , where is the radius of convergence of the series. (Contributed by Mario Carneiro, 4-Mar-2015.) |
Theorem | pserdvlem1 24181* | Lemma for pserdv 24183. (Contributed by Mario Carneiro, 7-May-2015.) |
Theorem | pserdvlem2 24182* | Lemma for pserdv 24183. (Contributed by Mario Carneiro, 7-May-2015.) |
Theorem | pserdv 24183* | The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.) |
Theorem | pserdv2 24184* | The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.) |
Theorem | abelthlem1 24185* | Lemma for abelth 24195. (Contributed by Mario Carneiro, 1-Apr-2015.) |
Theorem | abelthlem2 24186* | Lemma for abelth 24195. The peculiar region , known as a Stolz angle , is a teardrop-shaped subset of the closed unit ball containing . Indeed, except for itself, the rest of the Stolz angle is enclosed in the open unit ball. (Contributed by Mario Carneiro, 31-Mar-2015.) |
Theorem | abelthlem3 24187* | Lemma for abelth 24195. (Contributed by Mario Carneiro, 31-Mar-2015.) |
Theorem | abelthlem4 24188* | Lemma for abelth 24195. (Contributed by Mario Carneiro, 31-Mar-2015.) |
Theorem | abelthlem5 24189* | Lemma for abelth 24195. (Contributed by Mario Carneiro, 1-Apr-2015.) |
Theorem | abelthlem6 24190* | Lemma for abelth 24195. (Contributed by Mario Carneiro, 2-Apr-2015.) |
Theorem | abelthlem7a 24191* | Lemma for abelth 24195. (Contributed by Mario Carneiro, 8-May-2015.) |
Theorem | abelthlem7 24192* | Lemma for abelth 24195. (Contributed by Mario Carneiro, 2-Apr-2015.) |
Theorem | abelthlem8 24193* | Lemma for abelth 24195. (Contributed by Mario Carneiro, 2-Apr-2015.) |
Theorem | abelthlem9 24194* | Lemma for abelth 24195. By adjusting the constant term, we can assume that the entire series converges to . (Contributed by Mario Carneiro, 1-Apr-2015.) |
Theorem | abelth 24195* | Abel's theorem. If the power series is convergent at , then it is equal to the limit from "below", along a Stolz angle (note that the case of a Stolz angle is the real line ). (Continuity on follows more generally from psercn 24180.) (Contributed by Mario Carneiro, 2-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
Theorem | abelth2 24196* | Abel's theorem, restricted to the interval. (Contributed by Mario Carneiro, 2-Apr-2015.) |
Theorem | efcn 24197 | The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.) |
Theorem | sincn 24198 | Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
Theorem | coscn 24199 | Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
Theorem | reeff1olem 24200* | Lemma for reeff1o 24201. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |