Module mathcomp.analysis.ereal

From HB Require Import structures.
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.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

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%dE]_(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) :
  (forall 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) :
  (forall 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 ->
  (forall i, P i -> 0 <= F i) ->
  \sum_(i \in P) F i = 0 -> forall 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], forall 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 ->
  (forall 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) :
  (forall 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) :
  (forall 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^d R) :
  (forall 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) :
  (forall 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^d R.

Lemma dfsume_gt0 (I : choiceType) (P : set I) (F : I -> \bar^d 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^d 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^d R) :
  finite_set P ->
  (forall i, P i -> 0 <= F i) ->
  \sum_(i \in P) F i = 0 -> forall i, P i -> F i = 0.

Lemma le0_mule_dfsumr (T : choiceType) x (F : T -> \bar^d R) (P : set T) :
  (forall 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^d R) (P : set T) :
  (forall 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.

HB.instance Definition _ (R : numDomainType) := isPointed.Build (\bar 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_supy S : S +oo -> ereal_sup S = +oo.

Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= 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_le S x : (exists2 y, S y & y <= x) -> ereal_inf S <= x.

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 R) : ~ has_ubound A ->
  A !=set0 -> ereal_sup (EFin @` 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) : set_system (\bar R) :=
  [set P | match x with
    | r%:E => r^' (fun r => P r%:E)
    | +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y
    | -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y
  end].
Definition ereal_nbhs (x : \bar R) : set_system (\bar R) :=
  [set P | match x with
    | x%:E => nbhs x (fun r => P r%:E)
    | +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y
    | -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y
  end].
HB.instance Definition _ := hasNbhs.Build (\bar R) ereal_nbhs.
End ereal_nbhs.

Section ereal_nbhs_instances.
Context {R : numFieldType}.

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

Global Instance ereal_nbhs_filter : forall 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 -> \forall x \near +oo, r%:E < x.

Lemma ereal_nbhs_pinfty_ge r : r \is Num.real -> \forall x \near +oo, r%:E <= x.

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

Lemma ereal_nbhs_ninfty_le r : r \is Num.real -> \forall x \near -oo, r%:E >= x.

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

Lemma ereal_nbhs_ninfty_real : \forall 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).

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 (-%E : \bar R -> \bar 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)).

HB.instance Definition _ := Nbhs_isPseudoMetric.Build R (\bar R)
  ereal_nbhsE ereal_ball_center ereal_ball_sym ereal_ball_triangle erefl.

End ereal_PseudoMetric.

Lemma nbhs_interval (R : realFieldType) (P : R -> Prop) (r : R) (a b : \bar R) :
  a < r%:E -> r%:E < b ->
  (forall 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 @ \oo--> ereal_dnbhs x.