Taylor Series
We now generalize our work on Taylor's theorem to define the Taylor series of an infinitely many times differentiable function as a power series. We prove convergence (always) of the Taylor series and give criteria for when the sum of this series is the original function.
Definitions
Let J be a proper interval and F an infinitely many times differentiable function in J. Let a be a point of J.
Section Definitions.
Variable J : interval.
Hypothesis pJ : proper J.
Variable F : PartIR.
Hypothesis diffF : forall n : N, Diffble_n n J pJ F.
Variable a : IR.
Hypothesis Ha : J a.
Definition Taylor_Series' :=
FPowerSeries' a (fun n : N => N_Deriv _ _ _ _ (diffF n) a Ha).
Assume also that f is the sequence of
derivatives of F.
Variable f : N -> PartIR.
Hypothesis derF : forall n, Derivative_n n J pJ F (f n).
Definition Taylor_Series := FPowerSeries' a
(fun n => f n a (Derivative_n_imp_inc' _ _ _ _ _ (derF n) _ Ha)).
Characterizations of the Taylor remainder.
Lemma Taylor_Rem_char : forall n H x Hx Hx' Hx'',
F x Hx[-]∑0 (S n) Taylor_Series x Hx' [=] Taylor_Rem J pJ F a x Ha Hx'' n H.
Lemma abs_Taylor_Rem_char : forall n H x Hx Hx' Hx'',
AbsIR (F x Hx[-]∑0 (S n) Taylor_Series x Hx') [=]
AbsIR (Taylor_Rem J pJ F a x Ha Hx'' n H).
End Definitions.
Section Convergence_in_IR.
Convergence
Our interval is now the real line. We begin by proving some helpful continuity properties, then define a boundedness condition for the derivatives of F that guarantees convergence of its Taylor series to F.
Hypothesis H : proper (-∞,+∞).
Variable F : PartIR.
Variable a : IR.
Hypothesis Ha : (-∞,+∞) a.
Variable f : N -> PartIR.
Hypothesis derF : forall n, Derivative_n n (-∞,+∞) H F (f n).
Lemma Taylor_Series_imp_cont : Continuous (-∞,+∞) F.
Lemma Taylor_Series_lemma_cont : forall r n,
Continuous (-∞,+∞) ((r[^]n[/] _[//]nring_fac_ap_zero _ n) {**}f n).
Definition Taylor_bnd := forall r H, conv_fun_seq'_IR (-∞,+∞)
(fun n => (r[^]n[/] _[//]nring_fac_ap_zero _ n) {**}f n) _ H (Continuous_const _ 0).
Hypothesis bndf : Taylor_bnd.
The Taylor series always converges on the realline.
We now prove that, under our assumptions, it actually converges to the
original function. For generality and also usability, however, we
will separately assume convergence.
Hypothesis Hf : fun_series_convergent_IR (-∞,+∞) (Taylor_Series _ _ _ a Ha _ derF).
Lemma Taylor_Series_conv_to_fun : ≈ (-∞,+∞) F (∑'∞ Hf).
End Convergence_in_IR.
Section Other_Results.
The condition for the previous lemma is not very easy to prove. We
give some helpful lemmas.
Lemma Taylor_bnd_trans : forall f g : N -> PartIR,
(forall n x Hx Hx', AbsIR (f n x Hx) [<=] AbsIR (g n x Hx')) ->
(forall n, Continuous (-∞,+∞) (g n)) -> Taylor_bnd g -> Taylor_bnd f.
Lemma bnd_imp_Taylor_bnd : forall (f : N -> PartIR) (F : PartIR),
(forall n x Hx Hx', AbsIR (f n x Hx) [<=] AbsIR (F x Hx')) -> Continuous (-∞,+∞) F ->
(forall n, ⊆ (fun _ => CTrue) (Dom (f n))) -> Taylor_bnd f.
Finally, a uniqueness criterium: two functions F and G are equal,
provided that their derivatives coincide at a given point and their
Taylor series converge to themselves.
Variables F G : PartIR.
Variable a : IR.
Variables f g : N -> PartIR.
Hypothesis derF : forall n, Derivative_n n (-∞,+∞) CI F (f n).
Hypothesis derG : forall n, Derivative_n n (-∞,+∞) CI G (g n).
Hypothesis bndf : Taylor_bnd f.
Hypothesis bndg : Taylor_bnd g.
Hypothesis Heq : forall n HaF HaG, f n a HaF [=] g n a HaG.
Lemma Taylor_unique_crit : ≈ (-∞,+∞) F (∑'∞ Hf) -> ≈ (-∞,+∞) F G.
End Other_Results.