proposition: Lemma mine_cvg_minr_cvg u r : (0 < r)%R -> (forall k, 0 <= u k) -> mine (u n) r%:E @[n --> \oo] --> 0 -> minr (fine (u n)) r @[n --> \oo] --> 0%R.
proof: Proof. move=> r0 u0 mine_cvg; apply: (cvg_trans _ (fine_cvg mine_cvg)). move/fine_cvgP : mine_cvg => [_ /=] /cvgrPdist_lt. move=> /(_ _ r0)[N _ hN]; apply: near_eq_cvg; near=> n. have xnoo : u n < +oo. rewrite ltNge leye_eq; apply/eqP => xnoo. have /hN : (N <= n)%N by near: n; exists N. by rewrite /= sub0r normrN xnoo //= gtr0_norm // ltxx. by rewrite /= -(@fineK _ (u n)) ?ge0_fin_numE//= -fine_min. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau