Library mathcomp.analysis.altreals.realseq

(* -------------------------------------------------------------------- 
 Copyright (c) - 2015--2016 - IMDEA Software Institute                
 Copyright (c) - 2015--2018 - Inria                                   
 Copyright (c) - 2016--2018 - Polytechnique                           *)

From mathcomp Require Import all_ssreflect all_algebra.
Require Import mathcomp.bigenough.bigenough.
Require Import xfinmap boolp ereal reals discrete.
Require Import classical_sets topology.

Set Implicit Arguments.

Import Order.TTheory GRing.Theory Num.Theory BigEnough.

Local Open Scope ring_scope.

Notation "f '<=1' g" := (∀ x, f x ≤ g x)
  (at level 70, no associativity).

Notation "f '<=2' g" := (∀ x y, f x y ≤ g x y)
  (at level 70, no associativity).

Section FFTheory.
Context {R : realDomainType} (T : Type).

Implicit Types (f g h : T → R).

Lemma leff f : f <=1 f.

Lemma lef_trans g f h : f <=1 g → g <=1 h → f <=1 h.
End FFTheory.

Section Nbh.
Context {R : realType}.

Inductive nbh : \bar R → predArgType :=
| NFin (c e : R) of (0 < e) : nbh c%:E
| NPInf (M : R) : nbh +oo
| NNInf (M : R) : nbh -oo.

Coercion pred_of_nbh l (v : nbh l) :=
  match v with
  | @NFin l e _ ⇒ [pred x : R | `|x - l| < e]
  | @NPInf M ⇒ [pred x : R | x > M]
  | @NNInf M ⇒ [pred x : R | x < M]
  end.
End Nbh.

Section NbhElim.
Context {R : realType}.

Lemma nbh_finW c (P : ∀ x, nbh x → Prop) :
    (∀ e (h : 0 < e), P _ (@NFin R c e h))
  → ∀ (v : nbh c%:E), P _ v.

Lemma nbh_pinfW (P : ∀ x, nbh x → Prop) :
  (∀ M, P _ (@NPInf R M)) → ∀ (v : nbh +oo), P _ v.

Lemma nbh_ninfW (P : ∀ x, nbh x → Prop) :
  (∀ M, P _ (@NNInf R M)) → ∀ (v : nbh -oo), P _ v.
End NbhElim.

Arguments nbh_finW : clear implicits.
Arguments nbh_pinfW : clear implicits.
Arguments nbh_ninfW : clear implicits.

Definition eclamp {R : realType} (e : R) :=
  if e ≤ 0 then 1 else e.

Lemma gt0_clamp {R : realType} (e : R) : 0 < eclamp e.

Lemma eclamp_id {R : realType} (e : R) : 0 < e → eclamp e = e.

Definition B1 {R : realType} (x : R) :=
  @NFin R x 1 ltr01.

Definition B {R : realType} (x e : R) :=
  @NFin R x (eclamp e) (gt0_clamp e).

Lemma separable_le {R : realType} (l1 l2 : \bar R) :
  (l1 < l2)%E → ∃ (v1 : nbh l1) (v2 : nbh l2),
    ∀ x y, x \in v1 → y \in v2 → x < y.

Lemma separable {R : realType} (l1 l2 : \bar R) :
  l1 != l2 → ∃ (v1 : nbh l1) (v2 : nbh l2),
    ∀ x, x \notin [predI v1 & v2].

Section SequenceLim.
Variable (R : realType).

Implicit Types (u v : nat → R).

Definition ncvg u l :=
  ∀ v : nbh l, ∃ K, ∀ n, (K ≤ n)%N → u n \in v.

Definition iscvg (u : nat → R) := ∃ l, ncvg u l%:E.

Definition nbounded u :=
  ∃ v : nbh 0%:E, ∀ n, u n \in v.

Lemma nboundedP u :
  reflect (exists2 M, 0 < M & ∀ n, `|u n| < M) `[< nbounded u >].
End SequenceLim.

Notation "c %:S" := (fun _ : nat ⇒ c) (at level 2, format "c %:S").

Section SeqLimTh.
Variable (R : realType).

Implicit Types (u v : nat → R) (c : R) (l : \bar R).

Lemma ncvg_uniq u l1 l2 : ncvg u l1 → ncvg u l2 → l1 = l2.

Lemma ncvg_eq_from K v u l :
  (∀ n, (K ≤ n)%N → u n = v n) → ncvg v l → ncvg u l.

Lemma ncvg_eq v u l : u =1 v → ncvg v l → ncvg u l.

Lemma ncvg_le_from K v u (lv lu : \bar R) :
  (∀ n, (K ≤ n)%N → u n ≤ v n) → ncvg v lv → ncvg u lu → (lu ≤ lv)%E.

Lemma ncvg_le v u (lv lu : \bar R) :
  u <=1 v → ncvg v lv → ncvg u lu → (lu ≤ lv)%E.

Lemma ncvg_nbounded u x : ncvg u x%:E → nbounded u.

Lemma nboundedC c : nbounded c%:S.

Lemma ncvgC c : ncvg c%:S c%:E.

Lemma ncvgD u v lu lv : ncvg u lu%:E → ncvg v lv%:E →
  ncvg (u \+ v) (lu + lv)%:E.

Lemma ncvgN u lu : ncvg u lu → ncvg (- u) (- lu).

Lemma ncvgN_fin u lu : ncvg u lu%:E → ncvg (- u) (- lu)%:E.

Lemma ncvgB u v lu lv : ncvg u lu%:E → ncvg v lv%:E →
  ncvg (u \- v) (lu - lv)%:E.

Lemma ncvg_abs u lu : ncvg u lu%:E → ncvg (fun n ⇒ `|u n|) `|lu|%:E.

Lemma ncvg_abs0 u : ncvg (fun n ⇒ `|u n|) 0%:E → ncvg u 0%:E.

Lemma ncvgMl u v : ncvg u 0%:E → nbounded v → ncvg (u \* v) 0%:E.

Lemma ncvgMr u v : ncvg v 0%:E → nbounded u → ncvg (u \* v) 0%:E.

Lemma ncvgM u v lu lv : ncvg u lu%:E → ncvg v lv%:E →
  ncvg (u \* v) (lu × lv)%:E.

Lemma ncvgZ c u lu : ncvg u lu%:E → ncvg (c \*o u) (c × lu)%:E.

Lemma ncvg_leC c u (lu : \bar R) :
  (∀ n, u n ≤ c) → ncvg u lu → (lu ≤ c%:E)%E.

Lemma ncvg_geC c u (lu : \bar R) :
  (∀ n, c ≤ u n) → ncvg u lu → (c%:E ≤ lu)%E.

Lemma iscvgC c : iscvg c%:S.

Hint Resolve iscvgC : core.

Lemma iscvgD (u v : nat → R) : iscvg u → iscvg v → iscvg (u \+ v).

Lemma iscvg_sum {I : eqType} (u : I → nat → R) r :
  (∀ i, i \in r → iscvg (u i)) →
    iscvg (fun n ⇒ \sum_(i <- r) u i n).

Lemma iscvg_eq (u v : nat → R) :
  u =1 v → iscvg v → iscvg u.

Lemma ncvg_sub h u lu :
     {homo h : x y / (x < y)%N}
  → ncvg u lu → ncvg (fun n ⇒ u (h n)) lu.

Lemma iscvg_sub σ u :
  {homo σ : x y / (x < y)%N} → iscvg u → iscvg (u \o σ).

Lemma ncvg_shift k (u : nat → R) l :
  ncvg u l ↔ ncvg (fun n ⇒ u (n + k)%N) l.

Lemma iscvg_shift k (u : nat → R) :
  iscvg u ↔ iscvg (fun n ⇒ u (n + k)%N).

Lemma ncvg_gt (u : nat → R) (l1 l2 : \bar R) :
  (l1 < l2)%E → ncvg u l2 →
    ∃ K, ∀ n, (K ≤ n)%N → (l1 < (u n)%:E)%E.

Lemma ncvg_lt (u : nat → R) (l1 l2 : \bar R) :
  (l1 < l2)%E → ncvg u l1 →
    ∃ K, ∀ n, (K ≤ n)%N → ((u n)%:E < l2)%E.

Lemma ncvg_homo_lt (u : nat → R) (l1 l2 : \bar R) :
    (∀ m n, (m ≤ n)%N → u m ≤ u n)
  → (l1 < l2)%E → ncvg u l1 → ∀ n, ((u n)%:E < l2)%E.

Lemma ncvg_homo_le (u : nat → R) (l : \bar R) :
    (∀ m n, (m ≤ n)%N → u m ≤ u n)
  → ncvg u l → ∀ n, ((u n)%:E ≤ l)%E.
End SeqLimTh.

Section LimOp.
Context {R : realType}.

Implicit Types (u v : nat → R).

Definition nlim u : \bar R :=
  if @idP `[∃ l, `[< ncvg u l >]] is ReflectT Px then
    xchooseb Px else -oo.

Lemma nlim_ncvg u : (∃ l, ncvg u l) → ncvg u (nlim u).

Lemma nlim_out u : ¬ (∃ l, ncvg u l) → nlim u = -oo%E.

CoInductive nlim_spec (u : nat → R) : \bar R → Type :=
| NLimCvg l : ncvg u l → nlim_spec u l
| NLimOut : ¬ (∃ l, ncvg u l) → nlim_spec u -oo.

Lemma nlimP u : nlim_spec u (nlim u).

Lemma nlimE (u : nat → R) (l : \bar R) : ncvg u l → nlim u = l.

Lemma nlimC c : nlim c%:S = c%:E :> \bar R.

Lemma nlimD (u v : nat → R) : iscvg u → iscvg v →
  nlim (u \+ v) = (nlim u + nlim v)%E.

Lemma eq_from_nlim K (v u : nat → R) :
  (∀ n, (K ≤ n)%N → u n = v n) → nlim u = nlim v.

Lemma eq_nlim (v u : nat → R) : u =1 v → nlim u = nlim v.

Lemma nlim_bump (u : nat → R) : nlim (fun n ⇒ u n.+1) = nlim u.

Lemma nlim_lift (u : nat → R) p : nlim (fun n ⇒ u (n + p)%N) = nlim u.

Lemma nlim_sum {I : eqType} (u : I → nat → R) (r : seq I) :
  (∀ i, i \in r → iscvg (u i)) →
      nlim (fun n ⇒ \sum_(i <- r) (u i) n)
    = (\sum_(i <- r) nlim (u i))%E.

Lemma nlim_sumR {I : eqType} (u : I → nat → R) (r : seq I) :
    (∀ i, i \in r → iscvg (u i)) →
  nlim (fun n ⇒ \sum_(i <- r) (u i) n) = (\sum_(i <- r)
    (fine (nlim (u i)) : R))%:E.

Lemma nlim_sup (u : nat → R) l :
    (∀ n m, (n ≤ m)%N → u n ≤ u m)
  → ncvg u l%:E
  → sup [set r | ∃ n, r = u n] = l.

End LimOp.