Library mathcomp.analysis.ereal

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              
 -------------------------------------------------------------------- 
 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 finmap.
Require Import boolp mathcomp_extra classical_sets functions reals signed.
Require Import topology.
Require Export constructive_ereal.

Set Implicit Arguments.

Import Order.TTheory GRing.Theory Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope ring_scope.

Local Open Scope ereal_scope.

Local Open Scope classical_set_scope.

Lemma EFin_bigcup T (F : nat → set T) :
  EFin @` (\bigcup_i F i) = \bigcup_i (EFin @` F i).

Lemma EFin_setC T (A : set T) :
  EFin @` (~` A) = (~` (EFin @` A)) `\` [set -oo; +oo].

Local Close Scope classical_set_scope.

Section ERealArith.
Context {R : numDomainType}.
Implicit Types x y z : \bar R.

Local Open Scope classical_set_scope.

Lemma preimage_abse_pinfty : @abse R @^-1` [set +oo] = [set -oo; +oo].

Lemma preimage_abse_ninfty : (@abse R @^-1` [set -oo])%classic = set0.

Local Close Scope classical_set_scope.

End ERealArith.

Section ERealArithTh_numDomainType.
Context {R : numDomainType}.
Implicit Types (x y z : \bar R) (r : R).

Lemma oppe_subset (A B : set (\bar R)) :
  ((A `<=` B) ↔ (-%E @` A `<=` -%E @` B))%classic.

End ERealArithTh_numDomainType.

Section ereal_supremum.
Variable R : realFieldType.
Local Open Scope classical_set_scope.
Implicit Types (S : set (\bar R)) (x y : \bar R).

Lemma ereal_ub_pinfty S : ubound S +oo.

Lemma ereal_ub_ninfty S : ubound S -oo → S = set0 ∨ S = [set -oo].

Lemma ereal_supremums_set0_ninfty : supremums (@set0 (\bar R)) -oo.

Lemma supremum_pinfty S x0 : S +oo → supremum x0 S = +oo.

Definition ereal_sup S := supremum -oo S.

Definition ereal_inf S := - ereal_sup (-%E @` S).

Lemma ereal_sup0 : ereal_sup set0 = -oo.

Lemma ereal_sup1 x : ereal_sup [set x] = x.

Lemma ereal_inf0 : ereal_inf set0 = +oo.

Lemma ereal_inf1 x : ereal_inf [set x] = x.

Lemma ub_ereal_sup S M : ubound S M → ereal_sup S ≤ M.

Lemma lb_ereal_inf S M : lbound S M → M ≤ ereal_inf S.

Lemma ub_ereal_sup_adherent S (e : R) : (0 < e)%R →
  ereal_sup S \is a fin_num → exists2 x, S x & (ereal_sup S - e%:E < x).

Lemma lb_ereal_inf_adherent S (e : R) : (0 < e)%R →
  ereal_inf S \is a fin_num → exists2 x, S x & (x < ereal_inf S + e%:E).

Lemma ereal_sup_gt S x : x < ereal_sup S → exists2 y, S y & x < y.

Lemma ereal_inf_lt S x : ereal_inf S < x → exists2 y, S y & y < x.

End ereal_supremum.

Section ereal_supremum_realType.
Variable R : realType.
Local Open Scope classical_set_scope.
Implicit Types S : set (\bar R).
Implicit Types x : \bar R.

Let fine_def r0 x : R := if x is r%:E then r else r0.

Lemma ereal_supremums_neq0 S : supremums S !=set0.

Lemma ereal_sup_ub S : ubound S (ereal_sup S).

Lemma ereal_sup_ninfty S : ereal_sup S = -oo ↔ S `<=` [set -oo].

Lemma ereal_inf_lb S : lbound S (ereal_inf S).

Lemma ereal_inf_pinfty S : ereal_inf S = +oo ↔ S `<=` [set +oo].

Lemma le_ereal_sup : {homo @ereal_sup R : A B / A `<=` B >-> A ≤ B}.

Lemma le_ereal_inf : {homo @ereal_inf R : A B / A `<=` B >-> B ≤ A}.

Lemma hasNub_ereal_sup (A : set (\bar R)) : ¬ has_ubound A →
  A !=set0 → ereal_sup A = +oo%E.

Lemma ereal_sup_EFin (A : set R) :
  has_ubound A → A !=set0 → ereal_sup (EFin @` A) = (sup A)%:E.

Lemma ereal_inf_EFin (A : set R) : has_lbound A → A !=set0 →
   ereal_inf (EFin @` A) = (inf A)%:E.

End ereal_supremum_realType.

Canonical ereal_pointed (R : numDomainType) := PointedType (extended R) 0%E.

Lemma restrict_abse T (R : numDomainType) (f : T → \bar R) (D : set T) :
  (abse \o f) \_ D = abse \o (f \_ D).

Section SignedRealFieldStability.
Context {R : realFieldType}.

Definition ereal_sup_reality_subdef (xnz : KnownSign.nullity)
    (xr : KnownSign.reality) :=
  (if KnownSign.wider_reality <=0 xr then KnownSign.Real <=0
   else >=<0)%snum_sign.
Arguments ereal_sup_reality_subdef /.

Lemma ereal_sup_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
    (S : {compare (0 : \bar R) & xnz & xr} → Prop)
    (r := ereal_sup_reality_subdef xnz xr) :
  Signed.spec 0 ?=0 r (ereal_sup [set x%:num | x in S]%classic).

Canonical ereal_sup_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
    (S : {compare (0 : \bar R) & xnz & xr} → Prop) :=
  Signed.mk (ereal_sup_snum_subproof S).

Definition ereal_inf_reality_subdef (xnz : KnownSign.nullity)
    (xr : KnownSign.reality) :=
  (if KnownSign.wider_reality >=0 xr then KnownSign.Real >=0
   else >=<0)%snum_sign.
Arguments ereal_inf_reality_subdef /.

Lemma ereal_inf_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
    (S : {compare (0 : \bar R) & xnz & xr} → Prop)
    (r := ereal_inf_reality_subdef xnz xr) :
  Signed.spec 0 ?=0 r (ereal_inf [set x%:num | x in S]%classic).

Canonical ereal_inf_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
    (S : {compare (0 : \bar R) & xnz & xr} → Prop) :=
  Signed.mk (ereal_inf_snum_subproof S).

End SignedRealFieldStability.

Section ereal_nbhs.
Context {R : numFieldType}.
Local Open Scope ereal_scope.
Local Open Scope classical_set_scope.

Definition ereal_dnbhs (x : \bar R) (P : \bar R → Prop) : Prop :=
  match x with
    | r%:E ⇒ r^' (fun r ⇒ P r%:E)
    | +oo ⇒ ∃ M, M \is Num.real ∧ ∀ y, M%:E < y → P y
    | -oo ⇒ ∃ M, M \is Num.real ∧ ∀ y, y < M%:E → P y
  end.
Definition ereal_nbhs (x : \bar R) (P : \bar R → Prop) : Prop :=
  match x with
    | x%:E ⇒ nbhs x (fun r ⇒ P r%:E)
    | +oo ⇒ ∃ M, M \is Num.real ∧ ∀ y, M%:E < y → P y
    | -oo ⇒ ∃ M, M \is Num.real ∧ ∀ y, y < M%:E → P y
  end.
Canonical ereal_ereal_filter :=
  FilteredType (extended R) (extended R) (ereal_nbhs).
End ereal_nbhs.

Lemma ereal_nbhs_pinfty_ge (R : numFieldType) (e : {posnum R}) :
  \∀ x \near +oo, e%:num%:E ≤ x.

Lemma ereal_nbhs_ninfty_le (R : numFieldType) (r : R) : (r < 0)%R →
  \∀ x \near -oo, x ≤ r%:E.

Section ereal_nbhs_instances.
Context {R : numFieldType}.

Global Instance ereal_dnbhs_filter :
  ∀ x : \bar R, ProperFilter (ereal_dnbhs x).
Typeclasses Opaque ereal_dnbhs.

Global Instance ereal_nbhs_filter : ∀ x, ProperFilter (@ereal_nbhs R x).
Typeclasses Opaque ereal_nbhs.

End ereal_nbhs_instances.

Section ereal_topologicalType.
Variable R : realFieldType.

Lemma ereal_nbhs_singleton (p : \bar R) (A : set (\bar R)) :
  ereal_nbhs p A → A p.

Lemma ereal_nbhs_nbhs (p : \bar R) (A : set (\bar R)) :
  ereal_nbhs p A → ereal_nbhs p (ereal_nbhs^~ A).

Definition ereal_topologicalMixin : Topological.mixin_of (@ereal_nbhs R) :=
  topologyOfFilterMixin _ ereal_nbhs_singleton ereal_nbhs_nbhs.
Canonical ereal_topologicalType := TopologicalType _ ereal_topologicalMixin.

End ereal_topologicalType.

Local Open Scope classical_set_scope.

Lemma nbhsNe (R : realFieldType) (x : \bar R) :
  nbhs (- x) = [set (-%E @` A) | A in nbhs x].

Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) :
  nbhs (- z) (-%E @` A) → nbhs z A.

Lemma oppe_continuous (R : realFieldType) : continuous (@oppe R).

Section contract_expand.
Variable R : realFieldType.
Implicit Types (x : \bar R) (r : R).
Local Open Scope ereal_scope.

Lemma contract_imageN (S : set (\bar R)) :
  (@contract R) @` (-%E @` S) = -%R @` ((@contract R) @` S).

Lemma contractK : cancel (@contract R) (@expand R).

Lemma bijective_contract : {on [pred r | `|r| ≤ 1]%R, bijective (@contract R)}.

Definition le_expandLR := monoLR_in
  (in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) (@le_expand_in R).
Definition lt_expandLR := monoLR_in
  (in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) (@lt_expand R).
Definition le_expandRL := monoRL_in
  (in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) (@le_expand_in R).
Definition lt_expandRL := monoRL_in
  (in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) (@lt_expand R).

Lemma contract_eq0 x : (contract x == 0%R) = (x == 0).

Lemma contract_eqN1 x : (contract x == -1) = (x == -oo).

Lemma contract_eq1 x : (contract x == 1%R) = (x == +oo).

End contract_expand.

Section contract_expand_realType.
Variable R : realType.

Let contract := @contract R.

Lemma sup_contract_le1 S : S !=set0 → (`|sup (contract @` S)| ≤ 1)%R.

Lemma contract_sup S : S !=set0 → contract (ereal_sup S) = sup (contract @` S).

Lemma contract_inf S : S !=set0 → contract (ereal_inf S) = inf (contract @` S).

End contract_expand_realType.

Section ereal_PseudoMetric.
Variable R : realFieldType.
Implicit Types (x y : \bar R) (r : R).

Lemma le_ereal_ball x : {homo ereal_ball x : e e' / (e ≤ e')%R >-> e `<=` e'}.

Lemma expand_ereal_ball_pinfty {e : {posnum R}} r : (e%:num ≤ 1)%R →
  expand (1 - e%:num)%R < r%:E → ereal_ball +oo e%:num r%:E.

Lemma contract_ereal_ball_fin_le r r' (e : {posnum R}) : (r ≤ r')%R →
  (1 ≤ contract r%:E + e%:num)%R → ereal_ball r%:E e%:num r'%:E.

Lemma contract_ereal_ball_fin_lt r r' (e : {posnum R}) : (r' < r)%R →
  (contract r%:E - e%:num ≤ -1)%R → ereal_ball r%:E e%:num r'%:E.

Lemma expand_ereal_ball_fin_lt r' r (e : {posnum R}) : (r' < r)%R →
  expand (contract r%:E - e%:num)%R < r'%:E →
  (`|contract r%:E - e%:num| < 1)%R → ereal_ball r%:E e%:num r'%:E.

Lemma ball_ereal_ball_fin_lt r r' (e : {posnum R}) :
  let e' := (r - fine (expand (contract r%:E - e%:num)))%R in
  ball r e' r' → (r' < r)%R →
  (`|contract r%:E - (e)%:num| < 1)%R →
  ereal_ball r%:E (e)%:num r'%:E.

Lemma ball_ereal_ball_fin_le r r' (e : {posnum R}) :
  let e' : R := (fine (expand (contract r%:E + e%:num)) - r)%R in
  ball r e' r' → (r ≤ r')%R →
  (`| contract r%:E + e%:num | < 1)%R →
  (ereal_ball r%:E e%:num r'%:E).

Lemma nbhs_oo_up_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num ≤ 1)%R →
  ereal_ball +oo e%:num `<=` A → nbhs +oo A.

Lemma nbhs_oo_down_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num ≤ 1)%R →
  ereal_ball -oo e%:num `<=` A → nbhs -oo A.

Lemma nbhs_oo_up_1e (A : set (\bar R)) (e : {posnum R}) : (1 < e%:num)%R →
  ereal_ball +oo e%:num `<=` A → nbhs +oo A.

Lemma nbhs_oo_down_1e (A : set (\bar R)) (e : {posnum R}) : (1 < e%:num)%R →
  ereal_ball -oo e%:num `<=` A → nbhs -oo A.

Lemma nbhs_fin_out_above r (e : {posnum R}) (A : set (\bar R)) :
  ereal_ball r%:E e%:num `<=` A →
  (- 1 < contract r%:E - e%:num)%R →
  (1 ≤ contract r%:E + e%:num)%R →
  nbhs r%:E A.

Lemma nbhs_fin_out_below r (e : {posnum R}) (A : set (\bar R)) :
  ereal_ball r%:E e%:num `<=` A →
  (contract r%:E - e%:num ≤ - 1)%R →
  (contract r%:E + e%:num < 1)%R →
  nbhs r%:E A.

Lemma nbhs_fin_out_above_below r (e : {posnum R}) (A : set (\bar R)) :
  ereal_ball r%:E e%:num `<=` A →
  (contract r%:E - e%:num < -1)%R →
  (1 < contract r%:E + e%:num)%R →
  nbhs r%:E A.

Lemma nbhs_fin_inbound r (e : {posnum R}) (A : set (\bar R)) :
  ereal_ball r%:E e%:num `<=` A → nbhs r%:E A.

Lemma ereal_nbhsE : nbhs = nbhs_ (entourage_ (@ereal_ball R)).

Definition ereal_pseudoMetricType_mixin :=
  PseudoMetric.Mixin (@ereal_ball_center R) (@ereal_ball_sym R)
                     (@ereal_ball_triangle R) erefl.

Definition ereal_uniformType_mixin : @Uniform.mixin_of (\bar R) nbhs :=
  uniformityOfBallMixin ereal_nbhsE ereal_pseudoMetricType_mixin.

Canonical ereal_uniformType :=
  UniformType (extended R) ereal_uniformType_mixin.

Canonical ereal_pseudoMetricType :=
  PseudoMetricType (extended R) ereal_pseudoMetricType_mixin.

End ereal_PseudoMetric.

Lemma nbhs_interval (R : realFieldType) (P : R → Prop) (r : R) (a b : \bar R) :
  a < r%:E → r%:E < b →
  (∀ y, a < y%:E → y%:E < b → P y) →
  nbhs r P.

Lemma ereal_dnbhs_le (R : numFieldType) (x : \bar R) :
  ereal_dnbhs x --> ereal_nbhs x.

Lemma ereal_dnbhs_le_finite (R : numFieldType) (r : R) :
  ereal_dnbhs r%:E --> nbhs r%:E.

Definition ereal_loc_seq (R : numDomainType) (x : \bar R) (n : nat) :=
  match x with
    | x%:E ⇒ (x + (n%:R + 1)^-1)%:E
    | +oo ⇒ n%:R%:E
    | -oo ⇒ - n%:R%:E
  end.

Lemma cvg_ereal_loc_seq (R : realType) (x : \bar R) :
  ereal_loc_seq x --> ereal_dnbhs x.