From ff2de7d67b739ac14567e5413a197cf40b2c15e1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 2 Jun 2020 17:23:08 +0900 Subject: [PATCH] sup (resp. inf) of contract is contract of sup (resp. inf) --- CHANGELOG_UNRELEASED.md | 3 + theories/normedtype.v | 124 ++++++++++++++++++++++++++++++++-------- theories/sequences.v | 5 +- 3 files changed, 105 insertions(+), 27 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index cae19b75e..688e3f66f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -15,6 +15,9 @@ * `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`) + + `ereal_pseudoMetricType R` ### Changed diff --git a/theories/normedtype.v b/theories/normedtype.v index a919c4dcc..de98e1492 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -75,6 +75,16 @@ Require Import classical_sets posnum topology prodnormedzmodule. (* ereal_loc_seq x == sequence that converges to x in the set *) (* of extended real numbers. *) (* *) +(* * Extended real numbers: *) +(* ereal_topologicalType R == topology for extended real numbers over *) +(* R, a realFieldType *) +(* contract == order-preserving bijective function *) +(* from extended real numbers to [-1;1] *) +(* 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| *) +(* *) (* --> We used these definitions to prove the intermediate value theorem and *) (* the Heine-Borel theorem, which states that the compact sets of R^n are *) (* the closed and bounded sets. *) @@ -952,7 +962,7 @@ by move/h => [y Sy] /eqP; rewrite eqe_opp => /eqP <-. Qed. Section contract_expand. -Variable R : realType. +Variable R : realFieldType. Definition contract (x : {ereal R}) : R := match x with @@ -977,21 +987,32 @@ Proof. by rewrite /contract mul0r. Qed. Lemma contractN x : contract (- x) = - contract x. Proof. by case: x => //= [r|]; [ rewrite normrN mulNr | rewrite opprK]. Qed. -Definition expand r : {ereal R} := - if r == 1 then +oo%E else (* Cyril: r >= 1 would lead to a better convention *) - if r == -1 then -oo%E else (* and r <= -1 *) - (r / (1 - `|r|))%:E. +Lemma contract_imageN (S : set {ereal R}) : + contract @` (-%E @` S) = -%R @` (contract @` 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)%E; [exists y | rewrite contractN]. +Qed. -Lemma expand1 : expand 1 = +oo%E. Proof. by rewrite /expand eqxx. Qed. +(* TODO: not exploited yet: expand is nondecreasing everywhere so it should be + possible to use some of the homoRL/homoLR lemma where monoRL/monoLR do not + apply *) +Definition expand r : {ereal R} := + if r >= 1 then +oo%E else if r <= -1 then -oo%E else (r / (1 - `|r|))%:E. -Lemma expandN1 : expand (-1) = -oo%E. -Proof. by rewrite /expand -subr_eq0 -opprD oppr_eq0 gt_eqF // eqxx. Qed. +Lemma expand1 x : 1 <= x -> expand x = +oo%E. +Proof. by move=> x1; rewrite /expand x1. Qed. -Lemma expand0 : expand 0 = 0%:E. +Lemma expandN1 x : x <= -1 -> expand x = -oo%E. Proof. -by rewrite /expand eq_sym oner_eq0 -eqr_oppLR oppr0 eq_sym oner_eq0 mul0r. +move=> x1; rewrite /expand x1 ifF //; apply/negP => /le_trans/(_ x1). +by apply/negP; rewrite -ltNge -subr_gt0 opprK. Qed. +Lemma expand0 : expand 0 = 0%:E. +Proof. by rewrite /expand leNgt ltr01 /= oppr_ge0 leNgt ltr01 /= mul0r. Qed. + (* Cyril: TODO: add to ssrnum *) Lemma nlt_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false). Proof. @@ -1001,9 +1022,10 @@ Qed. Lemma expandK : {in [pred x | `|x| <= 1], cancel expand contract}. Proof. -move=> x. rewrite inE le_eqVlt => /orP[|x1]. - by rewrite eqr_norml => /andP[/orP[]/eqP->{x}]; rewrite ?(expand1,expandN1). -rewrite /expand nlt_eqF // nlt_eqF //. +move=> x; rewrite inE le_eqVlt => /orP[|x1]. + rewrite eqr_norml => /andP[/orP[]/eqP->{x}] _; + by [rewrite expand1|rewrite expandN1]. +rewrite /expand 2!leNgt ltr_oppl; case/ltr_normlP : (x1) => -> -> /=. have x_pneq0 : 1 + x / (1 - x) != 0. rewrite -[X in X + _](@divrr _ (1 - x)) -?mulrDl; last first. by rewrite unitfE subr_eq0 eq_sym nlt_eqF. @@ -1016,7 +1038,7 @@ wlog : x x1 x_pneq0 x_nneq0 / 0 <= x => wlog_x0. have [x0|x0] := lerP 0 x; first by rewrite wlog_x0. move: (wlog_x0 (- x)). rewrite !(normrN,opprK,mulNr) oppr_ge0 => /(_ x1 x_nneq0 x_pneq0 (ltW x0)). - by move=> /eqP; rewrite NERFin contractN eqr_opp => /eqP. + by move/eqP; rewrite eqr_opp => /eqP. rewrite /contract !ger0_norm //; last first. by rewrite divr_ge0 // subr_ge0 (le_trans _ (ltW x1)) // ler_norm. apply: (@mulIr _ (1 + x / (1 - x))); first by rewrite unitfE. @@ -1051,7 +1073,9 @@ Definition lt_expand := leW_mono_in le_expand. Definition expand_inj := mono_inj_in lexx le_anti le_expand. Lemma real_of_er_expand x : `|x| < 1 -> (real_of_er (expand x))%:E = expand x. -Proof. by move=> x1; rewrite /expand nlt_eqF // nlt_eqF. Qed. +Proof. +by move=> x1; rewrite /expand 2!leNgt ltr_oppl; case/ltr_normlP : x1 => -> ->. +Qed. Lemma contractK : cancel contract expand. Proof. @@ -1079,7 +1103,6 @@ Definition le_contractRL := monoRL_in Definition lt_contractRL := monoRL_in (onW_can_in predT expandK) (fun x _ => isT) (in2W lt_contract). - Lemma contract_eq0 x : (contract x == 0) = (x == 0%:E). Proof. by rewrite -(can_eq contractK) contract0. Qed. @@ -1089,22 +1112,73 @@ Proof. by rewrite -(can_eq contractK). Qed. Lemma contract_eq1 x : (contract x == 1) = (x == +oo%E). Proof. by rewrite -(can_eq contractK). Qed. -Lemma expand_eqoo (r : R) : (expand r == +oo%E) = (r == 1). -Proof. -apply/eqP/eqP => [|->]; last by rewrite expand1. -by rewrite /expand; do![case: (altP eqP) => ?]. -Qed. +Lemma expand_eqoo (r : R) : (expand r == +oo%E) = (1 <= r). +Proof. by rewrite /expand; case: ifP => //; case: ifP. Qed. -Lemma expand_eqNoo (r : R) : (expand r == -oo%E) = (r == -1). +Lemma expand_eqNoo (r : R) : (expand r == -oo%E) = (r <= -1). Proof. -apply/eqP/eqP => [|->]; last by rewrite expandN1. -by rewrite /expand; do![case: (altP eqP) => ?]. +rewrite /expand; case: ifP => /= r1; last by case: ifP. +by apply/esym/negbTE; rewrite -ltNge (lt_le_trans _ r1) // -subr_gt0 opprK. Qed. End contract_expand. -Section ereal_PseudoMetric. +Section contract_expand_realType. Variable R : realType. + +Let contract := @contract R. + +Lemma sup_contract_le1 S : S !=set0 -> `|sup (contract @` S)| <= 1. +Proof. +case=> x Sx; rewrite ler_norml; apply/andP; split; last first. + apply sup_le_ub; first by exists (contract x), x. + by move=> r [y Sy] <-; case/ler_normlP : (contract_le1 y). +rewrite (@le_trans _ _ (contract x)) //. + by case/ler_normlP : (contract_le1 x); rewrite ler_oppl. +apply sup_ub; last by exists x. +by exists 1 => r [y Sy <-]; case/ler_normlP : (contract_le1 y). +Qed. + +Lemma contract_sup S : S !=set0 -> contract (ereal_sup S) = sup (contract @` S). +Proof. +move=> S0; apply/eqP; rewrite eq_le; apply/andP; split; last first. + apply sup_le_ub. + by case: S0 => x Sx; exists (contract x), x. + move=> x [y Sy] <-{x}; rewrite le_contract; exact/ereal_sup_ub. +rewrite leNgt; apply/negP. +set supc := sup _; set csup := contract _; move=> ltsup. +suff [y [ysupS ?]] : exists y, (y < ereal_sup S)%E /\ ub S y. + have : (ereal_sup S <= y)%E by apply ub_ereal_sup. + by move/(lt_le_trans ysupS); rewrite ltxx. +suff [x [? [ubSx x1]]] : exists x, x < csup /\ ub (contract @` S) x /\ `|x| <= 1. + exists (expand x); split => [|y Sy]. + by rewrite -(contractK (ereal_sup S)) lt_expand // inE // contract_le1. + rewrite -(contractK y) le_expand // ?inE ?contract_le1 //. + by apply ubSx; exists y. +exists ((supc + csup) / 2); split; first by rewrite midf_lt. +split => [r [y Sy <-{r}]|]. + rewrite (@le_trans _ _ supc) ?midf_le //; last by rewrite ltW. + apply sup_ub; last by exists y. + by exists 1 => r [z Sz <-]; case/ler_normlP : (contract_le1 z). +rewrite ler_norml; apply/andP; split; last first. + rewrite ler_pdivr_mulr // mul1r (_ : 2 = 1 + 1) // ler_add //. + by case/ler_normlP : (sup_contract_le1 S0). + by case/ler_normlP : (contract_le1 (ereal_sup S)). +rewrite ler_pdivl_mulr // (_ : 2 = 1 + 1) // mulN1r opprD ler_add //. +by case/ler_normlP : (sup_contract_le1 S0); rewrite ler_oppl. +by case/ler_normlP : (contract_le1 (ereal_sup S)); rewrite ler_oppl. +Qed. + +Lemma contract_inf S : S !=set0 -> contract (ereal_inf S) = inf (contract @` S). +Proof. +move=> -[x Sx]; rewrite /ereal_inf /contract (contractN (ereal_sup (-%E @` S))). +by rewrite -/contract contract_sup /inf; [rewrite contract_imageN | exists (- x)%E, x]. +Qed. + +End contract_expand_realType. + +Section ereal_PseudoMetric. +Variable R : realFieldType. Implicit Types x y : {ereal R}. Definition ereal_ball x (e : R) y := `|contract x - contract y| < e. diff --git a/theories/sequences.v b/theories/sequences.v index 68f633e21..1ee2e6ba4 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -771,11 +771,12 @@ have [/eqP {lnoo}loo|lpoo] := boolP (l == +oo%E). near: n. suff [n Hn] : exists n, (expand (contract +oo - (e)%:num)%R < u_ n)%E. by exists n => // m nm; rewrite (lt_le_trans Hn) //; apply nd_u_. - apply/existsP => abs. + apply/existsPN => abs. have : (l <= expand (contract +oo - (e)%:num)%R)%E. apply: ub_ereal_sup => x [n _ <-{x}]. rewrite leNgt; apply/negP/abs. - by rewrite loo lee_pinfty_eq expand_eqoo lt_eqF // ltr_subl_addr ltr_addl. + rewrite loo lee_pinfty_eq expand_eqoo ler_sub_addr addrC -ler_sub_addr. + by rewrite subrr; apply/negP; rewrite -ltNge. have [e1|e1] := ltrP 1 e%:num. by rewrite ler_subl_addr (le_trans (ltW e2)). by rewrite ler_subl_addr ler_addl.