proposition: Lemma addTheta (F : filter_on pT) (f g h : _ -> R^o) (f0 : forall x, 0 <= f x) (g0 : forall x, 0 <= g x) (h0 : forall x, 0 <= h x) : [Theta_F h of f] + [O_F h of g] =Theta_F h.
proof: Proof. rewrite eqThetaE bigThetaE; split; first by rewrite eqThetaO addO. rewrite -eqOmegaE; apply: addOmega. - by move=> ?; rewrite /the_bigTheta val_insubd /=; case: ifP. - by move=> ?; rewrite /the_bigO val_insubd /=; case: ifP. - rewrite eqOmegaE eqOmegaO; have [T1 k1 k2 ? ?] := bigTheta. rewrite bigOE //; apply/bigO_exP; exists k1%:num^-1 => //. by near do rewrite ler_pdivlMl //. 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