proposition: Lemma diff_bilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p : continuous (fun p => f p.1 p.2) -> 'd (fun q => f q.1 q.2) p = (fun q => f p.1 q.2 + f q.1 p.2) :> (U * V' -> W').
proof: Proof. pose d q := f p.1 q.2 + f q.1 p.2. move=> fc; have lind : linear d. by move=> ???; rewrite /d linearPr linearPl scalerDr addrACA. pose dlM := GRing.isLinear.Build _ _ _ _ _ lind. pose dL : {linear _ -> _} := HB.pack d dlM. rewrite -/d -[d]/(dL : _ -> _). by apply/diff_unique; have [] := dbilin p fc. 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