proposition: Lemma derivable_sum n (h : 'I_n -> V -> W) (x v : V) : (forall i, derivable (h i) x v) -> derivable (\sum_(i < n) h i) x v.
proof: Proof. move=> df; suff : forall i, is_derive x v (h i) ('D_v (h i) x) by []. by move=> ?; apply: derivableP. 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