proposition: Lemma derive_big I (s : seq I) : forall (f : I -> R -> R) (x : R), (forall k : I, ex_derive (f k) x) -> Derive (fun y : Rdefinitions.R => \big[Rplus/0]_(i <- s) (f i y)) x = \big[(fun _ : unit => Rplus) tt/0]_(i <- s) ((Derive (f i)) x).
proof: Proof. move => f x Hf. elim: s => [ | a b Hrec] => /= . - rewrite (Derive_ext _ (fun x0 => 0)) => [|t]. by rewrite big_nil Derive_const. by rewrite big_nil. - rewrite (Derive_ext _ (fun t => f a t + \big[Rplus/0]_(j <- b) f j t)). + rewrite Derive_plus ?big_cons. * congr Rplus. by rewrite Hrec. * by apply: Hf. * by apply: ex_derive_big. + move => t. by rewrite big_cons. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound