proposition: Lemma deriv1E f x : derivable f x 1 -> 'd f x = ( *:%R^~ (f^`() x)) :> (R -> U).
proof: Proof. pose d (h : R) := h *: f^`() x. move=> df; have lin_scal : linear d by move=> ???; rewrite /d scalerDl scalerA. pose scallM := GRing.isLinear.Build _ _ _ _ _ lin_scal. pose scalL : {linear _ -> _} := HB.pack d scallM. rewrite -/d -[d]/(scalL : _ -> _). by apply: diff_unique; [apply: scalel_continuous|apply: der1]. 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