proposition: Lemma mulOmega (R : realFieldType) (F : filter_on pT) (h1 h2 f g : pT -> R^o) : [Omega_F h1 of f] * [Omega_F h2 of g] =Omega_F (h1 * h2).
proof: Proof. rewrite eqOmegaE eqOmegaO [in RHS]bigOE //. have [W1 k1 ?] := bigOmega; have [W2 k2 ?] := bigOmega. near=> k; near=> x; rewrite [`|_|]normrM. rewrite (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(W1 * W2) x|)) //. rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //. rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (W1 x)). by rewrite ler_pM ?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