proposition: Lemma differentiable_sum n (f : 'I_n -> V -> W) (x : V) : (forall i, differentiable (f i) x) -> differentiable (\sum_(i < n) f i) x.
proof: Proof. by elim/big_ind : _ => // ? ? g h ?; apply: differentiableD; [exact:g|exact:h]. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms