Skip to content

ereals form a pseudometric type #215

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
CohenCyril merged 6 commits into from
Jun 10, 2020
Merged

ereals form a pseudometric type #215

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
4b3281e
ereals from a pseudometric type
affeldt-aist May 29, 2020
6e7ad00
divergence in R is convergence to +oo in {ereal R}
affeldt-aist May 29, 2020
021e7a1
a non-decreasing sequence of ereals converges to its sup
affeldt-aist Jun 1, 2020
25d8408
exploiting fully the monotonicity of contract and expand
CohenCyril Jun 2, 2020
ff2de7d
sup (resp. inf) of contract is contract of sup (resp. inf)
affeldt-aist Jun 2, 2020
861a90d
minor fixes
affeldt-aist Jun 9, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,16 @@
- in `classical_sets.v`, definitions for supremums: `ul`, `lb`,
`supremum`
- in `ereal.v`:
+ technical lemmas `lee_ninfty_eq`, `lee_pinfty_eq`, `lte_subl_addr`
+ technical lemmas `lee_ninfty_eq`, `lee_pinfty_eq`, `lte_subl_addr`, `eqe_oppLR`
+ lemmas about supremum: `ereal_supremums_neq0`
+ definitions:
* `ereal_sup`, `ereal_inf`
+ lemmas about `ereal_sup`:
* `ereal_sup_ub`, `ub_ereal_sup`, `ub_ereal_sup_adherent`
- in `normedtype.v`:
+ function `contract` (bijection from `{ereal R}` to `R`)
+ function `expand` (that cancels `contract`)
+ `ereal_pseudoMetricType R`

### Changed

Expand Down
21 changes: 21 additions & 0 deletions theories/ereal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -325,6 +325,8 @@ Context {R : numDomainType}.

Implicit Types (x y z : {ereal R}).

Lemma NERFin (x : R) : (- x)%R%:E = (- x%:E)%E. Proof. by []. Qed.

Lemma adde0 : right_id (0%:E : {ereal R}) +%E.
Proof. by case=> //= x; rewrite addr0. Qed.

Expand Down Expand Up @@ -352,6 +354,9 @@ move: x y => [r| |] [r'| |] //=; apply/idP/idP => [|/eqP[->]//].
by move/eqP => -[] /eqP; rewrite eqr_opp => /eqP ->.
Qed.

Lemma eqe_oppLR x y : (- x == y)%E = (x == - y)%E.
Proof. by move: x y => [r0| |] [r1| |] //=; rewrite !eqe eqr_oppLR. Qed.

End ERealArithTh_numDomainType.

Section ERealArithTh_realDomainType.
Expand Down Expand Up @@ -463,6 +468,19 @@ Qed.
Lemma ereal_supremums_set0_ninfty : supremums (@set0 {ereal R}) -oo.
Proof. by split; [exact/ubP | apply/lbP=> y _; rewrite lee_ninfty]. Qed.

Lemma supremum_pinfty S x0 : S +oo%E -> supremum x0 S = +oo%E.
Proof.
move=> Spoo; rewrite /supremum.
case: pselect => [a /= {a}|]; last by move=> S0; exfalso; apply S0; exists +oo%E.
have sSoo : supremums S +oo%E.
split; first exact: ereal_ub_pinfty.
move=> /= y; rewrite /ub => /(_ _ Spoo).
by rewrite lee_pinfty_eq => /eqP ->.
case: xgetP.
by move=> y ->{y} sSxget; move: (is_subset1_supremums sSoo sSxget).
by move/(_ +oo%E) => gSoo; exfalso; apply gSoo => {gSoo}.
Qed.

Let real_of_er_def r0 x : R := if x is r%:E then r else r0.
(* NB: see also real_of_er above *)

Expand Down Expand Up @@ -529,6 +547,9 @@ by move=> x ->{x} -[] /ubP geS _; apply geS.
by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0).
Qed.

Lemma ereal_sup_ninfty S : ereal_sup S = -oo%E -> S `<=` [set -oo%E].
Proof. by move=> supS [r /ereal_sup_ub | /ereal_sup_ub |//]; rewrite supS. Qed.

Lemma ub_ereal_sup S M : ub S M -> (ereal_sup S <= M)%E.
Proof.
rewrite /ereal_sup /supremum; case: pselect => /= [|_ _].
Expand Down
Loading