From Coq Require Import Reals Psatz ssreflect.

Require Import Rcomplements Rbar Lub Markov Hierarchy.

Local Tactic Notation "intuition" := (intuition auto with arith zarith real).

Open Scope R_scope.

Definition is_sup_seq (u : nat → Rbar) (l : Rbar) :=
  match l with
    | Finite l ⇒ ∀ (eps : posreal), (∀ n, Rbar_lt (u n) (l+eps))
                                       ∧ (∃ n, Rbar_lt (l-eps) (u n))
    | p_infty ⇒ ∀ M : R, ∃ n, Rbar_lt M (u n)
    | m_infty ⇒ ∀ M : R, ∀ n, Rbar_lt (u n) M
  end.
Definition is_inf_seq (u : nat → Rbar) (l : Rbar) :=
  match l with
    | Finite l ⇒ ∀ (eps : posreal), (∀ n, Rbar_lt (Finite (l-eps)) (u n))
                                       ∧ (∃ n, Rbar_lt (u n) (Finite (l+eps)))
    | p_infty ⇒ ∀ M : R, ∀ n, Rbar_lt (Finite M) (u n)
    | m_infty ⇒ ∀ M : R, ∃ n, Rbar_lt (u n) (Finite M)
  end.

Lemma is_inf_opp_sup_seq (u : nat → Rbar) (l : Rbar) :
  is_inf_seq (fun n ⇒ Rbar_opp (u n)) (Rbar_opp l)
  ↔ is_sup_seq u l.
Lemma is_sup_opp_inf_seq (u : nat → Rbar) (l : Rbar) :
  is_sup_seq (fun n ⇒ Rbar_opp (u n)) (Rbar_opp l)
  ↔ is_inf_seq u l.

Lemma is_sup_seq_lub (u : nat → Rbar) (l : Rbar) :
  is_sup_seq u l → Rbar_is_lub (fun x ⇒ ∃ n, x = u n) l.

Lemma Rbar_is_lub_sup_seq (u : nat → Rbar) (l : Rbar) :
  Rbar_is_lub (fun x ⇒ ∃ n, x = u n) l → is_sup_seq u l.

Lemma is_inf_seq_glb (u : nat → Rbar) (l : Rbar) :
  is_inf_seq u l → Rbar_is_glb (fun x ⇒ ∃ n, x = u n) l.
Lemma Rbar_is_glb_inf_seq (u : nat → Rbar) (l : Rbar) :
  Rbar_is_glb (fun x ⇒ ∃ n, x = u n) l → is_inf_seq u l.

Lemma is_sup_seq_ext (u v : nat → Rbar) (l : Rbar) :
  (∀ n, u n = v n)
  → is_sup_seq u l → is_sup_seq v l.
Lemma is_inf_seq_ext (u v : nat → Rbar) (l : Rbar) :
  (∀ n, u n = v n)
  → is_inf_seq u l → is_inf_seq v l.

Lemma ex_sup_seq (u : nat → Rbar) : {l : Rbar | is_sup_seq u l}.

Lemma ex_inf_seq (u : nat → Rbar) : {l : Rbar | is_inf_seq u l}.

Definition Sup_seq (u : nat → Rbar) := proj1_sig (ex_sup_seq u).

Definition Inf_seq (u : nat → Rbar) := proj1_sig (ex_inf_seq u).

Lemma is_sup_seq_unique (u : nat → Rbar) (l : Rbar) :
  is_sup_seq u l → Sup_seq u = l.
Lemma Sup_seq_correct (u : nat → Rbar) :
  is_sup_seq u (Sup_seq u).
Lemma is_inf_seq_unique (u : nat → Rbar) (l : Rbar) :
  is_inf_seq u l → Inf_seq u = l.
Lemma Inf_seq_correct (u : nat → Rbar) :
  is_inf_seq u (Inf_seq u).

Lemma Sup_seq_ext (u v : nat → Rbar) :
  (∀ n, (u n) = (v n)) → Sup_seq u = Sup_seq v.
Lemma Inf_seq_ext (u v : nat → Rbar) :
  (∀ n, (u n) = (v n)) → Inf_seq u = Inf_seq v.

Lemma Rbar_sup_eq_lub (u : nat → Rbar) :
  Sup_seq u = Rbar_lub (fun x ⇒ ∃ n, x = u n).
Lemma Inf_eq_glb (u : nat → Rbar) :
  Inf_seq u = Rbar_glb (fun x ⇒ ∃ n, x = u n).

Lemma Sup_opp_inf (u : nat → Rbar) :
  Sup_seq u = Rbar_opp (Inf_seq (fun n ⇒ Rbar_opp (u n))).
Lemma Inf_opp_sup (u : nat → Rbar) :
  Inf_seq u = Rbar_opp (Sup_seq (fun n ⇒ Rbar_opp (u n))).

Lemma Sup_seq_scal_l (a : R) (u : nat → Rbar) : 0 ≤ a →
  Sup_seq (fun n ⇒ Rbar_mult a (u n)) = Rbar_mult a (Sup_seq u).
Lemma Inf_seq_scal_l (a : R) (u : nat → Rbar) : 0 ≤ a →
  Inf_seq (fun n ⇒ Rbar_mult a (u n)) = Rbar_mult a (Inf_seq u).

Lemma is_sup_seq_le (u v : nat → Rbar) {l1 l2 : Rbar} :
  (∀ n, Rbar_le (u n) (v n))
  → (is_sup_seq u l1) → (is_sup_seq v l2) → Rbar_le l1 l2.
Lemma is_inf_seq_le (u v : nat → Rbar) {l1 l2 : Rbar} :
  (∀ n, Rbar_le (u n) (v n))
  → (is_inf_seq u l1) → (is_inf_seq v l2) → Rbar_le l1 l2.

Lemma Sup_seq_le (u v : nat → Rbar) :
  (∀ n, Rbar_le (u n) (v n)) → Rbar_le (Sup_seq u) (Sup_seq v).
Lemma Inf_seq_le (u v : nat → Rbar) :
  (∀ n, Rbar_le (u n) (v n)) → Rbar_le (Inf_seq u) (Inf_seq v).

Lemma Inf_le_sup (u : nat → Rbar) : Rbar_le (Inf_seq u) (Sup_seq u).

Lemma is_sup_seq_major (u : nat → Rbar) (l : Rbar) (n : nat) :
  is_sup_seq u l → Rbar_le (u n) l.

Lemma Sup_seq_minor_lt (u : nat → Rbar) (M : R) :
  Rbar_lt M (Sup_seq u) ↔ ∃ n, Rbar_lt M (u n).
Lemma Sup_seq_minor_le (u : nat → Rbar) (M : R) (n : nat) :
  Rbar_le M (u n) → Rbar_le M (Sup_seq u).

Definition is_LimSup_seq (u : nat → R) (l : Rbar) :=
  match l with
    | Finite l ⇒ ∀ eps : posreal,
        (∀ N : nat, ∃ n : nat, (N ≤ n)%nat ∧ l - eps < u n)
        ∧ (∃ N : nat, ∀ n : nat, (N ≤ n)%nat → u n < l + eps)
    | p_infty ⇒ ∀ M : R, (∀ N : nat, ∃ n : nat, (N ≤ n)%nat ∧ M < u n)
    | m_infty ⇒ ∀ M : R, (∃ N : nat, ∀ n : nat, (N ≤ n)%nat → u n < M)
  end.

Definition is_LimInf_seq (u : nat → R) (l : Rbar) :=
  match l with
    | Finite l ⇒ ∀ eps : posreal,
        (∀ N : nat, ∃ n : nat, (N ≤ n)%nat ∧ u n < l + eps)
        ∧ (∃ N : nat, ∀ n : nat, (N ≤ n)%nat → l - eps < u n)
    | p_infty ⇒ ∀ M : R, (∃ N : nat, ∀ n : nat, (N ≤ n)%nat → M < u n)
    | m_infty ⇒ ∀ M : R, (∀ N : nat, ∃ n : nat, (N ≤ n)%nat ∧ u n < M)
  end.

Lemma is_LimInf_opp_LimSup_seq (u : nat → R) (l : Rbar) :
  is_LimInf_seq (fun n ⇒ - u n) (Rbar_opp l)
    ↔ is_LimSup_seq u l.
Lemma is_LimSup_opp_LimInf_seq (u : nat → R) (l : Rbar) :
  is_LimSup_seq (fun n ⇒ - u n) (Rbar_opp l)
    ↔ is_LimInf_seq u l.

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.
Lemma is_LimInf_supInf_seq (u : nat → R) (l : Rbar) :
  is_LimInf_seq u l ↔ is_sup_seq (fun m ⇒ Inf_seq (fun n ⇒ u (n + m)%nat)) l.

Lemma is_LimSup_seq_ext_loc (u v : nat → R) (l : Rbar) :
  eventually (fun n ⇒ u n = v n) →
  is_LimSup_seq u l → is_LimSup_seq v l.
Lemma is_LimSup_seq_ext (u v : nat → R) (l : Rbar) :
  (∀ n, u n = v n)
  → is_LimSup_seq u l → is_LimSup_seq v l.

Lemma is_LimInf_seq_ext_loc (u v : nat → R) (l : Rbar) :
  eventually (fun n ⇒ u n = v n) →
  is_LimInf_seq u l → is_LimInf_seq v l.
Lemma is_LimInf_seq_ext (u v : nat → R) (l : Rbar) :
  (∀ n, u n = v n)
  → is_LimInf_seq u l → is_LimInf_seq v l.

Lemma ex_LimSup_seq (u : nat → R) :
  {l : Rbar | is_LimSup_seq u l}.
Lemma ex_LimInf_seq (u : nat → R) :
  {l : Rbar | is_LimInf_seq u l}.

Definition LimSup_seq (u : nat → R) :=
  proj1_sig (ex_LimSup_seq u).
Definition LimInf_seq (u : nat → R) :=
  proj1_sig (ex_LimInf_seq u).

Lemma is_LimSup_seq_unique (u : nat → R) (l : Rbar) :
  is_LimSup_seq u l → LimSup_seq u = l.
Lemma is_LimInf_seq_unique (u : nat → R) (l : Rbar) :
  is_LimInf_seq u l → LimInf_seq u = l.

Lemma LimSup_InfSup_seq (u : nat → R) :
  LimSup_seq u = Inf_seq (fun m ⇒ Sup_seq (fun n ⇒ u (n + m)%nat)).
Lemma LimInf_SupInf_seq (u : nat → R) :
  LimInf_seq u = Sup_seq (fun m ⇒ Inf_seq (fun n ⇒ u (n + m)%nat)).

Lemma is_LimSup_LimInf_seq_le (u : nat → R) (ls li : Rbar) :
  is_LimSup_seq u ls → is_LimInf_seq u li → Rbar_le li ls.
Lemma LimSup_LimInf_seq_le (u : nat → R) :
  Rbar_le (LimInf_seq u) (LimSup_seq u).

Lemma is_LimSup_seq_const (a : R) :
  is_LimSup_seq (fun _ ⇒ a) a.
Lemma LimSup_seq_const (a : R) :
  LimSup_seq (fun _ ⇒ a) = a.

Lemma is_LimInf_seq_const (a : R) :
  is_LimInf_seq (fun _ ⇒ a) a.
Lemma LimInf_seq_const (a : R) :
  LimInf_seq (fun _ ⇒ a) = a.

Lemma LimSup_seq_opp (u : nat → R) :
  LimSup_seq (fun n ⇒ - u n) = Rbar_opp (LimInf_seq u).
Lemma LimInf_seq_opp (u : nat → R) :
  LimInf_seq (fun n ⇒ - u n) = Rbar_opp (LimSup_seq u).

Lemma LimSup_le (u v : nat → R) :
  eventually (fun n ⇒ u n ≤ v n)
  → Rbar_le (LimSup_seq u) (LimSup_seq v).
Lemma LimInf_le (u v : nat → R) :
  eventually (fun n ⇒ u n ≤ v n)
  → Rbar_le (LimInf_seq u) (LimInf_seq v).

Lemma is_LimSup_seq_scal_pos (a : R) (u : nat → R) (l : Rbar) :
  (0 < a) → is_LimSup_seq u l →
    is_LimSup_seq (fun n ⇒ a × u n) (Rbar_mult a l).
Lemma is_LimInf_seq_scal_pos (a : R) (u : nat → R) (l : Rbar) :
  (0 < a) → is_LimInf_seq u l →
    is_LimInf_seq (fun n ⇒ a × u n) (Rbar_mult a l).

Lemma is_LimSup_seq_ind_1 (u : nat → R) (l : Rbar) :
  is_LimSup_seq u l ↔
    is_LimSup_seq (fun n ⇒ u (S n)) l.
Lemma is_LimInf_seq_ind_1 (u : nat → R) (l : Rbar) :
  is_LimInf_seq u l ↔
    is_LimInf_seq (fun n ⇒ u (S n)) l.

Lemma is_LimSup_seq_ind_k (u : nat → R) (k : nat) (l : Rbar) :
  is_LimSup_seq u l ↔
    is_LimSup_seq (fun n ⇒ u (n + k)%nat) l.
Lemma is_LimInf_seq_ind_k (u : nat → R) (k : nat) (l : Rbar) :
  is_LimInf_seq u l ↔
    is_LimInf_seq (fun n ⇒ u (n + k)%nat) l.

Definition is_lim_seq (u : nat → R) (l : Rbar) :=
  filterlim u eventually (Rbar_locally l).

Definition is_lim_seq' (u : nat → R) (l : Rbar) :=
  match l with
    | Finite l ⇒ ∀ eps : posreal, eventually (fun n ⇒ Rabs (u n - l) < eps)
    | p_infty ⇒ ∀ M : R, eventually (fun n ⇒ M < u n)
    | m_infty ⇒ ∀ M : R, eventually (fun n ⇒ u n < M)
  end.
Definition ex_lim_seq (u : nat → R) :=
  ∃ l, is_lim_seq u l.
Definition ex_finite_lim_seq (u : nat → R) :=
  ∃ l : R, is_lim_seq u l.
Definition Lim_seq (u : nat → R) : Rbar :=
  Rbar_div_pos (Rbar_plus (LimSup_seq u) (LimInf_seq u))
    {| pos := 2; cond_pos := Rlt_R0_R2 |}.

Lemma is_lim_seq_spec :
  ∀ u l,
  is_lim_seq' u l ↔ is_lim_seq u l.

Lemma is_lim_seq_Reals (u : nat → R) (l : R) :
  is_lim_seq u l ↔ Un_cv u l.
Lemma is_lim_seq_p_infty_Reals (u : nat → R) :
  is_lim_seq u p_infty ↔ cv_infty u.

Lemma is_lim_LimSup_seq (u : nat → R) (l : Rbar) :
  is_lim_seq u l → is_LimSup_seq u l.
Lemma is_lim_LimInf_seq (u : nat → R) (l : Rbar) :
  is_lim_seq u l → is_LimInf_seq u l.
Lemma is_LimSup_LimInf_lim_seq (u : nat → R) (l : Rbar) :
  is_LimSup_seq u l → is_LimInf_seq u l → is_lim_seq u l.

Lemma ex_lim_LimSup_LimInf_seq (u : nat → R) :
  ex_lim_seq u ↔ LimSup_seq u = LimInf_seq u.

Lemma is_lim_seq_ext_loc (u v : nat → R) (l : Rbar) :
  eventually (fun n ⇒ u n = v n) →
  is_lim_seq u l → is_lim_seq v l.
Lemma ex_lim_seq_ext_loc (u v : nat → R) :
  eventually (fun n ⇒ u n = v n) →
  ex_lim_seq u → ex_lim_seq v.
Lemma Lim_seq_ext_loc (u v : nat → R) :
  eventually (fun n ⇒ u n = v n) →
  Lim_seq u = Lim_seq v.

Lemma is_lim_seq_ext (u v : nat → R) (l : Rbar) :
  (∀ n, u n = v n) → is_lim_seq u l → is_lim_seq v l.
Lemma ex_lim_seq_ext (u v : nat → R) :
  (∀ n, u n = v n) → ex_lim_seq u → ex_lim_seq v.
Lemma Lim_seq_ext (u v : nat → R) :
  (∀ n, u n = v n) →
  Lim_seq u = Lim_seq v.

Lemma is_lim_seq_unique (u : nat → R) (l : Rbar) :
  is_lim_seq u l → Lim_seq u = l.
Lemma Lim_seq_correct (u : nat → R) :
  ex_lim_seq u → is_lim_seq u (Lim_seq u).
Lemma Lim_seq_correct' (u : nat → R) :
  ex_finite_lim_seq u → is_lim_seq u (real (Lim_seq u)).

Lemma ex_finite_lim_seq_correct (u : nat → R) :
  ex_finite_lim_seq u ↔ ex_lim_seq u ∧ is_finite (Lim_seq u).

Lemma ex_lim_seq_dec (u : nat → R) :
  {ex_lim_seq u} + {¬ex_lim_seq u}.

Lemma ex_finite_lim_seq_dec (u : nat → R) :
  {ex_finite_lim_seq u} + {¬ ex_finite_lim_seq u}.

Definition ex_lim_seq_cauchy (u : nat → R) :=
  ∀ eps : posreal, ∃ N : nat, ∀ n m,
    (N ≤ n)%nat → (N ≤ m)%nat → Rabs (u n - u m) < eps.
Lemma ex_lim_seq_cauchy_corr (u : nat → R) :
  (ex_finite_lim_seq u) ↔ ex_lim_seq_cauchy u.

Lemma is_lim_seq_INR :
  is_lim_seq INR p_infty.
Lemma ex_lim_seq_INR :
  ex_lim_seq INR.
Lemma Lim_seq_INR :
  Lim_seq INR = p_infty.

Lemma is_lim_seq_const (a : R) :
  is_lim_seq (fun n ⇒ a) a.
Lemma ex_lim_seq_const (a : R) :
  ex_lim_seq (fun n ⇒ a).
Lemma Lim_seq_const (a : R) :
  Lim_seq (fun n ⇒ a) = a.

Lemma eventually_subseq_loc :
  ∀ phi,
  eventually (fun n ⇒ (phi n < phi (S n))%nat) →
  filterlim phi eventually eventually.
Lemma eventually_subseq :
  ∀ phi,
  (∀ n, (phi n < phi (S n))%nat) →
  filterlim phi eventually eventually.

Lemma is_lim_seq_subseq (u : nat → R) (l : Rbar) (phi : nat → nat) :
  filterlim phi eventually eventually →
  is_lim_seq u l →
  is_lim_seq (fun n ⇒ u (phi n)) l.
Lemma ex_lim_seq_subseq (u : nat → R) (phi : nat → nat) :
  filterlim phi eventually eventually →
  ex_lim_seq u →
  ex_lim_seq (fun n ⇒ u (phi n)).
Lemma Lim_seq_subseq (u : nat → R) (phi : nat → nat) :
  filterlim phi eventually eventually →
  ex_lim_seq u →
  Lim_seq (fun n ⇒ u (phi n)) = Lim_seq u.

Lemma is_lim_seq_incr_1 (u : nat → R) (l : Rbar) :
  is_lim_seq u l ↔ is_lim_seq (fun n ⇒ u (S n)) l.
Lemma ex_lim_seq_incr_1 (u : nat → R) :
  ex_lim_seq u ↔ ex_lim_seq (fun n ⇒ u (S n)).
Lemma Lim_seq_incr_1 (u : nat → R) :
  Lim_seq (fun n ⇒ u (S n)) = Lim_seq u.

Lemma is_lim_seq_incr_n (u : nat → R) (N : nat) (l : Rbar) :
  is_lim_seq u l ↔ is_lim_seq (fun n ⇒ u (n + N)%nat) l.
Lemma ex_lim_seq_incr_n (u : nat → R) (N : nat) :
  ex_lim_seq u ↔ ex_lim_seq (fun n ⇒ u (n + N)%nat).
Lemma Lim_seq_incr_n (u : nat → R) (N : nat) :
  Lim_seq (fun n ⇒ u (n + N)%nat) = Lim_seq u.

Lemma filterlim_le :
  ∀ {T F} {FF : ProperFilter' F} (f g : T → R) (lf lg : Rbar),
  F (fun x ⇒ f x ≤ g x) →
  filterlim f F (Rbar_locally lf) →
  filterlim g F (Rbar_locally lg) →
  Rbar_le lf lg.

Lemma is_lim_seq_le_loc (u v : nat → R) (l1 l2 : Rbar) :
  eventually (fun n ⇒ u n ≤ v n) →
  is_lim_seq u l1 → is_lim_seq v l2 →
  Rbar_le l1 l2.
Lemma Lim_seq_le_loc (u v : nat → R) :
  eventually (fun n ⇒ u n ≤ v n) →
  Rbar_le (Lim_seq u) (Lim_seq v).

Lemma is_lim_seq_le (u v : nat → R) (l1 l2 : Rbar) :
  (∀ n, u n ≤ v n) → is_lim_seq u l1 → is_lim_seq v l2 → Rbar_le l1 l2.

Lemma filterlim_ge_p_infty :
  ∀ {T F} {FF : Filter F} (f g : T → R),
  F (fun x ⇒ f x ≤ g x) →
  filterlim f F (Rbar_locally p_infty) →
  filterlim g F (Rbar_locally p_infty).

Lemma filterlim_le_m_infty :
  ∀ {T F} {FF : Filter F} (f g : T → R),
  F (fun x ⇒ g x ≤ f x) →
  filterlim f F (Rbar_locally m_infty) →
  filterlim g F (Rbar_locally m_infty).

Lemma filterlim_le_le :
  ∀ {T F} {FF : Filter F} (f g h : T → R) (l : Rbar),
  F (fun x ⇒ f x ≤ g x ≤ h x) →
  filterlim f F (Rbar_locally l) →
  filterlim h F (Rbar_locally l) →
  filterlim g F (Rbar_locally l).

Lemma is_lim_seq_le_le_loc (u v w : nat → R) (l : Rbar) :
  eventually (fun n ⇒ u n ≤ v n ≤ w n) → is_lim_seq u l → is_lim_seq w l → is_lim_seq v l.

Lemma is_lim_seq_le_le (u v w : nat → R) (l : Rbar) :
  (∀ n, u n ≤ v n ≤ w n) → is_lim_seq u l → is_lim_seq w l → is_lim_seq v l.

Lemma is_lim_seq_le_p_loc (u v : nat → R) :
  eventually (fun n ⇒ u n ≤ v n) →
  is_lim_seq u p_infty →
  is_lim_seq v p_infty.

Lemma is_lim_seq_le_m_loc (u v : nat → R) :
  eventually (fun n ⇒ v n ≤ u n) →
  is_lim_seq u m_infty →
  is_lim_seq v m_infty.

Lemma is_lim_seq_decr_compare (u : nat → R) (l : R) :
  is_lim_seq u l
  → (∀ n, (u (S n)) ≤ (u n))
  → ∀ n, l ≤ u n.
Lemma is_lim_seq_incr_compare (u : nat → R) (l : R) :
  is_lim_seq u l
  → (∀ n, (u n) ≤ (u (S n)))
  → ∀ n, u n ≤ l.

Lemma ex_lim_seq_decr (u : nat → R) :
  (∀ n, (u (S n)) ≤ (u n))
    → ex_lim_seq u.
Lemma ex_lim_seq_incr (u : nat → R) :
  (∀ n, (u n) ≤ (u (S n)))
    → ex_lim_seq u.

Lemma ex_finite_lim_seq_decr (u : nat → R) (M : R) :
  (∀ n, (u (S n)) ≤ (u n)) → (∀ n, M ≤ u n)
    → ex_finite_lim_seq u.
Lemma ex_finite_lim_seq_incr (u : nat → R) (M : R) :
  (∀ n, (u n) ≤ (u (S n))) → (∀ n, u n ≤ M)
    → ex_finite_lim_seq u.

Lemma filterlim_Rbar_opp :
  ∀ x,
  filterlim Ropp (Rbar_locally x) (Rbar_locally (Rbar_opp x)).

Lemma is_lim_seq_opp (u : nat → R) (l : Rbar) :
  is_lim_seq u l ↔ is_lim_seq (fun n ⇒ -u n) (Rbar_opp l).

Lemma ex_lim_seq_opp (u : nat → R) :
  ex_lim_seq u ↔ ex_lim_seq (fun n ⇒ -u n).

Lemma Lim_seq_opp (u : nat → R) :
  Lim_seq (fun n ⇒ - u n) = Rbar_opp (Lim_seq u).

Lemma filterlim_Rbar_plus :
  ∀ x y z,
  is_Rbar_plus x y z →
  filterlim (fun z ⇒ fst z + snd z) (filter_prod (Rbar_locally x) (Rbar_locally y)) (Rbar_locally z).

Lemma is_lim_seq_plus (u v : nat → R) (l1 l2 l : Rbar) :
  is_lim_seq u l1 → is_lim_seq v l2 →
  is_Rbar_plus l1 l2 l →
  is_lim_seq (fun n ⇒ u n + v n) l.
Lemma is_lim_seq_plus' (u v : nat → R) (l1 l2 : R) :
  is_lim_seq u l1 → is_lim_seq v l2 →
  is_lim_seq (fun n ⇒ u n + v n) (l1 + l2).

Lemma ex_lim_seq_plus (u v : nat → R) :
  ex_lim_seq u → ex_lim_seq v →
  ex_Rbar_plus (Lim_seq u) (Lim_seq v) →
  ex_lim_seq (fun n ⇒ u n + v n).

Lemma Lim_seq_plus (u v : nat → R) :
  ex_lim_seq u → ex_lim_seq v →
  ex_Rbar_plus (Lim_seq u) (Lim_seq v) →
  Lim_seq (fun n ⇒ u n + v n) = Rbar_plus (Lim_seq u) (Lim_seq v).

Lemma is_lim_seq_minus (u v : nat → R) (l1 l2 l : Rbar) :
  is_lim_seq u l1 → is_lim_seq v l2 →
  is_Rbar_minus l1 l2 l →
  is_lim_seq (fun n ⇒ u n - v n) l.
Lemma is_lim_seq_minus' (u v : nat → R) (l1 l2 : R) :
  is_lim_seq u l1 → is_lim_seq v l2 →
  is_lim_seq (fun n ⇒ u n - v n) (l1 - l2).

Lemma ex_lim_seq_minus (u v : nat → R) :
  ex_lim_seq u → ex_lim_seq v →
  ex_Rbar_minus (Lim_seq u) (Lim_seq v) →
  ex_lim_seq (fun n ⇒ u n - v n).

Lemma Lim_seq_minus (u v : nat → R) :
  ex_lim_seq u → ex_lim_seq v →
  ex_Rbar_minus (Lim_seq u) (Lim_seq v) →
  Lim_seq (fun n ⇒ u n - v n) = Rbar_minus (Lim_seq u) (Lim_seq v).

Lemma filterlim_Rbar_inv :
  ∀ l : Rbar, l ≠ 0 →
  filterlim Rinv (Rbar_locally l) (Rbar_locally (Rbar_inv l)).

Lemma is_lim_seq_inv (u : nat → R) (l : Rbar) :
  is_lim_seq u l → l ≠ 0 →
  is_lim_seq (fun n ⇒ / u n) (Rbar_inv l).

Lemma ex_lim_seq_inv (u : nat → R) :
  ex_lim_seq u
  → Lim_seq u ≠ 0
    → ex_lim_seq (fun n ⇒ / u n).

Lemma Lim_seq_inv (u : nat → R) :
  ex_lim_seq u → (Lim_seq u ≠ 0)
    → Lim_seq (fun n ⇒ / u n) = Rbar_inv (Lim_seq u).

Lemma filterlim_Rbar_mult :
  ∀ x y z,
  is_Rbar_mult x y z →
  filterlim (fun z ⇒ fst z × snd z) (filter_prod (Rbar_locally x) (Rbar_locally y)) (Rbar_locally z).

Lemma is_lim_seq_mult (u v : nat → R) (l1 l2 l : Rbar) :
  is_lim_seq u l1 → is_lim_seq v l2 →
  is_Rbar_mult l1 l2 l →
  is_lim_seq (fun n ⇒ u n × v n) l.
Lemma is_lim_seq_mult' (u v : nat → R) (l1 l2 : R) :
  is_lim_seq u l1 → is_lim_seq v l2 →
  is_lim_seq (fun n ⇒ u n × v n) (l1 × l2).

Lemma ex_lim_seq_mult (u v : nat → R) :
  ex_lim_seq u → ex_lim_seq v →
  ex_Rbar_mult (Lim_seq u) (Lim_seq v) →
  ex_lim_seq (fun n ⇒ u n × v n).

Lemma Lim_seq_mult (u v : nat → R) :
  ex_lim_seq u → ex_lim_seq v →
  ex_Rbar_mult (Lim_seq u) (Lim_seq v) →
  Lim_seq (fun n ⇒ u n × v n) = Rbar_mult (Lim_seq u) (Lim_seq v).

Lemma filterlim_Rbar_mult_l :
  ∀ (a : R) (l : Rbar),
  filterlim (Rmult a) (Rbar_locally l) (Rbar_locally (Rbar_mult a l)).

Lemma filterlim_Rbar_mult_r :
  ∀ (a : R) (l : Rbar),
  filterlim (fun x ⇒ Rmult x a) (Rbar_locally l) (Rbar_locally (Rbar_mult l a)).

Lemma is_lim_seq_scal_l (u : nat → R) (a : R) (lu : Rbar) :
  is_lim_seq u lu →
  is_lim_seq (fun n ⇒ a × u n) (Rbar_mult a lu).

Lemma ex_lim_seq_scal_l (u : nat → R) (a : R) :
  ex_lim_seq u → ex_lim_seq (fun n ⇒ a × u n).

Lemma Lim_seq_scal_l (u : nat → R) (a : R) :
  Lim_seq (fun n ⇒ a × u n) = Rbar_mult a (Lim_seq u).

Lemma is_lim_seq_scal_r (u : nat → R) (a : R) (lu : Rbar) :
  is_lim_seq u lu →
    is_lim_seq (fun n ⇒ u n × a) (Rbar_mult lu a).

Lemma ex_lim_seq_scal_r (u : nat → R) (a : R) :
  ex_lim_seq u → ex_lim_seq (fun n ⇒ u n × a).

Lemma Lim_seq_scal_r (u : nat → R) (a : R) :
  Lim_seq (fun n ⇒ u n × a) = Rbar_mult (Lim_seq u) a.

Lemma is_lim_seq_div (u v : nat → R) (l1 l2 l : Rbar) :
  is_lim_seq u l1 → is_lim_seq v l2 → l2 ≠ 0 →
  is_Rbar_div l1 l2 l →
  is_lim_seq (fun n ⇒ u n / v n) l.
Lemma is_lim_seq_div' (u v : nat → R) (l1 l2 : R) :
  is_lim_seq u l1 → is_lim_seq v l2 → l2 ≠ 0 →
  is_lim_seq (fun n ⇒ u n / v n) (l1 / l2).
Lemma ex_lim_seq_div (u v : nat → R) :
  ex_lim_seq u → ex_lim_seq v → Lim_seq v ≠ 0 →
  ex_Rbar_div (Lim_seq u) (Lim_seq v) →
  ex_lim_seq (fun n ⇒ u n / v n).
Lemma Lim_seq_div (u v : nat → R) :
  ex_lim_seq u → ex_lim_seq v → (Lim_seq v ≠ 0) →
  ex_Rbar_div (Lim_seq u) (Lim_seq v) →
  Lim_seq (fun n ⇒ u n / v n) = Rbar_div (Lim_seq u) (Lim_seq v).

Lemma ex_lim_seq_adj (u v : nat → R) :
  (∀ n, u n ≤ u (S n)) → (∀ n, v (S n) ≤ v n)
  → is_lim_seq (fun n ⇒ v n - u n) 0
  → ex_finite_lim_seq u ∧ ex_finite_lim_seq v ∧ Lim_seq u = Lim_seq v.

Lemma is_lim_seq_continuous (f : R → R) (u : nat → R) (l : R) :
  continuity_pt f l → is_lim_seq u l
  → is_lim_seq (fun n ⇒ f (u n)) (f l).

Lemma filterlim_Rabs :
  ∀ l : Rbar,
  filterlim Rabs (Rbar_locally l) (Rbar_locally (Rbar_abs l)).

Lemma is_lim_seq_abs (u : nat → R) (l : Rbar) :
  is_lim_seq u l → is_lim_seq (fun n ⇒ Rabs (u n)) (Rbar_abs l).
Lemma ex_lim_seq_abs (u : nat → R) :
  ex_lim_seq u → ex_lim_seq (fun n ⇒ Rabs (u n)).
Lemma Lim_seq_abs (u : nat → R) :
  ex_lim_seq u →
  Lim_seq (fun n ⇒ Rabs (u n)) = Rbar_abs (Lim_seq u).

Lemma is_lim_seq_abs_0 (u : nat → R) :
  is_lim_seq u 0 ↔ is_lim_seq (fun n ⇒ Rabs (u n)) 0.