proposition: Lemma diff1E f x : differentiable f x -> 'd f x = (fun h => h *: f^`() x) :> (R -> U).
proof: Proof. pose d (h : R) := h *: 'd f x 1. 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. have -> : (fun h => h *: f^`() x) = scalL by rewrite derive1E'. apply: diff_unique; first exact: scalel_continuous. apply/eqaddoE; have /diff_locally -> := df; congr (_ + _ + _). by rewrite funeqE => h /=; rewrite -{1}[h]mulr1 linearZ. 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