Library Coquelicot.Lim_seq

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Require Import Reals Ssreflect.ssreflect.
Require Import Rcomplements.
Require Import Rbar Lub Markov Hierarchy.

This file describes properties and definitions about limits of real sequences. This includes properties about the predicates is_lim_seq and ex_lim_seq. This file also defines several total functions using the Limited Principle of Omniscience. These total functions on R sequences are Sup_seq, Inf_seq, LimSup_seq, LimInf_seq and of course Lim_seq.

Open Scope R_scope.

Sup and Inf of sequences in Rbar

Definitions


Definition is_sup_seq (u : natRbar) (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 : natRbar) (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.

Equivalent forms

Lemma is_inf_opp_sup_seq (u : natRbar) (l : Rbar) :
  is_inf_seq (fun nRbar_opp (u n)) (Rbar_opp l)
   is_sup_seq u l.
Lemma is_sup_opp_inf_seq (u : natRbar) (l : Rbar) :
  is_sup_seq (fun nRbar_opp (u n)) (Rbar_opp l)
   is_inf_seq u l.

Lemma is_sup_seq_lub (u : natRbar) (l : Rbar) :
  is_sup_seq u lRbar_is_lub (fun x n, x = u n) l.

Lemma Rbar_is_lub_sup_seq (u : natRbar) (l : Rbar) :
  Rbar_is_lub (fun x n, x = u n) lis_sup_seq u l.

Lemma is_inf_seq_glb (u : natRbar) (l : Rbar) :
  is_inf_seq u lRbar_is_glb (fun x n, x = u n) l.
Lemma Rbar_is_glb_inf_seq (u : natRbar) (l : Rbar) :
  Rbar_is_glb (fun x n, x = u n) lis_inf_seq u l.

Extensionality

Lemma is_sup_seq_ext (u v : natRbar) (l : Rbar) :
  ( n, u n = v n)
  → is_sup_seq u lis_sup_seq v l.
Lemma is_inf_seq_ext (u v : natRbar) (l : Rbar) :
  ( n, u n = v n)
  → is_inf_seq u lis_inf_seq v l.

Existence

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

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

Notations

Definition Sup_seq (u : natRbar) := proj1_sig (ex_sup_seq u).

Definition Inf_seq (u : natRbar) := proj1_sig (ex_inf_seq u).

Lemma is_sup_seq_unique (u : natRbar) (l : Rbar) :
  is_sup_seq u lSup_seq u = l.
Lemma Sup_seq_correct (u : natRbar) :
  is_sup_seq u (Sup_seq u).
Lemma is_inf_seq_unique (u : natRbar) (l : Rbar) :
  is_inf_seq u lInf_seq u = l.
Lemma Inf_seq_correct (u : natRbar) :
  is_inf_seq u (Inf_seq u).

Lemma Sup_seq_ext (u v : natRbar) :
  ( n, (u n) = (v n)) → Sup_seq u = Sup_seq v.
Lemma Inf_seq_ext (u v : natRbar) :
  ( n, (u n) = (v n)) → Inf_seq u = Inf_seq v.

Lemma Rbar_sup_eq_lub (u : natRbar) :
  Sup_seq u = Rbar_lub (fun x n, x = u n).
Lemma Inf_eq_glb (u : natRbar) :
  Inf_seq u = Rbar_glb (fun x n, x = u n).

Lemma Sup_opp_inf (u : natRbar) :
  Sup_seq u = Rbar_opp (Inf_seq (fun nRbar_opp (u n))).
Lemma Inf_opp_sup (u : natRbar) :
  Inf_seq u = Rbar_opp (Sup_seq (fun nRbar_opp (u n))).

Lemma Sup_seq_scal_l (a : R) (u : natRbar) : 0 a
  Sup_seq (fun nRbar_mult a (u n)) = Rbar_mult a (Sup_seq u).
Lemma Inf_seq_scal_l (a : R) (u : natRbar) : 0 a
  Inf_seq (fun nRbar_mult a (u n)) = Rbar_mult a (Inf_seq u).

Order


Lemma is_sup_seq_le (u v : natRbar) {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 : natRbar) {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 : natRbar) :
  ( n, Rbar_le (u n) (v n)) → Rbar_le (Sup_seq u) (Sup_seq v).
Lemma Inf_seq_le (u v : natRbar) :
  ( n, Rbar_le (u n) (v n)) → Rbar_le (Inf_seq u) (Inf_seq v).

Lemma Inf_le_sup (u : natRbar) : Rbar_le (Inf_seq u) (Sup_seq u).

Lemma is_sup_seq_major (u : natRbar) (l : Rbar) (n : nat) :
  is_sup_seq u lRbar_le (u n) l.

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

LimSup and LimInf of sequences

Definitions


Definition is_LimSup_seq (u : natR) (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)%natu 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)%natu n < M)
  end.

