proposition: Lemma is_LimSup_infSup_seq (u : nat -> R) (l : Rbar) : is_LimSup_seq u l <-> is_inf_seq (fun m => Sup_seq (fun n => u (n + m)%nat)) l.
proof: Proof. case: l => [l | | ] ; rewrite /is_LimSup_seq /is_inf_seq ; split => Hl. split. move => N. apply Sup_seq_minor_lt. case: (proj1 (Hl eps) N) => {Hl} n Hl. exists (n - N)%nat. rewrite MyNat.sub_add ; intuition. case: (proj2 (Hl (pos_div_2 eps))) => /= {Hl} N Hl. exists N ; rewrite /Sup_seq ; case: ex_sup_seq => un Hun ; simpl proj1_sig. case: un Hun => [un | | ] /= Hun. case: (proj2 (Hun (pos_div_2 eps))) => {Hun} /= n Hun. apply Rlt_minus_l in Hun. apply Rlt_trans with (1 := Hun). apply Rlt_minus_r. apply Rlt_le_trans with (1 := Hl _ (MyNat.le_add_l _ _)) ; right ; field. case: (Hun (l + eps / 2)) => {Hun} n. apply Rle_not_lt, Rlt_le, Hl, MyNat.le_add_l. by []. split. move => N. move: (proj1 (Hl eps) N) => {} Hl. apply Sup_seq_minor_lt in Hl. case: Hl => /= n Hl. exists (n + N)%nat ; intuition. case: (proj2 (Hl eps)) => {Hl} N Hl. exists N => n Hn. apply (Rbar_not_le_lt (l + eps) (u n)). contradict Hl. apply Rbar_le_not_lt. apply Sup_seq_minor_le with (n - N)%nat. by rewrite MyNat.sub_add. move => M N. case: (Hl M N) => {Hl} n Hl. apply Sup_seq_minor_lt. exists (n - N)%nat. rewrite MyNat.sub_add ; intuition. move => M N. move: (Hl M N) => {} Hl. apply Sup_seq_minor_lt in Hl. case: Hl => /= n Hl. exists (n + N)%nat ; intuition. move => M. case: (Hl (M-1)) => {Hl} N Hl. exists N ; rewrite /Sup_seq ; case: ex_sup_seq => un Hun ; simpl proj1_sig. case: un Hun => [un | | ] /= Hun. case: (proj2 (Hun (mkposreal _ Rlt_0_1))) => {Hun} /= n Hun. apply Rlt_minus_l in Hun. apply Rlt_trans with (1 := Hun). apply Rlt_minus_r. apply Hl ; intuition. case: (Hun (M-1)) => {Hun} n. apply Rle_not_lt, Rlt_le, Hl, MyNat.le_add_l. by []. move => M. case: (Hl M) => {Hl} N Hl. exists N => n Hn. apply (Rbar_not_le_lt M (u n)). contradict Hl. apply Rbar_le_not_lt. apply Sup_seq_minor_le with (n - N)%nat. by rewrite MyNat.sub_add. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy