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.
# Extended real numbers, classical part ($\overline{\mathbb{R}}$)
This is an addition to the file constructive_ereal.v with classical logic
elements.
```
(\sum_(i \in A) f i)%E == finitely supported sum, see fsbigop.v
ereal_sup E == supremum of E
ereal_inf E == infimum of E
ereal_supremums_neq0 S == S has a supremum
```
## Topology of extended real numbers
```
ereal_topologicalType R == topology for extended real numbers over
R, a realFieldType
ereal_pseudoMetricType R == pseudometric space for extended reals
over R where is a realFieldType; the
distance between x and y is defined by
`|contract x - contract y|
```
## Filters
```
ereal_dnbhs x == filter on extended real numbers that
corresponds to the deleted neighborhood
x^' if x is a real number and to
predicates that are eventually true if x
is +oo/-oo.
ereal_nbhs x == same as ereal_dnbhs where dnbhs is
replaced with nbhs.
ereal_loc_seq x == sequence that converges to x in the set
of extended real numbers.
```
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).
Proof.
rewrite eqEsubset; split => [_ [r [n _ Fnr <-]]|]; first by exists n => //; exists r.
by move=> x [n _ [r Fnr <- /=]]; exists r => //; exists n.
Qed.
Lemma
EFin_setC
T
(
A
: set T)
:
EFin @` (
~` A)
= (
~` (
EFin @` A))
`\` [set -oo; +oo].
Proof.
rewrite eqEsubset; split => [_ [r Ar <-]|[r | |]].
by split => [|[]//]; apply: contra_not Ar => -[? ? [] <-].
- move=> [Ar _]; apply/not_exists2P; apply: contra_not Ar => h.
by exists r => //; have [|//] := h r; apply: contrapT.
- by move=> -[_] /not_orP[_ /=].
- by move=> -[_] /not_orP[/=].
Qed.
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].
Proof.
by rewrite predeqE => y; split ; move: y => [y//| |]//=; [right | left | case].
Qed.
Lemma
preimage_abse_ninfty
: (
@abse R @^-1` [set -oo])
%classic = set0.
Proof.
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.
Proof.
by move=> mh; apply/funext => t /=; rewrite mh. Qed.
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.
Proof.
by move=> mh; apply/funext => t /=; rewrite mh. Qed.
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.
Proof.
by move=> mh; apply/funext => t /=; rewrite mh. Qed.
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.
Proof.
by move=> mf; apply/funext => t /=; rewrite mf; rewrite muleC. Qed.
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.
Proof.
by apply/seteqP; split => [//|x] _; exists (
- x)
; rewrite ?oppeK. Qed.
Lemma
oppe_subset
(
A
B
: set (
\bar R))
:
((
A `<=` B)
<-> (
-%E @` A `<=` -%E @` B))
%classic.
Proof.
split=> [AB _ [] x ? <-|AB x Ax]; first by exists x => //; exact: AB.
have /AB[y By] : ((
-%E @` A) (
- x))
%classic by exists x.
by rewrite eqe_oppP => <-.
Qed.
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.
Proof.
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.
Proof.
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.
Proof.
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}}.
Proof.
move=> h x y; rewrite !inE/= => -[r Ar <-{x}] [s As <-{y}].
by rewrite !lee_fin/= => /h; apply; rewrite inE.
Qed.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
move=> finA finB AB f0; rewrite !fsbig_finite//=; apply: lee_sum_nneg_subfset.
by apply/fsubsetP; rewrite -fset_set_sub//; apply/subsetP.
by move=> t; rewrite !inE !in_fset_set// => /f0.
Qed.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
rewrite /finite_support !unlock; congr fset_set; congr setI.
by rewrite seteqP; split=> x /= /eqP + /ltac:(
apply/eqP)
; rewrite oppe_eq0.
Qed.
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.
Proof.
Lemma
dfsume_ge0
(
I
: choiceType) (
P
: set I) (
F
: I -> \bar R)
:
(
forall
i,
P i -> 0 <= F i)
-> 0 <= \sum_(
i
\in P)
F i.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Lemma
pdfsume_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.
Proof.
Lemma
le0_mule_dfsumr
(
T
: choiceType)
x
(
F
: T -> \bar R) (
P
: set T)
:
(
forall
i
: T, F i <= 0)
-> x * (
\sum_(
i
\in P)
F i)
= \sum_(
i
\in P)
x * F i.
Proof.
Lemma
le0_mule_dfsuml
(
T
: choiceType)
x
(
F
: T -> \bar R) (
P
: set T)
:
(
forall
i
: T, F i <= 0)
-> (
\sum_(
i
\in P)
F i)
* x = \sum_(
i
\in P)
F i * x.
Proof.
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].
Proof.
apply/seteqP; split => /= [x Tx|x -> ?]; last by rewrite leey.
by apply/eqP; rewrite eq_le leey /= Tx.
Qed.
Lemma
ereal_ub_pinfty
S
: ubound S +oo.
Proof.
by apply/ubP=> x _; rewrite leey. Qed.
Lemma
ereal_ub_ninfty
S
: ubound S -oo -> S = set0 \/ S = [set -oo].
Proof.
have [->|/set0P[x Sx] Snoo] := eqVneq S set0; first by left.
right; rewrite predeqE => y; split => [/Snoo|->{y}].
by rewrite leeNy_eq => /eqP ->.
by have := Snoo _ Sx; rewrite leeNy_eq => /eqP <-.
Qed.
Lemma
supremumsT
: supremums [set: \bar R] = [set +oo].
Proof.
rewrite /supremums uboundT.
by apply/seteqP; split=> [x []//|x -> /=]; split => // y ->.
Qed.
Lemma
ereal_supremums_set0_ninfty
: supremums (
@set0 (
\bar R))
-oo.
Proof.
by split; [exact/ubP | apply/lbP=> y _; rewrite leNye]. Qed.
Lemma
supremumT
: supremum -oo [set: \bar R] = +oo.
Proof.
Lemma
supremum_pinfty
S
x0
: S +oo -> supremum x0 S = +oo.
Proof.
move=> Spoo; rewrite /supremum ifF; last by apply/eqP => S0; rewrite S0 in Spoo.
have sSoo : supremums S +oo.
split; first exact: ereal_ub_pinfty.
by move=> /= y /(
_ _ Spoo)
; rewrite leye_eq => /eqP ->.
case: xgetP.
by move=> _ -> sSxget; move: (
is_subset1_supremums sSoo sSxget).
by move/(
_ +oo)
=> gSoo; exfalso; apply gSoo => {gSoo}.
Qed.
Definition
ereal_sup
S
:= supremum -oo S.
Definition
ereal_inf
S
:= - ereal_sup (
-%E @` S).
Lemma
ereal_sup0
: ereal_sup set0 = -oo
Proof.
Lemma
ereal_supT
: ereal_sup [set: \bar R] = +oo.
Proof.
Lemma
ereal_sup1
x
: ereal_sup [set x] = x
Proof.
Lemma
ereal_inf0
: ereal_inf set0 = +oo.
Proof.
Lemma
ereal_infT
: ereal_inf [set: \bar R] = -oo.
Proof.
Lemma
ereal_inf1
x
: ereal_inf [set x] = x.
Proof.
Lemma
ub_ereal_sup
S
M
: ubound S M -> ereal_sup S <= M.
Proof.
rewrite /ereal_sup /supremum; case: ifPn => [/eqP ->|]; first by rewrite leNye.
- by move=> _ SM; case: xgetP => [_ -> [_]| _] /=; [exact |rewrite leNye].
Qed.
Lemma
lb_ereal_inf
S
M
: lbound S M -> M <= ereal_inf S.
Proof.
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).
Proof.
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).
Proof.
Lemma
ereal_sup_gt
S
x
: x < ereal_sup S -> exists2
y,
S y & x < y.
Proof.
Lemma
ereal_inf_lt
S
x
: ereal_inf S < x -> exists2
y,
S y & y < x.
Proof.
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.
Proof.
have [->|Snoo] := eqVneq S [set -oo].
by exists -oo; split; [rewrite ub_set1 |exact: lb_ub_refl].
have [->|S0] := eqVneq S set0.
by exists -oo; exact: ereal_supremums_set0_ninfty.
have [Spoo|Spoo] := pselect (
S +oo).
by exists +oo; split; [apply/ereal_ub_pinfty | apply/lbP => /= y /ubP; apply].
have [r Sr] : exists
r,
S r%:E.
move: S0 => /set0P[] [r Sr| // |Snoo1]; first by exists r.
apply/not_existsP => nS; move/negP : Snoo; apply.
by apply/eqP; rewrite predeqE => -[] // r; split => // /nS.
set U := fine_def r @` S.
have [|] := eqVneq (
ubound U)
set0.
rewrite -subset0 => U0; exists +oo.
split; [exact/ereal_ub_pinfty | apply/lbP => /= -[r0 /ubP Sr0|//|]].
- suff : ubound U r0 by move/U0.
by apply/ubP=> _ -[] [r1 Sr1 <-|//| /= _ <-]; rewrite -lee_fin; apply Sr0.
- by move/ereal_ub_ninfty => [|]; by [move/eqP : S0|move/eqP : Snoo].
set u : R := sup U.
exists u%:E; split; last first.
apply/lbP=> -[r0 /ubP Sr0| |].
- rewrite lee_fin; apply/sup_le_ub; first by exists r, r%:E.
by apply/ubP => _ -[[r2 ? <-| // | /= _ <-]]; rewrite -lee_fin; exact: Sr0.
- by rewrite leey.
- by move/ereal_ub_ninfty=> [|/eqP //]; [move/eqP : S0|rewrite (
negbTE Snoo)
].
apply/ubP => -[r0 Sr0|//|_]; last by rewrite leNye.
rewrite lee_fin.
suff : has_sup U by move/sup_upper_bound/ubP; apply; exists r0%:E.
split; first by exists r0, r0%:E.
exists u; apply/ubP => y; move=> [] y' Sy' <-{y}.
have : has_sup U by split; [exists r, r%:E | exact/set0P].
move/sup_upper_bound/ubP; apply.
by case: y' Sy' => [r1 /= Sr1 | // | /= _]; [exists r1%:E | exists r%:E].
Qed.
Lemma
ereal_sup_ub
S
: ubound S (
ereal_sup S).
Proof.
move=> y Sy; rewrite /ereal_sup /supremum ifF; last first.
by apply/eqP; rewrite predeqE => /(
_ y)
[+ _]; exact.
case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply geS.
by case: (
ereal_supremums_neq0 S)
=> /= x0 Sx0; move/(
_ x0).
Qed.
Lemma
ereal_sup_le
S
x
: (
exists2
y,
S y & x <= y)
-> x <= ereal_sup S.
Proof.
by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed.
Lemma
ereal_sup_ninfty
S
: ereal_sup S = -oo <-> S `<=` [set -oo].
Proof.
split.
by move=> supS [r /ereal_sup_ub | /ereal_sup_ub |//]; rewrite supS.
move=> /(
@subset_set1 _ S)
[] ->; [exact: ereal_sup0|exact: ereal_sup1].
Qed.
Lemma
ereal_inf_lb
S
: lbound S (
ereal_inf S).
Proof.
Lemma
ereal_inf_le
S
x
: (
exists2
y,
S y & y <= x)
-> ereal_inf S <= x.
Proof.
Lemma
ereal_inf_pinfty
S
: ereal_inf S = +oo <-> S `<=` [set +oo].
Proof.
Lemma
le_ereal_sup
: {homo @ereal_sup R :
A
B
/ A `<=` B >-> A <= B}.
Proof.
by move=> A B AB; apply: ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed.
Lemma
le_ereal_inf
: {homo @ereal_inf R :
A
B
/ A `<=` B >-> B <= A}.
Proof.
by move=> A B AB; apply: lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed.
Lemma
hasNub_ereal_sup
(
A
: set R)
: ~ has_ubound A ->
A !=set0 -> ereal_sup (
EFin @` A)
= +oo%E.
Proof.
Lemma
ereal_sup_EFin
(
A
: set R)
:
has_ubound A -> A !=set0 -> ereal_sup (
EFin @` A)
= (
sup A)
%:E.
Proof.
Lemma
ereal_inf_EFin
(
A
: set R)
: has_lbound A -> A !=set0 ->
ereal_inf (
EFin @` A)
= (
inf A)
%:E.
Proof.
move=> has_lbA A0; rewrite /ereal_inf /inf EFinN; congr (
- _)
%E.
rewrite -ereal_sup_EFin; [|exact/has_lb_ubN|exact/nonemptyN].
by rewrite !image_comp.
Qed.
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).
Proof.
by apply/funext=> t; rewrite /restrict/=; case: ifPn => // _; rewrite abse0.
Qed.
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).
Proof.
rewrite {}/r; move: xr S => [[[]|]|] S /=;
do ?[by apply: ub_ereal_sup => _ [? _ <-]
|by case: ereal_sup => [s||];
rewrite ?leey ?leNye// !lee_fin -realE num_real].
Qed.
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).
Proof.
rewrite {}/r; move: xr S => [[[]|]|] S /=;
do ?[by apply: lb_ereal_inf => _ [? _ <-]
|by case: ereal_inf => [s||];
rewrite ?leey ?leNye// !lee_fin -realE num_real].
Qed.
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 => 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) (
P
: \bar R -> Prop)
: Prop :=
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.
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
:
forall
x
: \bar R, ProperFilter (
ereal_dnbhs x).
Proof.
Typeclasses Opaque ereal_dnbhs.
Global Instance
ereal_nbhs_filter
: forall
x,
ProperFilter (
@ereal_nbhs R x).
Proof.
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.
Proof.
by exists r. Qed.
Lemma
ereal_nbhs_pinfty_ge
r
: r \is Num.real -> \forall
x
\near +oo, r%:E <= x.
Proof.
by exists r; split => //; apply: ltW. Qed.
Lemma
ereal_nbhs_ninfty_lt
r
: r \is Num.real -> \forall
x
\near -oo, r%:E > x.
Proof.
by exists r. Qed.
Lemma
ereal_nbhs_ninfty_le
r
: r \is Num.real -> \forall
x
\near -oo, r%:E >= x.
Proof.
by exists r; split => // ?; apply: ltW. Qed.
Lemma
ereal_nbhs_pinfty_real
: \forall
x
\near +oo, fine x \is @Num.
real R.
Proof.
Lemma
ereal_nbhs_ninfty_real
: \forall
x
\near -oo, fine x \is @Num.
real R.
Proof.
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.
Proof.
move: p => -[p | [M [Mreal MA]] | [M [Mreal MA]]] /=; [|exact: MA | exact: MA].
move=> /nbhs_ballP[_/posnumP[e]]; apply; exact/ballxx.
Qed.
Lemma
ereal_nbhs_nbhs
(
p
: \bar R) (
A
: set (
\bar R))
:
ereal_nbhs p A -> ereal_nbhs p (
ereal_nbhs^~ A).
Proof.
move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=.
- move=> /nbhs_ballP[_/posnumP[e]] ballA.
apply/nbhs_ballP; exists (
e%:num / 2)
=> //= r per.
apply/nbhs_ballP; exists (
e%:num / 2)
=> //= x rex.
apply/ballA/(
@ball_splitl _ _ r)
=> //; exact/ball_sym.
- exists (
M + 1)
%R; split; first by rewrite realD.
move=> -[x| _ |_] //=; last by exists M.
rewrite lte_fin => M'x /=.
apply/nbhs_ballP; exists 1%R => //= y x1y.
apply MA; rewrite lte_fin.
rewrite addrC -ltr_subr_addl in M'x.
rewrite (
lt_le_trans M'x)
// ler_subl_addl addrC -ler_subl_addl.
rewrite (
le_trans _ (
ltW x1y))
// real_ler_norm // realB //.
rewrite ltr_subr_addr in M'x.
rewrite -comparabler0 (
@comparabler_trans _ (
M + 1)
%R)
//.
by rewrite /Order.
comparable (
ltW M'x)
orbT.
by rewrite comparabler0 realD.
by rewrite num_real.
- exists (
M - 1)
%R; split; first by rewrite realB.
move=> -[x| _ |_] //=; last by exists M.
rewrite lte_fin => M'x /=.
apply/nbhs_ballP; exists 1%R => //= y x1y.
apply MA; rewrite lte_fin.
rewrite ltr_subr_addl in M'x.
rewrite (
le_lt_trans _ M'x)
// addrC -ler_subl_addl.
rewrite (
le_trans _ (
ltW x1y))
// distrC real_ler_norm // realB //.
by rewrite num_real.
rewrite addrC -ltr_subr_addr in M'x.
rewrite -comparabler0 (
@comparabler_trans _ (
M - 1)
%R)
//.
by rewrite /Order.
comparable (
ltW M'x).
by rewrite comparabler0 realB.
Qed.
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].
Proof.
case: x => [r /=| |].
- rewrite /nbhs /= /ereal_nbhs -nbhs_ballE.
rewrite predeqE => S; split => [[_/posnumP[e] reS]|[S' [_ /posnumP[e] reS' <-]]].
exists (
-%E @` S).
exists e%:num => //= r1 rer1; exists (
- r1%:E)
; last by rewrite oppeK.
by apply reS; rewrite /ball /= opprK -normrN opprD opprK.
rewrite predeqE => s; split => [[y [z Sz] <- <-]|Ss].
by rewrite oppeK.
by exists (
- s)
; [exists s | rewrite oppeK].
exists e%:num => //= r1 rer1; exists (
- r1%:E)
; last by rewrite oppeK.
by apply reS'; rewrite /ball /= opprK -normrN opprD.
- rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
exists (
-%E @` S).
exists (
- M)
%R; rewrite realN Mreal; split => // x Mx.
by exists (
- x)
; [apply MS; rewrite lte_oppl | rewrite oppeK].
rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
by exists (
- x)
; [exists x | rewrite oppeK].
exists (
- M)
%R; rewrite realN; split => // y yM.
exists (
- y)
; by [apply Mx; rewrite lte_oppr|rewrite oppeK].
- rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
exists (
-%E @` S).
exists (
- M)
%R; rewrite realN Mreal; split => // x Mx.
by exists (
- x)
; [apply MS; rewrite lte_oppr | rewrite oppeK].
rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
by exists (
- x)
; [exists x | rewrite oppeK].
exists (
- M)
%R; rewrite realN; split => // y yM.
exists (
- y)
; by [apply Mx; rewrite lte_oppl|rewrite oppeK].
Qed.
Lemma
nbhsNKe
(
R
: realFieldType) (
z
: \bar R) (
A
: set (
\bar R))
:
nbhs (
- z) (
-%E @` A)
-> nbhs z A.
Proof.
rewrite nbhsNe => -[S zS] SA; rewrite -(
oppeK z)
nbhsNe.
exists (
-%E @` S)
; first by rewrite nbhsNe; exists S.
rewrite predeqE => x; split => [[y [u Su <-{y} <-]]|Ax].
rewrite oppeK.
move: SA; rewrite predeqE => /(
_ (
- u))
[h _].
have : (
exists2
y,
S y & - y = - u)
by exists u.
by move/h => -[y Ay] /eqP; rewrite eqe_opp => /eqP <-.
exists (
- x)
; last by rewrite oppeK.
exists x => //.
move: SA; rewrite predeqE => /(
_ (
- x))
[_ h].
have : (
-%E @` A) (
- x)
by exists x.
by move/h => [y Sy] /eqP; rewrite eqe_opp => /eqP <-.
Qed.
Lemma
oppe_continuous
(
R
: realFieldType)
: continuous (
@oppe R).
Proof.
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).
Proof.
rewrite predeqE => r; split => [[y [z Sz <-{y} <-{r}]]|[s [y Sy <-{s} <-{r}]]].
by exists (
contract z)
; [exists z | rewrite contractN].
by exists (
- y)
; [exists y | rewrite contractN].
Qed.
Lemma
contractK
: cancel (
@contract R) (
@expand R).
Proof.
Lemma
bijective_contract
: {on [pred
r
| `|r| <= 1]%R, bijective (
@contract R)
}.
Proof.
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).
Proof.
Lemma
contract_eqN1
x
: (
contract x == -1)
= (
x == -oo).
Proof.
Lemma
contract_eq1
x
: (
contract x == 1%R)
= (
x == +oo).
Proof.
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.
Proof.
Lemma
contract_sup
S
: S !=set0 -> contract (
ereal_sup S)
= sup (
contract @` S).
Proof.
Lemma
contract_inf
S
: S !=set0 -> contract (
ereal_inf S)
= inf (
contract @` S).
Proof.
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'}.
Proof.
by move=> e e' ee' y; rewrite /ereal_ball => /lt_le_trans; exact. Qed.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
move=> r'r ? r'e'r.
rewrite /ereal_ball gtr0_norm ?subr_gt0 ?lt_contract ?lte_fin//.
by rewrite ltr_subl_addl addrC -ltr_subl_addl -lt_expandLR ?inE ?ltW.
Qed.
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.
Proof.
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).
Proof.
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.
Proof.
move=> e1 ooeA.
exists (
fine (
expand (
1 - e%:num)
%R))
; rewrite num_real; split => //.
case => [r | | //].
- rewrite fine_expand; last first.
by rewrite ger0_norm ?ltr_subl_addl ?ltr_addr // subr_ge0.
by move=> ?; exact/ooeA/expand_ereal_ball_pinfty.
- by move=> _; exact/ooeA/ereal_ball_center.
Qed.
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.
Proof.
move=> e1 reA; suff h : nbhs +oo (
-%E @` A).
rewrite (
_ : -oo = - +oo)
// nbhsNe; exists (
-%E @` A)
=> //.
rewrite predeqE => x; split=> [[y [z Az <- <-]]|Ax]; rewrite ?oppeK //.
by exists (
- x)
; [exists x | rewrite oppeK].
apply (
@nbhs_oo_up_e1 _ e)
=> // x x1e; exists (
- x)
; last by rewrite oppeK.
by apply/reA/ereal_ballN; rewrite oppeK.
Qed.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Lemma
nbhs_fin_inbound
r
(
e
: {posnum R}) (
A
: set (
\bar R))
:
ereal_ball r%:E e%:num `<=` A -> nbhs r%:E A.
Proof.
Lemma
ereal_nbhsE
: nbhs = nbhs_ (
entourage_ (
@ereal_ball R)).
Proof.
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 ->
(
forall
y,
a < y%:E -> y%:E < b -> P y)
->
nbhs r P.
Proof.
move => ar rb abP; case: (
lt_ereal_nbhs ar rb)
=> d rd.
exists d%:num => //= y; rewrite /= distrC.
by move=> /rd /andP[? ?]; apply: abP.
Qed.
Lemma
ereal_dnbhs_le
(
R
: numFieldType) (
x
: \bar R)
:
ereal_dnbhs x --> ereal_nbhs x.
Proof.
move: x => [r P [_/posnumP[e] reP] |r P|r P] //=.
by exists e%:num => //= ? ? ?; apply: reP.
Qed.
Lemma
ereal_dnbhs_le_finite
(
R
: numFieldType) (
r
: R)
:
ereal_dnbhs r%:E --> nbhs r%:E.
Proof.
by move=> P [_/posnumP[e] reP] //=; exists e%:num => //= ? ? ?; exact: reP.
Qed.
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.
Proof.