Definition is_LimInf_seq (u : natR) (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)%natl - eps < u n)
    | p_infty M : R, ( N : nat, n : nat, (N n)%natM < u n)
    | m_infty M : R, ( N : nat, n : nat, (N n)%nat u n < M)
  end.

Equivalent forms

Lemma is_LimInf_opp_LimSup_seq (u : natR) (l : Rbar) :
  is_LimInf_seq (fun n- u n) (Rbar_opp l)
     is_LimSup_seq u l.
Lemma is_LimSup_opp_LimInf_seq (u : natR) (l : Rbar) :
  is_LimSup_seq (fun n- u n) (Rbar_opp l)
     is_LimInf_seq u l.

Lemma is_LimSup_infSup_seq (u : natR) (l : Rbar) :
  is_LimSup_seq u l is_inf_seq (fun mSup_seq (fun nu (n + m)%nat)) l.
Lemma is_LimInf_supInf_seq (u : natR) (l : Rbar) :
  is_LimInf_seq u l is_sup_seq (fun mInf_seq (fun nu (n + m)%nat)) l.

Extensionality

Lemma is_LimSup_seq_ext_loc (u v : natR) (l : Rbar) :
  eventually (fun nu n = v n) →
  is_LimSup_seq u lis_LimSup_seq v l.
Lemma is_LimSup_seq_ext (u v : natR) (l : Rbar) :
  ( n, u n = v n)
  → is_LimSup_seq u lis_LimSup_seq v l.

Lemma is_LimInf_seq_ext_loc (u v : natR) (l : Rbar) :
  eventually (fun nu n = v n) →
  is_LimInf_seq u lis_LimInf_seq v l.
Lemma is_LimInf_seq_ext (u v : natR) (l : Rbar) :
  ( n, u n = v n)
  → is_LimInf_seq u lis_LimInf_seq v l.

Existence

Lemma ex_LimSup_seq (u : natR) :
  {l : Rbar | is_LimSup_seq u l}.
Lemma ex_LimInf_seq (u : natR) :
  {l : Rbar | is_LimInf_seq u l}.

Functions

Definition LimSup_seq (u : natR) :=
  proj1_sig (ex_LimSup_seq u).
Definition LimInf_seq (u : natR) :=
  proj1_sig (ex_LimInf_seq u).

Uniqueness

Lemma is_LimSup_seq_unique (u : natR) (l : Rbar) :
  is_LimSup_seq u lLimSup_seq u = l.
Lemma is_LimInf_seq_unique (u : natR) (l : Rbar) :
  is_LimInf_seq u lLimInf_seq u = l.

Lemma LimSup_InfSup_seq (u : natR) :
  LimSup_seq u = Inf_seq (fun mSup_seq (fun nu (n + m)%nat)).
Lemma LimInf_SupInf_seq (u : natR) :
  LimInf_seq u = Sup_seq (fun mInf_seq (fun nu (n + m)%nat)).

Operations and order


Lemma is_LimSup_LimInf_seq_le (u : natR) (ls li : Rbar) :
  is_LimSup_seq u lsis_LimInf_seq u liRbar_le li ls.
Lemma LimSup_LimInf_seq_le (u : natR) :
  Rbar_le (LimInf_seq u) (LimSup_seq u).

Constant

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.

Opposite

Lemma LimSup_seq_opp (u : natR) :
  LimSup_seq (fun n- u n) = Rbar_opp (LimInf_seq u).
Lemma LimInf_seq_opp (u : natR) :
  LimInf_seq (fun n- u n) = Rbar_opp (LimSup_seq u).

Rbar_le

Lemma LimSup_le (u v : natR) :
  eventually (fun nu n v n)
  → Rbar_le (LimSup_seq u) (LimSup_seq v).
Lemma LimInf_le (u v : natR) :
  eventually (fun nu n v n)
  → Rbar_le (LimInf_seq u) (LimInf_seq v).

Scalar multplication

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

Index shifting

Lemma is_LimSup_seq_ind_1 (u : natR) (l : Rbar) :
  is_LimSup_seq u l
    is_LimSup_seq (fun nu (S n)) l.
Lemma is_LimInf_seq_ind_1 (u : natR) (l : Rbar) :
  is_LimInf_seq u l
    is_LimInf_seq (fun nu (S n)) l.

Lemma is_LimSup_seq_ind_k (u : natR) (k : nat) (l : Rbar) :
  is_LimSup_seq u l
    is_LimSup_seq (fun nu (n + k)%nat) l.
Lemma is_LimInf_seq_ind_k (u : natR) (k : nat) (l : Rbar) :
  is_LimInf_seq u l
    is_LimInf_seq (fun nu (n + k)%nat) l.

Limit of sequences

Definition


Definition is_lim_seq (u : natR) (l : Rbar) :=
  filterlim u eventually (Rbar_locally l).

Definition is_lim_seq' (u : natR) (l : Rbar) :=
  match l with
    | Finite l eps : posreal, eventually (fun nRabs (u n - l) < eps)
    | p_infty M : R, eventually (fun nM < u n)
    | m_infty M : R, eventually (fun nu n < M)
  end.
Definition ex_lim_seq (u : natR) :=
   l, is_lim_seq u l.
Definition ex_finite_lim_seq (u : natR) :=
   l : R, is_lim_seq u l.
Definition Lim_seq (u : natR) : 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.

Equivalence with standard library Reals

Lemma is_lim_seq_Reals (u : natR) (l : R) :
  is_lim_seq u l Un_cv u l.
Lemma is_lim_seq_p_infty_Reals (u : natR) :
  is_lim_seq u p_infty cv_infty u.

Lemma is_lim_LimSup_seq (u : natR) (l : Rbar) :
  is_lim_seq u lis_LimSup_seq u l.
Lemma is_lim_LimInf_seq (u : natR) (l : Rbar) :
  is_lim_seq u lis_LimInf_seq u l.
Lemma is_LimSup_LimInf_lim_seq (u : natR) (l : Rbar) :
  is_LimSup_seq u lis_LimInf_seq u lis_lim_seq u l.

Lemma ex_lim_LimSup_LimInf_seq (u : natR) :
  ex_lim_seq u LimSup_seq u = LimInf_seq u.

Extensionality

Lemma is_lim_seq_ext_loc (u v : natR) (l : Rbar) :
  eventually (fun nu n = v n) →
  is_lim_seq u lis_lim_seq v l.
Lemma ex_lim_seq_ext_loc (u v : natR) :
  eventually (fun nu n = v n) →
  ex_lim_seq uex_lim_seq v.
Lemma Lim_seq_ext_loc (u v : natR) :
  eventually (fun nu n = v n) →
  Lim_seq u = Lim_seq v.

Lemma is_lim_seq_ext (u v : natR) (l : Rbar) :
  ( n, u n = v n) → is_lim_seq u lis_lim_seq v l.
Lemma ex_lim_seq_ext (u v : natR) :
  ( n, u n = v n) → ex_lim_seq uex_lim_seq v.
Lemma Lim_seq_ext (u v : natR) :
  ( n, u n = v n) →
  Lim_seq u = Lim_seq v.

Unicity

Lemma is_lim_seq_unique (u : natR) (l : Rbar) :
  is_lim_seq u lLim_seq u = l.
Lemma Lim_seq_correct (u : natR) :
  ex_lim_seq uis_lim_seq u (Lim_seq u).
Lemma Lim_seq_correct' (u : natR) :
  ex_finite_lim_seq uis_lim_seq u (real (Lim_seq u)).

Lemma ex_finite_lim_seq_correct (u : natR) :
  ex_finite_lim_seq u ex_lim_seq u is_finite (Lim_seq u).

Lemma ex_lim_seq_dec (u : natR) :
  {ex_lim_seq u} + {¬ex_lim_seq u}.

Lemma ex_finite_lim_seq_dec (u : natR) :
  {ex_finite_lim_seq u} + {¬ ex_finite_lim_seq u}.

Definition ex_lim_seq_cauchy (u : natR) :=
   eps : posreal, N : nat, n m,
    (N n)%nat → (N m)%natRabs (u n - u m) < eps.
Lemma ex_lim_seq_cauchy_corr (u : natR) :
  (ex_finite_lim_seq u) ex_lim_seq_cauchy u.

Arithmetic operations and order

Identity
Constants

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

Subsequences

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 : natR) (l : Rbar) (phi : natnat) :
  filterlim phi eventually eventually
  is_lim_seq u l
  is_lim_seq (fun nu (phi n)) l.
Lemma ex_lim_seq_subseq (u : natR) (phi : natnat) :
  filterlim phi eventually eventually
  ex_lim_seq u
  ex_lim_seq (fun nu (phi n)).
Lemma Lim_seq_subseq (u : natR) (phi : natnat) :
  filterlim phi eventually eventually
  ex_lim_seq u
  Lim_seq (fun nu (phi n)) = Lim_seq u.

Lemma is_lim_seq_incr_1 (u : natR) (l : Rbar) :
  is_lim_seq u l is_lim_seq (fun nu (S n)) l.
Lemma ex_lim_seq_incr_1 (u : natR) :
  ex_lim_seq u ex_lim_seq (fun nu (S n)).
Lemma Lim_seq_incr_1 (u : natR) :
  Lim_seq (fun nu (S n)) = Lim_seq u.

Lemma is_lim_seq_incr_n (u : natR) (N : nat) (l : Rbar) :
  is_lim_seq u l is_lim_seq (fun nu (n + N)%nat) l.
Lemma ex_lim_seq_incr_n (u : natR) (N : nat) :
  ex_lim_seq u ex_lim_seq (fun nu (n + N)%nat).
Lemma Lim_seq_incr_n (u : natR) (N : nat) :
  Lim_seq (fun nu (n + N)%nat) = Lim_seq u.

Order


Lemma filterlim_le :
   {T F} {FF : ProperFilter' F} (f g : TR) (lf lg : Rbar),
  F (fun xf 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 : natR) (l1 l2 : Rbar) :
  eventually (fun nu n v n) →
  is_lim_seq u l1is_lim_seq v l2
  Rbar_le l1 l2.
Lemma Lim_seq_le_loc (u v : natR) :
  eventually (fun nu n v n) →
  Rbar_le (Lim_seq u) (Lim_seq v).

Lemma is_lim_seq_le (u v : natR) (l1 l2 : Rbar) :
  ( n, u n v n) → is_lim_seq u l1is_lim_seq v l2Rbar_le l1 l2.

Lemma filterlim_ge_p_infty :
   {T F} {FF : Filter F} (f g : TR),
  F (fun xf 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 : TR),
  F (fun xg 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 : TR) (l : Rbar),
  F (fun xf 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 : natR) (l : Rbar) :
  eventually (fun nu n v n w n) → is_lim_seq u lis_lim_seq w lis_lim_seq v l.

Lemma is_lim_seq_le_le (u v w : natR) (l : Rbar) :
  ( n, u n v n w n) → is_lim_seq u lis_lim_seq w lis_lim_seq v l.

Lemma is_lim_seq_le_p_loc (u v : natR) :
  eventually (fun nu n v n) →
  is_lim_seq u p_infty
  is_lim_seq v p_infty.

Lemma is_lim_seq_le_m_loc (u v : natR) :
  eventually (fun nv n u n) →
  is_lim_seq u m_infty
  is_lim_seq v m_infty.

Lemma is_lim_seq_decr_compare (u : natR) (l : R) :
  is_lim_seq u l
  → ( n, (u (S n)) (u n))
  → n, l u n.
Lemma is_lim_seq_incr_compare (u : natR) (l : R) :
  is_lim_seq u l
  → ( n, (u n) (u (S n)))
  → n, u n l.

Lemma ex_lim_seq_decr (u : natR) :
  ( n, (u (S n)) (u n))
    → ex_lim_seq u.
Lemma ex_lim_seq_incr (u : natR) :
  ( n, (u n) (u (S n)))
    → ex_lim_seq u.

Lemma ex_finite_lim_seq_decr (u : natR) (M : R) :
  ( n, (u (S n)) (u n)) → ( n, M u n)
    → ex_finite_lim_seq u.
Lemma ex_finite_lim_seq_incr (u : natR) (M : R) :
  ( n, (u n) (u (S n))) → ( n, u n M)
    → ex_finite_lim_seq u.

Additive operators

Opposite

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

Lemma is_lim_seq_opp (u : natR) (l : Rbar) :
  is_lim_seq u l is_lim_seq (fun n-u n) (Rbar_opp l).

Lemma ex_lim_seq_opp (u : natR) :
  ex_lim_seq u ex_lim_seq (fun n-u n).

Lemma Lim_seq_opp (u : natR) :
  Lim_seq (fun n- u n) = Rbar_opp (Lim_seq u).

Addition

Lemma filterlim_Rbar_plus :
   x y z,
  is_Rbar_plus x y z
  filterlim (fun zfst z + snd z) (filter_prod (Rbar_locally x) (Rbar_locally y)) (Rbar_locally z).

Lemma is_lim_seq_plus (u v : natR) (l1 l2 l : Rbar) :
  is_lim_seq u l1is_lim_seq v l2
  is_Rbar_plus l1 l2 l
  is_lim_seq (fun nu n + v n) l.
Lemma is_lim_seq_plus' (u v : natR) (l1 l2 : R) :
  is_lim_seq u l1is_lim_seq v l2
  is_lim_seq (fun nu n + v n) (l1 + l2).

Lemma ex_lim_seq_plus (u v : natR) :
  ex_lim_seq uex_lim_seq v
  ex_Rbar_plus (Lim_seq u) (Lim_seq v) →
  ex_lim_seq (fun nu n + v n).

Lemma Lim_seq_plus (u v : natR) :
  ex_lim_seq uex_lim_seq v
  ex_Rbar_plus (Lim_seq u) (Lim_seq v) →
  Lim_seq (fun nu n + v n) = Rbar_plus (Lim_seq u) (Lim_seq v).

Subtraction

Lemma is_lim_seq_minus (u v : natR) (l1 l2 l : Rbar) :
  is_lim_seq u l1is_lim_seq v l2
  is_Rbar_minus l1 l2 l
  is_lim_seq (fun nu n - v n) l.
Lemma is_lim_seq_minus' (u v : natR) (l1 l2 : R) :
  is_lim_seq u l1is_lim_seq v l2
  is_lim_seq (fun nu n - v n) (l1 - l2).

Lemma ex_lim_seq_minus (u v : natR) :
  ex_lim_seq uex_lim_seq v
  ex_Rbar_minus (Lim_seq u) (Lim_seq v) →
  ex_lim_seq (fun nu n - v n).

Lemma Lim_seq_minus (u v : natR) :
  ex_lim_seq uex_lim_seq v
  ex_Rbar_minus (Lim_seq u) (Lim_seq v) →
  Lim_seq (fun nu n - v n) = Rbar_minus (Lim_seq u) (Lim_seq v).

Multiplicative operators

Inverse

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

Lemma is_lim_seq_inv (u : natR) (l : Rbar) :
  is_lim_seq u ll 0 →
  is_lim_seq (fun n/ u n) (Rbar_inv l).

Lemma ex_lim_seq_inv (u : natR) :
  ex_lim_seq u
  → Lim_seq u 0
    → ex_lim_seq (fun n/ u n).

Lemma Lim_seq_inv (u : natR) :
  ex_lim_seq u → (Lim_seq u 0)
    → Lim_seq (fun n/ u n) = Rbar_inv (Lim_seq u).

Multiplication

Lemma filterlim_Rbar_mult :
   x y z,
  is_Rbar_mult x y z
  filterlim (fun zfst z × snd z) (filter_prod (Rbar_locally x) (Rbar_locally y)) (Rbar_locally z).

Lemma is_lim_seq_mult (u v : natR) (l1 l2 l : Rbar) :
  is_lim_seq u l1is_lim_seq v l2
  is_Rbar_mult l1 l2 l
  is_lim_seq (fun nu n × v n) l.
Lemma is_lim_seq_mult' (u v : natR) (l1 l2 : R) :
  is_lim_seq u l1is_lim_seq v l2
  is_lim_seq (fun nu n × v n) (l1 × l2).

Lemma ex_lim_seq_mult (u v : natR) :
  ex_lim_seq uex_lim_seq v
  ex_Rbar_mult (Lim_seq u) (Lim_seq v) →
  ex_lim_seq (fun nu n × v n).

Lemma Lim_seq_mult (u v : natR) :
  ex_lim_seq uex_lim_seq v
  ex_Rbar_mult (Lim_seq u) (Lim_seq v) →
  Lim_seq (fun nu n × v n) = Rbar_mult (Lim_seq u) (Lim_seq v).

Multiplication by a scalar

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 xRmult x a) (Rbar_locally l) (Rbar_locally (Rbar_mult l a)).

Lemma is_lim_seq_scal_l (u : natR) (a : R) (lu : Rbar) :
  is_lim_seq u lu
  is_lim_seq (fun na × u n) (Rbar_mult a lu).

Lemma ex_lim_seq_scal_l (u : natR) (a : R) :
  ex_lim_seq uex_lim_seq (fun na × u n).

Lemma Lim_seq_scal_l (u : natR) (a : R) :
  Lim_seq (fun na × u n) = Rbar_mult a (Lim_seq u).

Lemma is_lim_seq_scal_r (u : natR) (a : R) (lu : Rbar) :
  is_lim_seq u lu
    is_lim_seq (fun nu n × a) (Rbar_mult lu a).

Lemma ex_lim_seq_scal_r (u : natR) (a : R) :
  ex_lim_seq uex_lim_seq (fun nu n × a).

Lemma Lim_seq_scal_r (u : natR) (a : R) :
  Lim_seq (fun nu n × a) = Rbar_mult (Lim_seq u) a.

Division

Lemma is_lim_seq_div (u v : natR) (l1 l2 l : Rbar) :
  is_lim_seq u l1is_lim_seq v l2l2 0 →
  is_Rbar_div l1 l2 l
  is_lim_seq (fun nu n / v n) l.
Lemma is_lim_seq_div' (u v : natR) (l1 l2 : R) :
  is_lim_seq u l1is_lim_seq v l2l2 0 →
  is_lim_seq (fun nu n / v n) (l1 / l2).
Lemma ex_lim_seq_div (u v : natR) :
  ex_lim_seq uex_lim_seq vLim_seq v 0 →
  ex_Rbar_div (Lim_seq u) (Lim_seq v) →
  ex_lim_seq (fun nu n / v n).
Lemma Lim_seq_div (u v : natR) :
  ex_lim_seq uex_lim_seq v → (Lim_seq v 0) →
  ex_Rbar_div (Lim_seq u) (Lim_seq v) →
  Lim_seq (fun nu n / v n) = Rbar_div (Lim_seq u) (Lim_seq v).

Additional limits


Lemma ex_lim_seq_adj (u v : natR) :
  ( n, u n u (S n)) → ( n, v (S n) v n)
  → is_lim_seq (fun nv n - u n) 0
  → ex_finite_lim_seq u ex_finite_lim_seq v Lim_seq u = Lim_seq v.

Image by a continuous function

Lemma is_lim_seq_continuous (f : RR) (u : natR) (l : R) :
  continuity_pt f lis_lim_seq u l
  → is_lim_seq (fun nf (u n)) (f l).

Absolute value

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

Lemma is_lim_seq_abs (u : natR) (l : Rbar) :
  is_lim_seq u lis_lim_seq (fun nRabs (u n)) (Rbar_abs l).
Lemma ex_lim_seq_abs (u : natR) :
  ex_lim_seq uex_lim_seq (fun nRabs (u n)).
Lemma Lim_seq_abs (u : natR) :
  ex_lim_seq u
  Lim_seq (fun nRabs (u n)) = Rbar_abs (Lim_seq u).

Lemma is_lim_seq_abs_0 (u : natR) :
  is_lim_seq u 0 is_lim_seq (fun nRabs (u n)) 0.

Geometric sequences

Lemma is_lim_seq_geom (q : R) :
  Rabs q < 1 → is_lim_seq (fun nq ^ n) 0.
Lemma ex_lim_seq_geom (q : R) :
  Rabs q < 1 → ex_lim_seq (fun nq ^ n).
Lemma Lim_seq_geom (q : R) :
  Rabs q < 1 → Lim_seq (fun nq ^ n) = 0.

Lemma is_lim_seq_geom_p (q : R) :
  1 < qis_lim_seq (fun nq ^ n) p_infty.
Lemma ex_lim_seq_geom_p (q : R) :
  1 < qex_lim_seq (fun nq ^ n).
Lemma Lim_seq_geom_p (q : R) :
  1 < qLim_seq (fun nq ^ n) = p_infty.

Lemma ex_lim_seq_geom_m (q : R) :
  q -1 → ¬ ex_lim_seq (fun nq ^ n).

Rbar_loc_seq converges