proposition: Lemma filterlim_bounded {K : AbsRing} {V : NormedModule K} (a : nat -> V) : (exists x, filterlim a eventually (locally x)) -> {M : R | forall n, norm (a n) <= M}.
proof: Proof. intros Ha. assert (exists x : R, filterlim (fun n => norm (a n)) eventually (locally x)). destruct Ha as [l Hl]. exists (norm l). eapply filterlim_comp. by apply Hl. by apply filterlim_norm. clear Ha. destruct (LPO_ub_dec (fun n => norm (a n))) as [[M HM]|HM]. now exists M. exfalso. case: H => l Hl. assert (H := proj1 (filterlim_locally (F := eventually) _ l) Hl (mkposreal _ Rlt_0_1)). clear Hl ; simpl in H ; rewrite /ball /= /AbsRing_ball in H. destruct H as [N HN]. specialize (HM (seq.foldr Rmax (1 + norm l) (seq.map (fun n => norm (a n)) (seq.iota 0 N)))). destruct HM as [n Hn]. revert Hn. apply Rle_not_lt. elim: N a n HN => /=[ |N IH] a n HN. rewrite Rplus_comm. apply Rlt_le, Rabs_lt_between'. eapply Rle_lt_trans, HN. rewrite /abs /=. eapply Rle_trans, (norm_triangle_inv (norm (a n)) l). apply Req_le, f_equal, f_equal2 => //. apply sym_eq, Rabs_pos_eq, norm_ge_0. by apply Nat.le_0_l. case: n => [ | n]. apply Rmax_l. eapply Rle_trans, Rmax_r. eapply Rle_trans. apply (IH (fun n => a (S n))). intros k Hk. apply HN. by apply le_n_S. clear. apply Req_le. elim: N 0%nat => /=[ |N IH] n0. by []. apply f_equal. apply IH. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub