proposition: Lemma cvg_approx x (f0 : forall x, D x -> (0 <= f x)%E) : D x -> (f x < +oo)%E -> approx^~ x @ \oo --> fine (f x).
proof: Proof. move=> Dx fxoo; have fxfin : f x \is a fin_num by rewrite ge0_fin_numE// f0. apply/(@cvgrPdist_lt _ [the normedModType R of R^o]) => _/posnumP[e]. have [fx0|fx0] := eqVneq (f x) 0%E. by near=> n; rewrite f0_approx0 // fx0 /= subrr normr0. have /(fpos_approx_neq0 Dx)[m _ Hm] : (0 < f x < +oo)%E by rewrite lt0e fx0 f0. near=> n. have mn : (m <= n)%N by near: n; exists m. have : fine (f x) < n%:R. near: n. exists `|floor (fine (f x))|.+1%N => //= p /=. rewrite -(@ler_nat R); apply: lt_le_trans. rewrite -natr1 (_ : `| _ |%:R = (floor (fine (f x)))%:~R); last first. by rewrite -[in RHS](@gez0_abs (floor _))// floor_ge0//; exact/fine_ge0/f0. by rewrite lt_succ_floor. rewrite -lte_fin (fineK fxfin) => fxn. have [approx_nx0|[k [/andP[k0 kn2n] ? ->]]] := f_ub_approx fxn. by have := Hm _ mn; rewrite approx_nx0. rewrite inE /= => -[r /=]; rewrite in_itv /= => /andP[k1 k2] rfx. rewrite (@le_lt_trans _ _ (1 / 2 ^+ n)) //. rewrite ler_norml; apply/andP; split. rewrite lerBrDl -mulrBl -lee_fin (fineK fxfin) -rfx lee_fin. by rewrite (le_trans _ k1)// ler_pM2r// lerBlDl lerDr. by rewrite lerBlDr -mulrDl -lee_fin nat1r fineK// ltW// -rfx lte_fin. by near: n; exact: near_infty_natSinv_expn_lt. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun