proposition: Lemma mulTheta (F : filter_on pT) (h1 h2 f g : pT -> R^o) : [Theta_F h1 of f] * [Theta_F h2 of g] =Theta_F h1 * h2.
proof: Proof. rewrite eqThetaE bigThetaE; split. by rewrite (eqThetaO _ f) (eqThetaO _ g) mulO. rewrite eqOmegaO [in RHS]bigOE //. have [T1 k1 l1 P1 ?] := bigTheta; have [T2 k2 l2 P2 ?] := bigTheta. near=> k; first near=> x. rewrite [`|_|]normrM (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(T1 * T2) x|)) //. rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //. rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (T1 x)) ler_pM //; by [rewrite mulr_ge0 //|near: x]. by rewrite ler_wpM2r // ltW //. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule