proposition: Lemma ex_dom_bound {T : Type} {K : numFieldType} {V W : pseudoMetricNormedZmodType K} (h : T -> V) (f : T -> W) (F : set_system T) {PF : ProperFilter F}: (\forall M \near +oo, dominated_by h M f F) <-> exists M, dominated_by h M f F.
proof: Proof. rewrite /dominated_by; split => [/pinfty_ex_gt0[M M_gt0]|[M]] FM. by exists M. have [] := pselect (exists x, (h x != 0) && (`|f x| <= M * `|h x|)); last first. rewrite -forallNE => Nex; exists 0; split => //. move=> k k_gt0; apply: filterS FM => x /= f_le_Mh. have /negP := Nex x; rewrite negb_and negbK f_le_Mh orbF => /eqP h_eq0. by rewrite h_eq0 normr0 !mulr0 in f_le_Mh *. case => x0 /andP[hx0_neq0] /(le_trans (normr_ge0 _)) /ger0_real. rewrite realrM // ?normr_eq0// => M_real. exists M; split => // k Mk; apply: filterS FM => x /le_trans/= ->//. by rewrite ler_wpM2r// ltW. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule