Home | Metamath
Proof Explorer Theorem List (p. 257 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elqaalem1 25601* | Lemma for elqaa 25604. The function π represents the denominators of the rational coefficients π΅. By multiplying them all together to make π , we get a number big enough to clear all the denominators and make π Β· πΉ an integer polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ β ((Polyββ) β {0π})) & β’ (π β (πΉβπ΄) = 0) & β’ π΅ = (coeffβπΉ) & β’ π = (π β β0 β¦ inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, < )) & β’ π = (seq0( Β· , π)β(degβπΉ)) β β’ ((π β§ πΎ β β0) β ((πβπΎ) β β β§ ((π΅βπΎ) Β· (πβπΎ)) β β€)) | ||
Theorem | elqaalem2 25602* | Lemma for elqaa 25604. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ β ((Polyββ) β {0π})) & β’ (π β (πΉβπ΄) = 0) & β’ π΅ = (coeffβπΉ) & β’ π = (π β β0 β¦ inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, < )) & β’ π = (seq0( Β· , π)β(degβπΉ)) & β’ π = (π₯ β V, π¦ β V β¦ ((π₯ Β· π¦) mod (πβπΎ))) β β’ ((π β§ πΎ β (0...(degβπΉ))) β (π mod (πβπΎ)) = 0) | ||
Theorem | elqaalem3 25603* | Lemma for elqaa 25604. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ β ((Polyββ) β {0π})) & β’ (π β (πΉβπ΄) = 0) & β’ π΅ = (coeffβπΉ) & β’ π = (π β β0 β¦ inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, < )) & β’ π = (seq0( Β· , π)β(degβπΉ)) β β’ (π β π΄ β πΈ) | ||
Theorem | elqaa 25604* | The set of numbers generated by the roots of polynomials in the rational numbers is the same as the set of algebraic numbers, which by elaa 25598 are defined only in terms of polynomials over the integers. (Contributed by Mario Carneiro, 23-Jul-2014.) (Proof shortened by AV, 3-Oct-2020.) |
β’ (π΄ β πΈ β (π΄ β β β§ βπ β ((Polyββ) β {0π})(πβπ΄) = 0)) | ||
Theorem | qaa 25605 | Every rational number is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β β β π΄ β πΈ) | ||
Theorem | qssaa 25606 | The rational numbers are contained in the algebraic numbers. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ β β πΈ | ||
Theorem | iaa 25607 | The imaginary unit is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ i β πΈ | ||
Theorem | aareccl 25608 | The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π΄ β πΈ β§ π΄ β 0) β (1 / π΄) β πΈ) | ||
Theorem | aacjcl 25609 | The conjugate of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ (π΄ β πΈ β (ββπ΄) β πΈ) | ||
Theorem | aannenlem1 25610* | Lemma for aannen 25613. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ (π΄ β β0 β (π»βπ΄) β Fin) | ||
Theorem | aannenlem2 25611* | Lemma for aannen 25613. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ πΈ = βͺ ran π» | ||
Theorem | aannenlem3 25612* | The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ πΈ β β | ||
Theorem | aannen 25613 | The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΈ β β | ||
Theorem | aalioulem1 25614 | Lemma for aaliou 25620. An integer polynomial cannot inflate the denominator of a rational by more than its degree. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β€) & β’ (π β π β β) β β’ (π β ((πΉβ(π / π)) Β· (πβ(degβπΉ))) β β€) | ||
Theorem | aalioulem2 25615* | Lemma for aaliou 25620. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Proof shortened by AV, 28-Sep-2020.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem3 25616* | Lemma for aaliou 25620. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β ((absβ(π΄ β π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π)))) | ||
Theorem | aalioulem4 25617* | Lemma for aaliou 25620. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β (((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem5 25618* | Lemma for aaliou 25620. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem6 25619* | Lemma for aaliou 25620. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou 25620* | Liouville's theorem on diophantine approximation: Any algebraic number, being a root of a polynomial πΉ in integer coefficients, is not approximable beyond order π = deg(πΉ) by rational numbers. In this form, it also applies to rational numbers themselves, which are not well approximable by other rational numbers. This is Metamath 100 proof #18. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) < (absβ(π΄ β (π / π))))) | ||
Theorem | geolim3 25621* | Geometric series convergence with arbitrary shift, radix, and multiplicative constant. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < 1) & β’ (π β πΆ β β) & β’ πΉ = (π β (β€β₯βπ΄) β¦ (πΆ Β· (π΅β(π β π΄)))) β β’ (π β seqπ΄( + , πΉ) β (πΆ / (1 β π΅))) | ||
Theorem | aaliou2 25622* | Liouville's approximation theorem for algebraic numbers per se. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (π΄ β (πΈ β© β) β βπ β β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) < (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou2b 25623* | Liouville's approximation theorem extended to complex π΄. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ (π΄ β πΈ β βπ β β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) < (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou3lem1 25624* | Lemma for aaliou3 25633. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) β β’ ((π΄ β β β§ π΅ β (β€β₯βπ΄)) β (πΊβπ΅) β β) | ||
Theorem | aaliou3lem2 25625* | Lemma for aaliou3 25633. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) & β’ πΉ = (π β β β¦ (2β-(!βπ))) β β’ ((π΄ β β β§ π΅ β (β€β₯βπ΄)) β (πΉβπ΅) β (0(,](πΊβπ΅))) | ||
Theorem | aaliou3lem3 25626* | Lemma for aaliou3 25633. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) & β’ πΉ = (π β β β¦ (2β-(!βπ))) β β’ (π΄ β β β (seqπ΄( + , πΉ) β dom β β§ Ξ£π β (β€β₯βπ΄)(πΉβπ) β β+ β§ Ξ£π β (β€β₯βπ΄)(πΉβπ) β€ (2 Β· (2β-(!βπ΄))))) | ||
Theorem | aaliou3lem8 25627* | Lemma for aaliou3 25633. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ ((π΄ β β β§ π΅ β β+) β βπ₯ β β (2 Β· (2β-(!β(π₯ + 1)))) β€ (π΅ / ((2β(!βπ₯))βπ΄))) | ||
Theorem | aaliou3lem4 25628* | Lemma for aaliou3 25633. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ πΏ β β | ||
Theorem | aaliou3lem5 25629* | Lemma for aaliou3 25633. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β (π»βπ΄) β β) | ||
Theorem | aaliou3lem6 25630* | Lemma for aaliou3 25633. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β ((π»βπ΄) Β· (2β(!βπ΄))) β β€) | ||
Theorem | aaliou3lem7 25631* | Lemma for aaliou3 25633. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β ((π»βπ΄) β πΏ β§ (absβ(πΏ β (π»βπ΄))) β€ (2 Β· (2β-(!β(π΄ + 1)))))) | ||
Theorem | aaliou3lem9 25632* | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ Β¬ πΏ β πΈ | ||
Theorem | aaliou3 25633 | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 23-Nov-2014.) |
β’ Ξ£π β β (2β-(!βπ)) β πΈ | ||
Syntax | ctayl 25634 | Taylor polynomial of a function. |
class Tayl | ||
Syntax | cana 25635 | The class of analytic functions. |
class Ana | ||
Definition | df-tayl 25636* | Define the Taylor polynomial or Taylor series of a function. TODO-AV: π β (β0 βͺ {+β}) should be replaced by π β β0*. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ Tayl = (π β {β, β}, π β (β βpm π ) β¦ (π β (β0 βͺ {+β}), π β β© π β ((0[,]π) β© β€)dom ((π Dπ π)βπ) β¦ βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ π)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))))))) | ||
Definition | df-ana 25637* | 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 = (π β {β, β} β¦ {π β (β βpm π ) β£ βπ₯ β dom π π₯ β ((intβ((TopOpenββfld) βΎt π ))βdom (π β© (+β(π Tayl π)π₯)))}) | ||
Theorem | taylfvallem1 25638* | Lemma for taylfval 25640. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) β β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ)) β β) | ||
Theorem | taylfvallem 25639* | Lemma for taylfval 25640. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) β β’ ((π β§ π β β) β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ)))) β β) | ||
Theorem | taylfval 25640* |
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 25646 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.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β π = βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) | ||
Theorem | eltayl 25641* | 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.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β (πππ β (π β β β§ π β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ))))))) | ||
Theorem | taylf 25642* | The Taylor series defines a function on a subset of the complex numbers. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β π:dom πβΆβ) | ||
Theorem | tayl0 25643* | 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.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β (π΅ β dom π β§ (πβπ΅) = (πΉβπ΅))) | ||
Theorem | taylplem1 25644* | Lemma for taylpfval 25646 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) β β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) | ||
Theorem | taylplem2 25645* | Lemma for taylpfval 25646 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) β β’ (((π β§ π β β) β§ π β (0...π)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ)) β β) | ||
Theorem | taylpfval 25646* | 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.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β π = (π₯ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) | ||
Theorem | taylpf 25647 | 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.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β π:ββΆβ) | ||
Theorem | taylpval 25648* | Value of the Taylor polynomial. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) & β’ (π β π β β) β β’ (π β (πβπ) = Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ))) | ||
Theorem | taylply2 25649* | The Taylor polynomial is a polynomial of degree (at most) π. This version of taylply 25650 shows that the coefficients of π are in a subring of the complex numbers. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) & β’ (π β π· β (SubRingββfld)) & β’ (π β π΅ β π·) & β’ ((π β§ π β (0...π)) β ((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) β π·) β β’ (π β (π β (Polyβπ·) β§ (degβπ) β€ π)) | ||
Theorem | taylply 25650 | The Taylor polynomial is a polynomial of degree (at most) π. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β (π β (Polyββ) β§ (degβπ) β€ π)) | ||
Theorem | dvtaylp 25651 | The derivative of the Taylor polynomial is the Taylor polynomial of the derivative of the function. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)β(π + 1))) β β’ (π β (β D ((π + 1)(π Tayl πΉ)π΅)) = (π(π Tayl (π D πΉ))π΅)) | ||
Theorem | dvntaylp 25652 | 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.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)β(π + π))) β β’ (π β ((β Dπ ((π + π)(π Tayl πΉ)π΅))βπ) = (π(π Tayl ((π Dπ πΉ)βπ))π΅)) | ||
Theorem | dvntaylp0 25653 | 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.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β (0...π)) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β (((β Dπ π)βπ)βπ΅) = (((π Dπ πΉ)βπ)βπ΅)) | ||
Theorem | taylthlem1 25654* | Lemma for taylth 25656. 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 25656 itself we must restrict to β. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β dom ((π Dπ πΉ)βπ) = π΄) & β’ (π β π β β) & β’ (π β π΅ β π΄) & β’ π = (π(π Tayl πΉ)π΅) & β’ π = (π₯ β (π΄ β {π΅}) β¦ (((πΉβπ₯) β (πβπ₯)) / ((π₯ β π΅)βπ))) & β’ ((π β§ (π β (1..^π) β§ 0 β ((π¦ β (π΄ β {π΅}) β¦ (((((π Dπ πΉ)β(π β π))βπ¦) β (((β Dπ π)β(π β π))βπ¦)) / ((π¦ β π΅)βπ))) limβ π΅))) β 0 β ((π₯ β (π΄ β {π΅}) β¦ (((((π Dπ πΉ)β(π β (π + 1)))βπ₯) β (((β Dπ π)β(π β (π + 1)))βπ₯)) / ((π₯ β π΅)β(π + 1)))) limβ π΅)) β β’ (π β 0 β (π limβ π΅)) | ||
Theorem | taylthlem2 25655* | Lemma for taylth 25656. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β dom ((β Dπ πΉ)βπ) = π΄) & β’ (π β π β β) & β’ (π β π΅ β π΄) & β’ π = (π(β Tayl πΉ)π΅) & β’ (π β π β (1..^π)) & β’ (π β 0 β ((π₯ β (π΄ β {π΅}) β¦ (((((β Dπ πΉ)β(π β π))βπ₯) β (((β Dπ π)β(π β π))βπ₯)) / ((π₯ β π΅)βπ))) limβ π΅)) β β’ (π β 0 β ((π₯ β (π΄ β {π΅}) β¦ (((((β Dπ πΉ)β(π β (π + 1)))βπ₯) β (((β Dπ π)β(π β (π + 1)))βπ₯)) / ((π₯ β π΅)β(π + 1)))) limβ π΅)) | ||
Theorem | taylth 25656* | 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.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β dom ((β Dπ πΉ)βπ) = π΄) & β’ (π β π β β) & β’ (π β π΅ β π΄) & β’ π = (π(β Tayl πΉ)π΅) & β’ π = (π₯ β (π΄ β {π΅}) β¦ (((πΉβπ₯) β (πβπ₯)) / ((π₯ β π΅)βπ))) β β’ (π β 0 β (π limβ π΅)) | ||
Syntax | culm 25657 | Extend class notation to include the uniform convergence predicate. |
class βπ’ | ||
Definition | df-ulm 25658* | 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 0 < π₯ there is a π such that the functions πΉ(π) for π β€ π are all uniformly within π₯ of πΊ on the domain π. Compare with df-clim 15305. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ βπ’ = (π β V β¦ {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β βm π ) β§ π¦:π βΆβ β§ βπ₯ β β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)}) | ||
Theorem | ulmrel 25659 | The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ Rel (βπ’βπ) | ||
Theorem | ulmscl 25660 | Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β π β V) | ||
Theorem | ulmval 25661* | Express the predicate: The sequence of functions πΉ converges uniformly to πΊ on π. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (π β π β (πΉ(βπ’βπ)πΊ β βπ β β€ (πΉ:(β€β₯βπ)βΆ(β βm π) β§ πΊ:πβΆβ β§ βπ₯ β β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) | ||
Theorem | ulmcl 25662 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) | ||
Theorem | ulmf 25663* | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β βπ β β€ πΉ:(β€β₯βπ)βΆ(β βm π)) | ||
Theorem | ulmpm 25664 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β πΉ β ((β βm π) βpm β€)) | ||
Theorem | ulmf2 25665 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ ((πΉ Fn π β§ πΉ(βπ’βπ)πΊ) β πΉ:πβΆ(β βm π)) | ||
Theorem | ulm2 25666* | Simplify ulmval 25661 when πΉ and πΊ are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ ((π β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = π΅) & β’ ((π β§ π§ β π) β (πΊβπ§) = π΄) & β’ (π β πΊ:πβΆβ) & β’ (π β π β π) β β’ (π β (πΉ(βπ’βπ)πΊ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) | ||
Theorem | ulmi 25667* | The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ ((π β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = π΅) & β’ ((π β§ π§ β π) β (πΊβπ§) = π΄) & β’ (π β πΉ(βπ’βπ)πΊ) & β’ (π β πΆ β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < πΆ) | ||
Theorem | ulmclm 25668* | A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π΄ β π) & β’ (π β π» β π) & β’ ((π β§ π β π) β ((πΉβπ)βπ΄) = (π»βπ)) & β’ (π β πΉ(βπ’βπ)πΊ) β β’ (π β π» β (πΊβπ΄)) | ||
Theorem | ulmres 25669 | A sequence of functions converges iff the tail of the sequence converges (for any finite cutoff). (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) β β’ (π β (πΉ(βπ’βπ)πΊ β (πΉ βΎ π)(βπ’βπ)πΊ)) | ||
Theorem | ulmshftlem 25670* | Lemma for ulmshft 25671. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯β(π + πΎ)) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π» = (π β π β¦ (πΉβ(π β πΎ)))) β β’ (π β (πΉ(βπ’βπ)πΊ β π»(βπ’βπ)πΊ)) | ||
Theorem | ulmshft 25671* | A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯β(π + πΎ)) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π» = (π β π β¦ (πΉβ(π β πΎ)))) β β’ (π β (πΉ(βπ’βπ)πΊ β π»(βπ’βπ)πΊ)) | ||
Theorem | ulm0 25672 | Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β πΊ:πβΆβ) β β’ ((π β§ π = β ) β πΉ(βπ’βπ)πΊ) | ||
Theorem | ulmuni 25673 | A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.) |
β’ ((πΉ(βπ’βπ)πΊ β§ πΉ(βπ’βπ)π») β πΊ = π») | ||
Theorem | ulmdm 25674 | 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.) |
β’ (πΉ β dom (βπ’βπ) β πΉ(βπ’βπ)((βπ’βπ)βπΉ)) | ||
Theorem | ulmcaulem 25675* | Lemma for ulmcau 25676 and ulmcau2 25677: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 15175. (Contributed by Mario Carneiro, 1-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) β β’ (π β (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) | ||
Theorem | ulmcau 25676* | A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < π₯ 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 25677 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) β β’ (π β (πΉ β dom (βπ’βπ) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) | ||
Theorem | ulmcau2 25677* | A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < π₯ there is a π such that for all π β€ π, π the functions πΉ(π) and πΉ(π) are uniformly within π₯ of each other on π. (Contributed by Mario Carneiro, 1-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) β β’ (π β (πΉ β dom (βπ’βπ) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) | ||
Theorem | ulmss 25678* | A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π₯ β π) β π΄ β π) & β’ (π β (π₯ β π β¦ π΄)(βπ’βπ)πΊ) β β’ (π β (π₯ β π β¦ (π΄ βΎ π))(βπ’βπ)(πΊ βΎ π)) | ||
Theorem | ulmbdd 25679* | A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ ((π β§ π β π) β βπ₯ β β βπ§ β π (absβ((πΉβπ)βπ§)) β€ π₯) & β’ (π β πΉ(βπ’βπ)πΊ) β β’ (π β βπ₯ β β βπ§ β π (absβ(πΊβπ§)) β€ π₯) | ||
Theorem | ulmcn 25680 | A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(πβcnββ)) & β’ (π β πΉ(βπ’βπ)πΊ) β β’ (π β πΊ β (πβcnββ)) | ||
Theorem | ulmdvlem1 25681* | Lemma for ulmdv 25684. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β {β, β}) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π§ β π) β (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) & β’ (π β (π β π β¦ (π D (πΉβπ)))(βπ’βπ)π») & β’ ((π β§ π) β πΆ β π) & β’ ((π β§ π) β π β β+) & β’ ((π β§ π) β π β β+) & β’ ((π β§ π) β π β β+) & β’ ((π β§ π) β π < π) & β’ ((π β§ π) β (πΆ(ballβ((abs β β ) βΎ (π Γ π)))π) β π) & β’ ((π β§ π) β (absβ(π β πΆ)) < π) & β’ ((π β§ π) β π β π) & β’ ((π β§ π) β βπ β (β€β₯βπ)βπ₯ β π (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π / 2) / 2)) & β’ ((π β§ π) β (absβ(((π D (πΉβπ))βπΆ) β (π»βπΆ))) < (π / 2)) & β’ ((π β§ π) β π β π) & β’ ((π β§ π) β π β πΆ) & β’ ((π β§ π) β ((absβ(π β πΆ)) < π β (absβ(((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ))) < ((π / 2) / 2))) β β’ ((π β§ π) β (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β (π»βπΆ))) < π ) | ||
Theorem | ulmdvlem2 25682* | Lemma for ulmdv 25684. (Contributed by Mario Carneiro, 8-May-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β {β, β}) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π§ β π) β (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) & β’ (π β (π β π β¦ (π D (πΉβπ)))(βπ’βπ)π») β β’ ((π β§ π β π) β dom (π D (πΉβπ)) = π) | ||
Theorem | ulmdvlem3 25683* | Lemma for ulmdv 25684. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
β’ π = (β€β₯βπ) & β’ (π β π β {β, β}) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π§ β π) β (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) & β’ (π β (π β π β¦ (π D (πΉβπ)))(βπ’βπ)π») β β’ ((π β§ π§ β π) β π§(π D πΊ)(π»βπ§)) | ||
Theorem | ulmdv 25684* | 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.) |
β’ π = (β€β₯βπ) & β’ (π β π β {β, β}) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π§ β π) β (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) & β’ (π β (π β π β¦ (π D (πΉβπ)))(βπ’βπ)π») β β’ (π β (π D πΊ) = π») | ||
Theorem | mtest 25685* | 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.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π β π) & β’ ((π β§ π β π) β (πβπ) β β) & β’ ((π β§ (π β π β§ π§ β π)) β (absβ((πΉβπ)βπ§)) β€ (πβπ)) & β’ (π β seqπ( + , π) β dom β ) β β’ (π β seqπ( βf + , πΉ) β dom (βπ’βπ)) | ||
Theorem | mtestbdd 25686* | Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π β π) & β’ ((π β§ π β π) β (πβπ) β β) & β’ ((π β§ (π β π β§ π§ β π)) β (absβ((πΉβπ)βπ§)) β€ (πβπ)) & β’ (π β seqπ( + , π) β dom β ) & β’ (π β seqπ( βf + , πΉ)(βπ’βπ)π) β β’ (π β βπ₯ β β βπ§ β π (absβ(πβπ§)) β€ π₯) | ||
Theorem | mbfulm 25687 | 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 24954.) (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆMblFn) & β’ (π β πΉ(βπ’βπ)πΊ) β β’ (π β πΊ β MblFn) | ||
Theorem | iblulm 25688 | A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπΏ1) & β’ (π β πΉ(βπ’βπ)πΊ) & β’ (π β (volβπ) β β) β β’ (π β πΊ β πΏ1) | ||
Theorem | itgulm 25689* | A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπΏ1) & β’ (π β πΉ(βπ’βπ)πΊ) & β’ (π β (volβπ) β β) β β’ (π β (π β π β¦ β«π((πΉβπ)βπ₯) dπ₯) β β«π(πΊβπ₯) dπ₯) | ||
Theorem | itgulm2 25690* | A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (π₯ β π β¦ π΄) β πΏ1) & β’ (π β (π β π β¦ (π₯ β π β¦ π΄))(βπ’βπ)(π₯ β π β¦ π΅)) & β’ (π β (volβπ) β β) β β’ (π β ((π₯ β π β¦ π΅) β πΏ1 β§ (π β π β¦ β«ππ΄ dπ₯) β β«ππ΅ dπ₯)) | ||
Theorem | pserval 25691* | Value of the function πΊ that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) β β’ (π β β β (πΊβπ) = (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) | ||
Theorem | pserval2 25692* | Value of the function πΊ that gives the sequence of monomials of a power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) β β’ ((π β β β§ π β β0) β ((πΊβπ)βπ) = ((π΄βπ) Β· (πβπ))) | ||
Theorem | psergf 25693* | The sequence of terms in the infinite sequence defining a power series for fixed π. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ (π β π β β) β β’ (π β (πΊβπ):β0βΆβ) | ||
Theorem | radcnvlem1 25694* | Lemma for radcnvlt1 25699, radcnvle 25701. 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.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (absβπ) < (absβπ)) & β’ (π β seq0( + , (πΊβπ)) β dom β ) & β’ π» = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) β β’ (π β seq0( + , π») β dom β ) | ||
Theorem | radcnvlem2 25695* | Lemma for radcnvlt1 25699, radcnvle 25701. 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.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (absβπ) < (absβπ)) & β’ (π β seq0( + , (πΊβπ)) β dom β ) β β’ (π β seq0( + , (abs β (πΊβπ))) β dom β ) | ||
Theorem | radcnvlem3 25696* | Lemma for radcnvlt1 25699, radcnvle 25701. 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.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (absβπ) < (absβπ)) & β’ (π β seq0( + , (πΊβπ)) β dom β ) β β’ (π β seq0( + , (πΊβπ)) β dom β ) | ||
Theorem | radcnv0 25697* | Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) β β’ (π β 0 β {π β β β£ seq0( + , (πΊβπ)) β dom β }) | ||
Theorem | radcnvcl 25698* | The radius of convergence π of an infinite series is a nonnegative extended real number. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) β β’ (π β π β (0[,]+β)) | ||
Theorem | radcnvlt1 25699* | 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.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ (π β π β β) & β’ (π β (absβπ) < π ) & β’ π» = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) β β’ (π β (seq0( + , π») β dom β β§ seq0( + , (abs β (πΊβπ))) β dom β )) | ||
Theorem | radcnvlt2 25700* | If π is within the open disk of radius π centered at zero, then the infinite series converges at π. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) & β’ (π β π΄:β0βΆβ) & β’ π = sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*, < ) & β’ (π β π β β) & β’ (π β (absβπ) < π ) β β’ (π β seq0( + , (πΊβπ)) β dom β ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |