proposition: Lemma dvg_approx x : D x -> f x = +oo%E -> ~ cvgn (approx^~ x : _ -> R^o).
proof: Proof. move=> Dx fxoo; have approx_x n : approx n x = n%:R. rewrite /approx foo_B1// mulr1 big1 ?add0r// => /= i _. by rewrite fgen_A0 // ?mulr0 // fxoo leey. case/cvg_ex => /= l; have [l0|l0] := leP 0%R l. - move=> /cvgrPdist_lt/(_ _ ltr01) -[n _]. move=> /(_ (`|ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)). rewrite approx_x. apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //. rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//. rewrite natrD lerD// ?ler1n// ger0_norm // (le_trans (ceil_ge _)) //. by rewrite -(@gez0_abs (ceil _)) // ceil_ge0. - move/cvgrPdist_lt => /(_ _ ltr01) -[n _]. move=> /(_ (`|floor l|.+1 + n)%N) /= /(_ (leq_addl _ _)). rewrite approx_x. apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //. rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//. rewrite natrD lerD// ?ler1n// ler0_norm //; last by rewrite ltW. rewrite (@le_trans _ _ (- floor l)%:~R) //. by rewrite mulrNz lerNl opprK floor_le. by rewrite -(@lez0_abs (floor _)) // floor_le0 // ltW. 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