proposition: Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) : continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ (0 : U * V') id.
proof: Proof. move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc. apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//. rewrite ler_pM ?pmulr_rge0 //; last by rewrite num_le_maxr /= lexx orbT. rewrite -ler_pdivlMl //. suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite num_le_maxr /= lexx. near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm. by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite /= distrC subr0 => /ltW. Unshelve. all: by end_near. 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