Library Interval.Real.Taylor
This file is part of the CoqApprox formalization of rigorous
polynomial approximation in Coq:
http://tamadi.gforge.inria.fr/CoqApprox/
Copyright (C) 2010-2012, ENS de Lyon.
Copyright (C) 2010-2016, Inria.
Copyright (C) 2014-2016, IRIT.
This library is governed by the CeCILL-C license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/or redistribute the library under the terms of the CeCILL-C
license as circulated by CEA, CNRS and Inria at the following URL:
http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the library's author, the holder of
the economic rights, and the successive licensors have only limited
liability. See the COPYING file for more details.
From Coq Require Import Reals Psatz.
From Coquelicot Require Import Coquelicot.
Require Import Stdlib.
Local Open Scope R_scope.
Lemma Rolle_lim (f : R → R) (a b : R) (h : R → R) :
(∀ x : R, a < x < b ∨ b < x < a → derivable_pt_lim f x (h x)) →
(∀ x : R, a ≤ x ≤ b ∨ b ≤ x ≤ a → continuity_pt f x) →
a ≠ b →
f a = f b →
∃ c : R, (a < c < b ∨ b < c < a) ∧ derivable_pt_lim f c 0.
Section TaylorLagrange.
Variables a b : R.
Variable n : nat.
Notation Cab x := (a ≤ x ≤ b) (only parsing).
Notation Oab x := (a < x < b) (only parsing).
Variable D : nat → R → R.
Notation Tcoeff n x0 := (D n x0 / (INR (fact n))) (only parsing).
Notation Tterm n x0 x := (Tcoeff n x0 × (x - x0)^n) (only parsing).
Notation Tsum n x0 x := (sum_f_R0 (fun i ⇒ Tterm i x0 x) n) (only parsing).
Lemma continuity_pt_sum (f : nat → R → R) (x : R) :
(∀ k, (k ≤ n)%nat → continuity_pt (f k) x) →
continuity_pt
(fun y ⇒ (sum_f_R0 (fun n ⇒ f n y) n)) x.
Lemma derivable_pt_lim_sum (f : nat → R → R) (x : R) (lf : nat → R) :
(∀ i, (i ≤ n)%nat → derivable_pt_lim (f i) x (lf i)) →
derivable_pt_lim
(fun y ⇒ (sum_f_R0 (fun n ⇒ f n y) n)) x
(sum_f_R0 lf n).
Section TL.
Hypothesis derivable_pt_lim_Dp :
∀ k x, (k ≤ n)%nat → Oab x →
derivable_pt_lim (D k) x (D (S k) x).
Hypothesis continuity_pt_Dp :
∀ k x, (k ≤ n)%nat → Cab x →
continuity_pt (D k) x.
Variables x0 x : R.
Let c := (D 0 x - Tsum n x0 x) / (x - x0)^(S n).
Let g := fun y ⇒ D 0 x - Tsum n y x - c × (x - y)^(S n).
Hypotheses (Hx0 : Cab x0) (Hx : Cab x).
Lemma derivable_pt_lim_aux (y : R) :
Oab y →
derivable_pt_lim g y (- ((D (S n) y) / (INR (fact n)) × (x - y)^n)
+ c × (INR (S n)) × (x - y)^n).
Theorem Taylor_Lagrange :
∃ xi : R,
D 0 x - Tsum n x0 x =
Tcoeff (S n) xi × (x - x0)^(S n)
∧ (x0 ≠ x → x0 < xi < x ∨ x < xi < x0).
End TL.
Section CorTL.
Hypothesis derivable_pt_lim_Dp :
∀ k x, (k ≤ n)%nat → Cab x →
derivable_pt_lim (D k) x (D (S k) x).
Theorem Cor_Taylor_Lagrange (x0 x : R) :
Cab x0 → Cab x →
∃ c,
D 0 x - Tsum n x0 x =
Tcoeff (S n) c × (x - x0)^(S n)
∧ (x0 ≠ x → x0 < c < x ∨ x < c < x0).
End CorTL.
End TaylorLagrange.
Let g := fun y ⇒ D 0 x - Tsum n y x - c × (x - y)^(S n).
Hypotheses (Hx0 : Cab x0) (Hx : Cab x).
Lemma derivable_pt_lim_aux (y : R) :
Oab y →
derivable_pt_lim g y (- ((D (S n) y) / (INR (fact n)) × (x - y)^n)
+ c × (INR (S n)) × (x - y)^n).
Theorem Taylor_Lagrange :
∃ xi : R,
D 0 x - Tsum n x0 x =
Tcoeff (S n) xi × (x - x0)^(S n)
∧ (x0 ≠ x → x0 < xi < x ∨ x < xi < x0).
End TL.
Section CorTL.
Hypothesis derivable_pt_lim_Dp :
∀ k x, (k ≤ n)%nat → Cab x →
derivable_pt_lim (D k) x (D (S k) x).
Theorem Cor_Taylor_Lagrange (x0 x : R) :
Cab x0 → Cab x →
∃ c,
D 0 x - Tsum n x0 x =
Tcoeff (S n) c × (x - x0)^(S n)
∧ (x0 ≠ x → x0 < c < x ∨ x < c < x0).
End CorTL.
End TaylorLagrange.