proposition: Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p : continuous (fun p => f p.1 p.2) -> continuous (fun q => (f p.1 q.2 + f q.1 p.2)) /\ (fun q => f q.1 q.2) \o shift p = cst (f p.1 p.2) + (fun q => f p.1 q.2 + f q.1 p.2) +o_ (0 : U * V') id.
proof: Proof. move=> fc; split=> [q|]. by apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2)); move=> A /(fc (_.1, _.2)) /= /nbhs_ballP [_ /posnumP[e] fpqe_A]; apply/nbhs_ballP; exists e%:num => //= r [? ?]; exact: (fpqe_A (_.1, _.2)). apply/eqaddoE; rewrite funeqE => q /=. rewrite linearDl !linearDr addrA addrC. rewrite -[f q.1 _ + _ + _]addrA [f q.1 _ + _]addrC addrA [f q.1 _ + _]addrC. by congr (_ + _); rewrite -[LHS]/((fun p => f p.1 p.2) q) bilinear_eqo. 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