proposition: Lemma compOo_eqo (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') : [O_ (0 : V') id of g] \o [o_ (0 : U) id of f] =o_ (0 : U) id.
proof: Proof. apply/eqoP => _ /posnumP[e]. have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ (0 : V') id of g]]. move=> /nbhs_ballP [_ /posnumP[d] hd]. have ekgt0 : e%:num / k%:num > 0 by []. have /(_ _ ekgt0) := littleoP [littleo of [o_ (0 : U) id of f]]. apply: filter_app; near=> x => leoxekx; apply: le_trans (hd _ _) _; last first. by rewrite -ler_pdivlMl // mulrA [_^-1 * _]mulrC. by rewrite -ball_normE /= distrC subr0 (le_lt_trans leoxekx)// -ltr_pdivlMl //. 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