Home | Metamath
Proof Explorer Theorem List (p. 240 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | aaliou3lem1 23901* | Lemma for aaliou3 23910. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴)))) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐺‘𝐵) ∈ ℝ) | ||
Theorem | aaliou3lem2 23902* | Lemma for aaliou3 23910. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴)))) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐹‘𝐵) ∈ (0(,](𝐺‘𝐵))) | ||
Theorem | aaliou3lem3 23903* | Lemma for aaliou3 23910. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦ ((2↑-(!‘𝐴)) · ((1 / 2)↑(𝑐 − 𝐴)))) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) ⇒ ⊢ (𝐴 ∈ ℕ → (seq𝐴( + , 𝐹) ∈ dom ⇝ ∧ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐹‘𝑏) ∈ ℝ+ ∧ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐹‘𝑏) ≤ (2 · (2↑-(!‘𝐴))))) | ||
Theorem | aaliou3lem8 23904* | Lemma for aaliou3 23910. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℕ (2 · (2↑-(!‘(𝑥 + 1)))) ≤ (𝐵 / ((2↑(!‘𝑥))↑𝐴))) | ||
Theorem | aaliou3lem4 23905* | Lemma for aaliou3 23910. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) & ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) & ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) ⇒ ⊢ 𝐿 ∈ ℝ | ||
Theorem | aaliou3lem5 23906* | Lemma for aaliou3 23910. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) & ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) & ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) ⇒ ⊢ (𝐴 ∈ ℕ → (𝐻‘𝐴) ∈ ℝ) | ||
Theorem | aaliou3lem6 23907* | Lemma for aaliou3 23910. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) & ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) & ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) ⇒ ⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) · (2↑(!‘𝐴))) ∈ ℤ) | ||
Theorem | aaliou3lem7 23908* | Lemma for aaliou3 23910. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) & ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) & ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) ⇒ ⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) ≠ 𝐿 ∧ (abs‘(𝐿 − (𝐻‘𝐴))) ≤ (2 · (2↑-(!‘(𝐴 + 1)))))) | ||
Theorem | aaliou3lem9 23909* | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎))) & ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) & ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) ⇒ ⊢ ¬ 𝐿 ∈ 𝔸 | ||
Theorem | aaliou3 23910 | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 23-Nov-2014.) |
⊢ Σ𝑘 ∈ ℕ (2↑-(!‘𝑘)) ∉ 𝔸 | ||
Syntax | ctayl 23911 | Taylor polynomial of a function. |
class Tayl | ||
Syntax | cana 23912 | The class of analytic functions. |
class Ana | ||
Definition | df-tayl 23913* | Define the Taylor polynomial or Taylor series of a function. TODO-AV: 𝑛 ∈ (ℕ0 ∪ {+∞}) can/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 23914* | 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 23915* | Lemma for taylfval 23917. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) ⇒ ⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ ℂ) | ||
Theorem | taylfvallem 23916* | Lemma for taylfval 23917. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ ℂ) → (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)))) ⊆ ℂ) | ||
Theorem | taylfval 23917* |
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 23923 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 23918* | 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 23919* | 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 23920* | 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 23921* | Lemma for taylpfval 23923 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) | ||
Theorem | taylplem2 23922* | Lemma for taylpfval 23923 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) ⇒ ⊢ (((𝜑 ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘)) ∈ ℂ) | ||
Theorem | taylpfval 23923* | 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 23924 | 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 23925* | Value of the Taylor polynomial. (Contributed by Mario Carneiro, 31-Dec-2016.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) & ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑇‘𝑋) = Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑋 − 𝐵)↑𝑘))) | ||
Theorem | taylply2 23926* | The Taylor polynomial is a polynomial of degree (at most) 𝑁. This version of taylply 23927 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 23927 | 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 23928 | 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 23929 | 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 23930 | 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 23931* | Lemma for taylth 23933. 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 23933 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 23932* | Lemma for taylth 23933. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵) & ⊢ (𝜑 → 𝑀 ∈ (1..^𝑁)) & ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))) limℂ 𝐵)) ⇒ ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵)) | ||
Theorem | taylth 23933* | 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 23934 | Extend class notation to include the uniform convergence predicate. |
class ⇝𝑢 | ||
Definition | df-ulm 23935* | 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 14067. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ ⇝𝑢 = (𝑠 ∈ V ↦ {〈𝑓, 𝑦〉 ∣ ∃𝑛 ∈ ℤ (𝑓:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑠) ∧ 𝑦:𝑠⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑠 (abs‘(((𝑓‘𝑘)‘𝑧) − (𝑦‘𝑧))) < 𝑥)}) | ||
Theorem | ulmrel 23936 | The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ Rel (⇝𝑢‘𝑆) | ||
Theorem | ulmscl 23937 | Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V) | ||
Theorem | ulmval 23938* | Express the predicate: The sequence of functions 𝐹 converges uniformly to 𝐺 on 𝑆. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝑆 ∈ 𝑉 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) | ||
Theorem | ulmcl 23939 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) | ||
Theorem | ulmf 23940* | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → ∃𝑛 ∈ ℤ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) | ||
Theorem | ulmpm 23941 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐹 ∈ ((ℂ ↑𝑚 𝑆) ↑pm ℤ)) | ||
Theorem | ulmf2 23942 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ ((𝐹 Fn 𝑍 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) | ||
Theorem | ulm2 23943* | Simplify ulmval 23938 when 𝐹 and 𝐺 are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) & ⊢ (𝜑 → 𝐺:𝑆⟶ℂ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) | ||
Theorem | ulmi 23944* | The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝐶) | ||
Theorem | ulmclm 23945* | A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘)‘𝐴) = (𝐻‘𝑘)) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐻 ⇝ (𝐺‘𝐴)) | ||
Theorem | ulmres 23946 | 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 23947* | Lemma for ulmshft 23948. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) & ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐻(⇝𝑢‘𝑆)𝐺)) | ||
Theorem | ulmshft 23948* | A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝐾)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) & ⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ 𝐻(⇝𝑢‘𝑆)𝐺)) | ||
Theorem | ulm0 23949 | Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) & ⊢ (𝜑 → 𝐺:𝑆⟶ℂ) ⇒ ⊢ ((𝜑 ∧ 𝑆 = ∅) → 𝐹(⇝𝑢‘𝑆)𝐺) | ||
Theorem | ulmuni 23950 | An sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017.) |
⊢ ((𝐹(⇝𝑢‘𝑆)𝐺 ∧ 𝐹(⇝𝑢‘𝑆)𝐻) → 𝐺 = 𝐻) | ||
Theorem | ulmdm 23951 | 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 23952* | Lemma for ulmcau 23953 and ulmcau2 23954: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 13943. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥)) | ||
Theorem | ulmcau 23953* | 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 23954 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom (⇝𝑢‘𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) | ||
Theorem | ulmcau2 23954* | 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.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom (⇝𝑢‘𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥)) | ||
Theorem | ulmss 23955* | A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇)) | ||
Theorem | ulmbdd 23956* | A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘((𝐹‘𝑘)‘𝑧)) ≤ 𝑥) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘(𝐺‘𝑧)) ≤ 𝑥) | ||
Theorem | ulmcn 23957 | A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(𝑆–cn→ℂ)) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑆–cn→ℂ)) | ||
Theorem | ulmdvlem1 23958* | Lemma for ulmdv 23961. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝜓) → 𝑈 < 𝑊) & ⊢ ((𝜑 ∧ 𝜓) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ 𝑋) & ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) < 𝑈) & ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝜓) → ∀𝑚 ∈ (ℤ≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2)) & ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝐶) − (𝐻‘𝐶))) < (𝑅 / 2)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ≠ 𝐶) & ⊢ ((𝜑 ∧ 𝜓) → ((abs‘(𝑌 − 𝐶)) < 𝑊 → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < ((𝑅 / 2) / 2))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − (𝐻‘𝐶))) < 𝑅) | ||
Theorem | ulmdvlem2 23959* | Lemma for ulmdv 23961. (Contributed by Mario Carneiro, 8-May-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝑆 D (𝐹‘𝑘)) = 𝑋) | ||
Theorem | ulmdvlem3 23960* | Lemma for ulmdv 23961. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧(𝑆 D 𝐺)(𝐻‘𝑧)) | ||
Theorem | ulmdv 23961* | 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.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐺:𝑋⟶ℂ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) ⇒ ⊢ (𝜑 → (𝑆 D 𝐺) = 𝐻) | ||
Theorem | mtest 23962* | 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.) |
⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐹‘𝑘)‘𝑧)) ≤ (𝑀‘𝑘)) & ⊢ (𝜑 → seq𝑁( + , 𝑀) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → seq𝑁( ∘𝑓 + , 𝐹) ∈ dom (⇝𝑢‘𝑆)) | ||
Theorem | mtestbdd 23963* | Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐹‘𝑘)‘𝑧)) ≤ (𝑀‘𝑘)) & ⊢ (𝜑 → seq𝑁( + , 𝑀) ∈ dom ⇝ ) & ⊢ (𝜑 → seq𝑁( ∘𝑓 + , 𝐹)(⇝𝑢‘𝑆)𝑇) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 (abs‘(𝑇‘𝑧)) ≤ 𝑥) | ||
Theorem | mbfulm 23964 | 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 23241.) (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶MblFn) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ MblFn) | ||
Theorem | iblulm 23965 | A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝐿1) & ⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) & ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐿1) | ||
Theorem | itgulm 23966* | 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 23967* | A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ 𝐿1) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵)) & ⊢ (𝜑 → (vol‘𝑆) ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐵) ∈ 𝐿1 ∧ (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥) ⇝ ∫𝑆𝐵 d𝑥)) | ||
Theorem | pserval 23968* | 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 23969* | 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 23970* | 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 23971* | Lemma for radcnvlt1 23976, radcnvle 23978. 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 23972* | Lemma for radcnvlt1 23976, radcnvle 23978. 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 23973* | Lemma for radcnvlt1 23976, radcnvle 23978. 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 23974* | Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) ⇒ ⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) | ||
Theorem | radcnvcl 23975* | 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 23976* | 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 23977* | 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 ⇝ ) | ||
Theorem | radcnvle 23978* | 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.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → (abs‘𝑋) ≤ 𝑅) | ||
Theorem | dvradcnv 23979* | 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.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝑋) < 𝑅) ⇒ ⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ ) | ||
Theorem | pserulm 23980* | 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.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑀 < 𝑅) & ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀))) ⇒ ⊢ (𝜑 → 𝐻(⇝𝑢‘𝑆)𝐹) | ||
Theorem | psercn2 23981* | Since by pserulm 23980 the series converges uniformly, it is also continuous by ulmcn 23957. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 𝑀 < 𝑅) & ⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) | ||
Theorem | psercnlem2 23982* | Lemma for psercn 23984. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ − ))𝑀) ∧ (0(ball‘(abs ∘ − ))𝑀) ⊆ (◡abs “ (0[,]𝑀)) ∧ (◡abs “ (0[,]𝑀)) ⊆ 𝑆)) | ||
Theorem | psercnlem1 23983* | Lemma for psercn 23984. (Contributed by Mario Carneiro, 18-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) | ||
Theorem | psercn 23984* | 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.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) | ||
Theorem | pserdvlem1 23985* | Lemma for pserdv 23987. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧ (abs‘𝑎) < (((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅)) | ||
Theorem | pserdvlem2 23986* | Lemma for pserdv 23987. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) & ⊢ 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (ℂ D (𝐹 ↾ 𝐵)) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) | ||
Theorem | pserdv 23987* | The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) & ⊢ 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⇒ ⊢ (𝜑 → (ℂ D 𝐹) = (𝑦 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) | ||
Theorem | pserdv2 23988* | The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝑆 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) & ⊢ 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⇒ ⊢ (𝜑 → (ℂ D 𝐹) = (𝑦 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ ((𝑘 · (𝐴‘𝑘)) · (𝑦↑(𝑘 − 1))))) | ||
Theorem | abelthlem1 23989* | Lemma for abelth 23999. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) | ||
Theorem | abelthlem2 23990* | Lemma for abelth 23999. The peculiar region 𝑆, known as a Stolz angle , is a teardrop-shaped subset of the closed unit ball containing 1. Indeed, except for 1 itself, the rest of the Stolz angle is enclosed in the open unit ball. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⇒ ⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))) | ||
Theorem | abelthlem3 23991* | Lemma for abelth 23999. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ ) | ||
Theorem | abelthlem4 23992* | Lemma for abelth 23999. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ⇒ ⊢ (𝜑 → 𝐹:𝑆⟶ℂ) | ||
Theorem | abelthlem5 23993* | Lemma for abelth 23999. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) | ||
Theorem | abelthlem6 23994* | Lemma for abelth 23999. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) & ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | ||
Theorem | abelthlem7a 23995* | Lemma for abelth 23999. (Contributed by Mario Carneiro, 8-May-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) & ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) ⇒ ⊢ (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))))) | ||
Theorem | abelthlem7 23996* | Lemma for abelth 23999. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) & ⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅) & ⊢ (𝜑 → (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) ⇒ ⊢ (𝜑 → (abs‘(𝐹‘𝑋)) < ((𝑀 + 1) · 𝑅)) | ||
Theorem | abelthlem8 23997* | Lemma for abelth 23999. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) & ⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) ⇒ ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) | ||
Theorem | abelthlem9 23998* | Lemma for abelth 23999. By adjusting the constant term, we can assume that the entire series converges to 0. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ⇒ ⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) | ||
Theorem | abelth 23999* | Abel's theorem. If the power series Σ𝑛 ∈ ℕ0𝐴(𝑛)(𝑥↑𝑛) is convergent at 1, then it is equal to the limit from "below", along a Stolz angle 𝑆 (note that the 𝑀 = 1 case of a Stolz angle is the real line [0, 1]). (Continuity on 𝑆 ∖ {1} follows more generally from psercn 23984.) (Contributed by Mario Carneiro, 2-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑀) & ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) | ||
Theorem | abelth2 24000* | Abel's theorem, restricted to the [0, 1] interval. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ ) & ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((0[,]1)–cn→ℂ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |