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.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import fsbigop cardinality set_interval.
Require Import reals signed 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.

Notation "\sum_ ( i '\in' A ) F" := (\big[+%dE/0%E]_(i \in A) F%dE) :
  ereal_dual_scope.
Notation "\sum_ ( i '\in' A ) F" := (\big[+%E/0%E]_(i \in A) F%E) :
  ereal_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.

Lemma compreDr T (h : R → \bar R) (f g : T → R) :
  {morph h : x y / (x + y)%R >-> (x + y)%E} →
  h \o (f \+ g)%R = ((h \o f) \+ (h \o g))%E.

Lemma compreN T (h : R → \bar R) (f : T → R) :
  {morph h : x / (- x)%R >-> (- x)%E} →
  h \o (\- f)%R = \- (h \o f)%E.

Lemma compreBr T (h : R → \bar R) (f g : T → R) :
  {morph h : x y / (x - y)%R >-> (x - y)%E} →
  h \o (f \- g)%R = ((h \o f) \- (h \o g))%E.

Lemma compre_scale T (h : R → \bar R) (f : T → R) k :
  {morph h : x y / (x × y)%R >-> (x × y)%E} →
  h \o (k \o× f) = (fun t ⇒ h k × h (f t))%E.

Local Close Scope classical_set_scope.

End ERealArith.

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

Lemma range_oppe : range -%E = [set: \bar R]%classic.

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

Lemma fsume_ge0 (I : choiceType) (P : set I) (F : I → \bar R) :
  (∀ i, P i → 0 ≤ F i) → 0 ≤ \sum_(i \in P) F i.

Lemma fsume_le0 (I : choiceType) (P : set I) (F : I → \bar R) :
  (∀ t, P t → F t ≤ 0) → \sum_(i \in P) F i ≤ 0.

Lemma fsumEFin (I : choiceType) A (F : I → R) : finite_set A →
  \sum_(i \in A) (F i)%:E = (\sum_(i \in A) F i)%:E.

End ERealArithTh_numDomainType.

Section ERealArithTh_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y z u a b : \bar R) (r : R).

Lemma le_er_map_in (A : set R) (f : R → R) :
  {in A &, {homo f : x y / (x ≤ y)%O}} →
  {in (EFin @` A)%classic &, {homo er_map f : x y / (x ≤ y)%E}}.

Lemma fsume_gt0 (I : choiceType) (P : set I) (F : I → \bar R) :
  0 < \sum_(i \in P) F i → exists2 i, P i & 0 < F i.

Lemma fsume_lt0 (I : choiceType) (P : set I) (F : I → \bar R) :
  \sum_(i \in P) F i < 0 → exists2 i, P i & F i < 0.

Lemma pfsume_eq0 (I : choiceType) (P : set I) (F : I → \bar R) :
  finite_set P →
  (∀ i, P i → 0 ≤ F i) →
  \sum_(i \in P) F i = 0 → ∀ i, P i → F i = 0.

Lemma lee_fsum_nneg_subset [T : choiceType] [A B : set T] [f : T → \bar R] :
  finite_set A → finite_set B →
  {subset A ≤ B} → {in [predD B & A], ∀ t : T, 0 ≤ f t}%E →
  (\sum_(t \in A) f t ≤ \sum_(t \in B) f t)%E.

Lemma lee_fsum [T : choiceType] (I : set T) (a b : T → \bar R) :
  finite_set I →
  (∀ i, I i → a i ≤ b i)%E → (\sum_(i \in I) a i ≤ \sum_(i \in I) b i)%E.

Lemma ge0_mule_fsumr (T : choiceType) x (F : T → \bar R) (P : set T) :
  (∀ i : T, 0 ≤ F i) → x × (\sum_(i \in P) F i) = \sum_(i \in P) x × F i.

Lemma ge0_mule_fsuml (T : choiceType) x (F : T → \bar R) (P : set T) :
  (∀ i : T, 0 ≤ F i) → (\sum_(i \in P) F i) × x = \sum_(i \in P) F i × x.

End ERealArithTh_realDomainType.
Arguments lee_fsum [R T I a b].

Module DualAddTheoryNumDomain.

Import DualAddTheory.

Section DualERealArithTh_numDomainType.

Local Open Scope ereal_dual_scope.

Context {R : numDomainType}.

Implicit Types x y z : \bar R.

Lemma finite_supportNe (I : choiceType) (P : set I) (F : I → \bar R) :
  finite_support 0%E P (\- F)%E = finite_support 0%E P F.

Lemma dual_fsumeE (I : choiceType) (P : set I) (F : I → \bar R) :
  (\sum_(i \in P) F i)%dE = (- (\sum_(i \in P) (- F i)))%E.

Lemma dfsume_ge0 (I : choiceType) (P : set I) (F : I → \bar R) :
  (∀ i, P i → 0 ≤ F i) → 0 ≤ \sum_(i \in P) F i.

Lemma dfsume_le0 (I : choiceType) (P : set I) (F : I → \bar R) :
  (∀ t, P t → F t ≤ 0) → \sum_(i \in P) F i ≤ 0.

End DualERealArithTh_numDomainType.

Section DualERealArithTh_realDomainType.

Import DualAddTheory.

Local Open Scope ereal_dual_scope.

Context {R : realDomainType}.
Implicit Types x y z a b : \bar R.

Lemma dfsume_gt0 (I : choiceType) (P : set I) (F : I → \bar R) :
  0 < \sum_(i \in P) F i → exists2 i, P i & 0 < F i.

Lemma dfsume_lt0 (I : choiceType) (P : set I) (F : I → \bar R) :
  \sum_(i \in P) F i < 0 → exists2 i, P i & F i < 0.

Lemma pdfsume_eq0 (I : choiceType) (P : set I) (F : I → \bar R) :
  finite_set P →
  (∀ i, P i → 0 ≤ F i) →
  \sum_(i \in P) F i = 0 → ∀ i, P i → F i = 0.

Lemma le0_mule_dfsumr (T : choiceType) x (F : T → \bar R) (P : set T) :
  (∀ i : T, F i ≤ 0) → x × (\sum_(i \in P) F i) = \sum_(i \in P) x × F i.

Lemma le0_mule_dfsuml (T : choiceType) x (F : T → \bar R) (P : set T) :
  (∀ i : T, F i ≤ 0) → (\sum_(i \in P) F i) × x = \sum_(i \in P) F i × x.

End DualERealArithTh_realDomainType.

End DualAddTheoryNumDomain.

Module DualAddTheory.
Export ConstructiveDualAddTheory.
Export DualAddTheoryNumDomain.
End DualAddTheory.

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

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

Lemma uboundT : ubound [set: \bar R] = [set +oo].

Lemma ereal_ub_pinfty S : ubound S +oo.

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

Lemma supremumsT : supremums [set: \bar R] = [set +oo].

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

Lemma supremumT : supremum -oo [set: \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_supT : ereal_sup [set: \bar R] = +oo.

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

Lemma ereal_inf0 : ereal_inf set0 = +oo.

Lemma ereal_infT : ereal_inf [set: \bar R] = -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.

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.

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_nbhs_infty.
Context (R : numFieldType).
Implicit Type (r : R).

Lemma ereal_nbhs_pinfty_gt r : r \is Num.real → \∀ x \near +oo, r%:E < x.

Lemma ereal_nbhs_pinfty_ge r : r \is Num.real → \∀ x \near +oo, r%:E ≤ x.

Lemma ereal_nbhs_ninfty_lt r : r \is Num.real → \∀ x \near -oo, r%:E > x.

Lemma ereal_nbhs_ninfty_le r : r \is Num.real → \∀ x \near -oo, r%:E ≥ x.

Lemma ereal_nbhs_pinfty_real : \∀ x \near +oo, fine x \is @Num.real R.

Lemma ereal_nbhs_ninfty_real : \∀ x \near -oo, fine x \is @Num.real R.

End ereal_nbhs_infty.

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.