From 4b3281e45c570ca3ee21659b09e8ba8707f250d2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 29 May 2020 22:42:40 +0900 Subject: [PATCH 1/6] ereals from a pseudometric type --- theories/normedtype.v | 672 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 672 insertions(+) diff --git a/theories/normedtype.v b/theories/normedtype.v index f054d3b715..11e295da38 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -787,6 +787,678 @@ Hint Extern 0 (is_true (0 < _)) => match goal with H : ?x \is_near (locally +oo) |- _ => solve[near: x; exists 0 => _/posnumP[x] //] end : core. +Lemma locallyNe (R : realFieldType) (x : {ereal R}) : + locally (- x)%E = [set [set (- y)%E | y in A] | A in locally x]. +Proof. +case: x => [r /=| |]. +- rewrite predeqE => S; split => [[_/posnumP[e] reS]|[S' [_ /posnumP[e] reS' <-]]]. + exists (-%E @` S). + exists e%:num => // x rex; exists (- x%:E)%E; last by rewrite oppeK. + by apply reS; rewrite /= opprK -normrN opprD opprK. + rewrite predeqE => s; split => [[y [z Sz] <- <-]|Ss]. + by rewrite oppeK. + by exists (- s)%E; [exists s | rewrite oppeK]. + exists e%:num => // x rex; exists (- x%:E)%E; last by rewrite oppeK. + by apply reS'; rewrite /= opprK -normrN opprD. +- rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]]. + exists (-%E @` S). + exists (- M); rewrite realN Mreal; split => // x Mx. + by exists (- x)%E; [apply MS; rewrite lte_oppl | rewrite oppeK]. + rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK. + by exists (- x)%E; [exists x | rewrite oppeK]. + exists (- M); rewrite realN; split => // y yM. + exists (- y)%E; by [apply Mx; rewrite lte_oppr|rewrite oppeK]. +- rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]]. + exists (-%E @` S). + exists (- M); rewrite realN Mreal; split => // x Mx. + by exists (- x)%E; [apply MS; rewrite lte_oppr | rewrite oppeK]. + rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK. + by exists (- x)%E; [exists x | rewrite oppeK]. + exists (- M); rewrite realN; split => // y yM. + exists (- y)%E; by [apply Mx; rewrite lte_oppl|rewrite oppeK]. +Qed. + +Lemma locallyNKe (R : realFieldType) (z : {ereal R}) (A : set {ereal R}) : + locally (- z)%E (-%E @` A) -> locally z A. +Proof. +rewrite locallyNe => -[S zS] SA; rewrite -(oppeK z) locallyNe. +exists (-%E @` S); first by rewrite locallyNe; exists S. +rewrite predeqE => x; split => [[y [u Su <-{y} <-]]|Ax]. + rewrite oppeK. + move: SA; rewrite predeqE => /(_ (- u)%E) [h _]. + have : (exists2 y : {ereal R}, S y & (- y)%E = (- u)%E) by exists u. + by move/h => -[y Ay] /eqP; rewrite eqe_opp => /eqP <-. +exists (- x)%E; last by rewrite oppeK. +exists x => //. +move: SA; rewrite predeqE => /(_ (- x)%E) [_ h]. +have : (-%E @` A) (- x)%E by exists x. +by move/h => [y Sy] /eqP; rewrite eqe_opp => /eqP <-. +Qed. + +Section contract_expand. +Variable R : realType. + +Definition contract (x : {ereal R}) : R := + match x with + | r%:E => r / (1 + `|r|) | +oo%E => 1 | -oo%E => -1 + end. + +Lemma contract_lt1 x : `|contract x%:E| < 1. +Proof. +rewrite /= normrM normrV ?unitfE //; last first. + rewrite eq_sym lt_eqF // -ltr_subl_addr sub0r (@le_lt_trans _ _ 0) //. + by rewrite -ler_oppl oppr0. +rewrite ltr_pdivr_mulr // ?mul1r; last first. + by rewrite gtr0_norm (@lt_le_trans _ _ 1) // ler_addl. +by rewrite [X in _ < X]gtr0_norm ?ltr_addr// (@lt_le_trans _ _ 1)// ler_addl. +Qed. + +Lemma contract_le1 x : `|contract x| <= 1. +Proof. +by case: x => [x| |] /=; rewrite ?normrN1 ?normr1 // (ltW (contract_lt1 _)). +Qed. + +Lemma contractN x : contract (- x) = - contract x. +Proof. by case: x => //= [r|]; [ rewrite normrN mulNr | rewrite opprK]. Qed. + +Lemma contract0 : contract 0%:E = 0. +Proof. by rewrite /contract mul0r. Qed. + +Lemma contract_eq0 r : (contract r == 0) = (r == 0%:E). +Proof. +case: r => [r| |] /=. +- apply/idP/idP => [|/eqP[->]]; last by rewrite mul0r. + rewrite mulf_eq0 => /orP[/eqP -> //|]. + rewrite invr_eq0 eq_sym -subr_eq add0r -eqr_opp opprK => r1. + by move: (normr_ge0 r); rewrite (eqP r1) /= oppr_ge0 leNgt /= ltr01. +- exact/idP/idP. +- by rewrite -eqr_opp opprK oppr0 oner_eq0. +Qed. + +Definition expand r : {ereal R} := + if r == 1 then +oo%E else + if r == -1 then -oo%E else + (r / (1 - `|r|))%:E. + +Lemma expand0 : expand 0 = 0%:E. +Proof. +by rewrite /expand eq_sym oner_eq0 -eqr_oppLR oppr0 eq_sym oner_eq0 mul0r. +Qed. + +Lemma contractK : cancel contract expand. +Proof. +case=> [r| |]; rewrite /expand /= ?eqxx //. +- rewrite (_ : _ == 1 = false); last first. + apply/negP => /eqP/divr1_eq; apply/eqP; rewrite lt_eqF //. + by rewrite -{1}(add0r r) ltr_le_add // real_ler_norm // num_real. + rewrite (_ : _ == -1 = false); last first. + apply/negP; rewrite -eqr_oppLR -mulrN -invrN => /eqP/divr1_eq/eqP. + rewrite -eqr_oppLR lt_eqF // -{1}(add0r (- r)) ltr_le_add //. + by rewrite real_ler_normr ?num_real // lexx orbT. + congr (_ %:E). + have ? : 1 + `|r| != 0 by rewrite lt0r_neq0 // -(addr0 0) ltr_le_add. + rewrite -[RHS]mulr1 -mulrA; congr (r * _). + rewrite normrM normrV ?unitfE // (@ger0_norm _ (1 + `|r|)) ?addr_ge0 //. + rewrite -{2}(@divrr _ (1 + `|r|)) ?unitfE // -mulrBl invrM; last 2 first. + by rewrite addrK unitfE. + by rewrite unitfE invr_eq0. + by rewrite invrK mulrA mulVr ?unitfE // addrK divr1. +- rewrite eq_sym -subr_eq0 opprK {1 2}(_ : 1 = 1%:R) // -natrD /= addn1 /=. + by rewrite (_ : _ == 0 = false) //; apply/negP/negP. +Qed. + +Lemma lt1_neq1 (x : R) : `|x| < 1 -> x == 1 = false. +Proof. by move=> x1; rewrite lt_eqF // (le_lt_trans (ler_norm _) x1). Qed. + +Lemma lt1_neqN1 (x : R) : `|x| < 1 -> x == -1 = false. +Proof. by rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF. Qed. + +Lemma expandK : {in [pred x | `|x| <= 1], cancel expand contract}. +Proof. +move=> x; rewrite inE => x1; rewrite /expand /contract. +move: x1; rewrite le_eqVlt => /orP[|x1]. + have [x0|x0] := lerP 0 x. + by rewrite ger0_norm // => x1; rewrite x1; apply/esym/eqP. + rewrite ltr0_norm // eqr_oppLR => /eqP ->. + by rewrite eqxx eq_sym -subr_eq0 opprK (_ : 1 = 1%:R) // -natrD pnatr_eq0. +rewrite lt1_neq1 // lt1_neqN1 //. +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 lt1_neq1. + by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym lt1_neq1. +have x_nneq0 : 1 - x / (1 + x) != 0. + rewrite -[X in X + _](@divrr _ (1 + x)) -?mulrBl; last first. + by rewrite unitfE addrC addr_eq0 lt1_neqN1. + by rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym lt1_neqN1. +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 eqr_opp => /eqP. +rewrite !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. +rewrite -(mulrA (x / _)) mulVr ?unitfE // mulr1. +rewrite -[X in X + _ / _](@divrr _ (1 - x)) -?mulrDl ?subrK ?div1r //. +by rewrite unitfE subr_eq0 eq_sym lt1_neq1. +Qed. + +Lemma bijective_contract : {on [pred x| `|x| <= 1], bijective contract}. +Proof. exists expand; [by move=> x _; rewrite contractK | exact: expandK]. Qed. + +Lemma contract_preserves_order : {homo contract : x y / (x < y)%O}. +Proof. +move=> -[r0 | | ] [r1 | _ | _ ] //=. +- rewrite lte_fin => r0r1; rewrite ltr_pdivr_mulr; last first. + by rewrite -(addr0 0) ltr_le_add. + rewrite mulrAC ltr_pdivl_mulr 2?mulrDr 2?mulr1; last first. + by rewrite -(addr0 0) ltr_le_add. + have [r10|r10] := lerP 0 r1. + rewrite ger0_norm //. + have [r00|r00] := lerP 0 r0. + move: r00 r0r1; rewrite le_eqVlt => /orP[/eqP <-|r00]. + by rewrite add0r mul0r normr0 mulr0 addr0. + by move=> r0r1; rewrite gtr0_norm // mulrC ltr_add2r. + move: r10 r0r1; rewrite le_eqVlt => /orP[/eqP <-|r10 r0r1]. + by rewrite mulr0 addr0 add0r mul0r. + rewrite ltr0_norm // ltr_add // (@lt_trans _ _ 0) //. + by rewrite nmulr_rlt0. + by rewrite pmulr_lgt0 // oppr_gt0. + rewrite ltr0_norm //. + have [r00|r00] := lerP 0 r0. + by move: (le_lt_trans r00 r0r1) => /(lt_trans r10); rewrite ltxx. + by rewrite ltr0_norm // mulrC mulrN -mulNr ltr_add2r. +- rewrite ltr_pdivr_mulr; last by rewrite -(addr0 0) ltr_le_add. + by rewrite mul1r -{1}(add0r r0) ltr_le_add // ler_norm. +- rewrite ltr_pdivl_mulr ?mulN1r; last by rewrite -(addr0 0) ltr_le_add. + by rewrite ltr_oppl -(add0r (- r1)) ltr_le_add // -(normrN r1) ler_norm. +- by rewrite -subr_gt0 opprK (_ : 1 = 1%:R). +Qed. + +Lemma contract_preserves_le_order : {homo contract : x y / (x <= y)%O}. +Proof. exact/ltW_homo/contract_preserves_order. Qed. + +Lemma expand_preserves_order : + {in [pred x| `|x| <= 1] & [pred x| `|x| <= 1], {homo expand : x y / (x < y)%O}}. +Proof. +move=> x y; rewrite !inE => x1 y1 xy; rewrite /expand. +move: x1; rewrite le_eqVlt => /orP[|x1]. + have [x0|x0] := lerP 0 x. + rewrite ger0_norm // => x1; exfalso. + move: xy; rewrite (eqP x1) ltNge => /negP; apply. + by rewrite (le_trans _ y1) // ler_norm. + rewrite ltr0_norm // eqr_oppLR => x1. + rewrite (eqP x1) eqxx eq_sym -subr_eq0 opprK (_ : 1 = 1%:R) // -natrD. + rewrite pnatr_eq0 //=; case: ifPn => // y_neq1. + rewrite -mulNrn -mulr_natr mulr1 ifF; last first. + apply: contraNF y_neq1 => y_eq1. + by move: xy; rewrite (eqP x1) (eqP y_eq1) ltxx. + by rewrite lte_ninfty. +move: y1; rewrite le_eqVlt => /orP[|y1]. + have [y0|y0] := lerP 0 y. + rewrite ger0_norm // => y1; rewrite y1. + by rewrite lt1_neq1 // lt1_neqN1 // lte_pinfty. + rewrite ltr0_norm // eqr_oppLR => y1; exfalso. + move: xy; rewrite (eqP y1) {y1 y0} ltNge => /negP; apply. + have [x0|x0] := lerP 0 x. + by rewrite (le_trans _ x0) // ler_oppl oppr0. + rewrite ltr0_norm // ltr_oppl in x1. + exact: ltW. +rewrite !lt1_neq1 // !lt1_neqN1 //. +have [x0|x0] := lerP 0 x. + move: (x0); rewrite le_eqVlt => /orP[/eqP <-|{x0}x0]. + by rewrite mul0r lte_fin divr_gt0 // ?subr_gt0 // (le_lt_trans x0). + rewrite lte_fin gtr0_norm // gtr0_norm; last by rewrite (lt_trans x0). + rewrite ltr_pdivr_mulr; last first. + by rewrite subr_gt0 (le_lt_trans _ x1) // ler_norm. + rewrite mulrAC -ltr_pdivr_mulr; last first. + by rewrite invr_gt0 // subr_gt0 (le_lt_trans _ y1) // ler_norm. + by rewrite invrK !(mulrBr,mulr1) mulrC ltr_le_sub. +rewrite ltr0_norm // opprK lte_fin ltr_pdivr_mulr; last first. + by rewrite -ltr_subl_addr sub0r -(ltr0_norm x0). +rewrite mulrAC -ltr_pdivr_mulr; last by rewrite invr_gt0 subr_gt0. +rewrite invrK. +have [|y0] := lerP 0 y. + rewrite le_eqVlt => /orP[/eqP <-|y0]. + by rewrite normr0 mul0r subr0 mulr1. + rewrite gtr0_norm // (@le_lt_trans _ _ 0) //. + rewrite mulrC nmulr_lle0 // subr_ge0 ltW //. + by rewrite (le_lt_trans _ y1) // ler_norm. + rewrite mulr_gt0 // -ltr_subl_addl sub0r ltr_oppl. + by rewrite (le_lt_trans _ x1) // ler0_norm // ltW. +by rewrite ltr0_norm // opprK !mulrDr !mulr1 mulrC ltr_add2r. +Qed. + +Lemma real_of_er_expand x : `|x| < 1 -> (real_of_er (expand x))%:E = expand x. +Proof. by move=> x1; rewrite /expand lt1_neq1 // lt1_neqN1. Qed. + +End contract_expand. + +Section ereal_PseudoMetric. +Variable R : realType. +Implicit Types x y : {ereal R}. + +Definition ereal_ball x (e : R) y := `|contract x - contract y| < e. + +Lemma ereal_ball_center x (e : R) : 0 < e -> ereal_ball x e x. +Proof. by move=> e0; rewrite /ereal_ball subrr normr0. Qed. + +Lemma ereal_ball_sym x y (e : R) : ereal_ball x e y -> ereal_ball y e x. +Proof. by rewrite /ereal_ball distrC. Qed. + +Lemma ereal_ball_triangle x y z (e1 e2 : R) : + ereal_ball x e1 y -> ereal_ball y e2 z -> ereal_ball x (e1 + e2) z. +Proof. +rewrite /ereal_ball => h1 h2; rewrite -[X in X - _](subrK (contract y)) -addrA. +by rewrite (le_lt_trans (ler_norm_add _ _)) // ltr_add. +Qed. + +Lemma locally_oo_up_e1 (A : set {ereal R}) (e : {posnum R}) : + (fun y : {ereal R} => `|1 - contract y| < (e)%:num) `<=` A -> + (e)%:num <= 1 -> + locally +oo%E A. +Proof. +move=> reA e1. +exists (real_of_er (expand (1 - e%:num))); split; first by rewrite num_real. +case => [r | | //]. +- rewrite real_of_er_expand; last first. + by rewrite ger0_norm ?ltr_subl_addl ?ltr_addr // subr_ge0. + move=> h; apply reA; rewrite gtr0_norm ?subr_gt0; last first. + by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. + rewrite ltr_subl_addl addrC -ltr_subl_addl -[X in X < _]expandK; last first. + by rewrite inE ger0_norm ?ler_subl_addl ?ler_addr // subr_ge0. + exact: contract_preserves_order. +- by move=> _; apply reA; rewrite /= subrr normr0. +Qed. + +Lemma locally_oo_down_e1 (A : set {ereal R}) (e : {posnum R}) : + (fun y : {ereal R} => `|-1 - contract y| < (e)%:num) `<=` A -> + (e)%:num <= 1 -> + locally -oo%E A. +Proof. +move=> reA e1. +suff h : locally +oo%E ((fun x : {ereal R} => - x)%E @` A). + rewrite (_ : -oo = - +oo)%E // locallyNe. + exists (-%E @` A) => //. + rewrite predeqE => x; split=> [[y [z Az <- <-]]|Ax]; rewrite ?oppeK //. + exists (- x)%E; last by rewrite oppeK. + by exists x. +apply (@locally_oo_up_e1 _ e) => // x x1e; exists (- x)%E; last by rewrite oppeK. +by apply reA; rewrite contractN opprK -normrN opprD opprK. +Qed. + +Lemma locally_oo_up_1e (A : set {ereal R}) (e : {posnum R}) : + (fun y : {ereal R} => `|1 - contract y| < (e)%:num) `<=` A -> + 1 < (e)%:num -> + locally +oo%E A. +Proof. +move=> reA e1. +have [e2{e1}|e2] := ltrP 2 e%:num. + suff -> : A = setT by exists 0; rewrite real0. + rewrite predeqE => x; split => // _; apply reA. + rewrite (le_lt_trans _ e2) // (le_trans (ler_norm_sub _ _)) // normr1. + by rewrite addrC -ler_subr_addr (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1) // addrK. +have /andP[e10 e11] : 0 < e%:num - 1 <= 1 by rewrite subr_gt0 e1 /= ler_subl_addl. +apply locallyNKe. +have : (PosNum e10)%:num <= 1 by []. +move/(@locally_oo_down_e1 (-%E @` A) (PosNum e10)); apply. +move=> y ye; exists (- y)%E; last by rewrite oppeK. +apply reA. +rewrite contractN opprK. +rewrite -opprB opprK normrN addrC in ye. +move/lt_le_trans : ye; apply. +by rewrite (le_trans e11) // ltW. +Qed. + +Lemma locally_oo_down_1e (A : set {ereal R}) (e : {posnum R}) : + (fun y : {ereal R} => `|-1 - contract y| < (e)%:num) `<=` A -> + 1 < (e)%:num -> + locally -oo%E A. +Proof. +move=> reA e1. +have [e2{e1}|e2] := ltrP 2 e%:num. + suff -> : A = setT by exists 0; rewrite real0. + rewrite predeqE => x; split => // _; apply reA. + rewrite (le_lt_trans _ e2) // -opprB normrN opprK (le_trans (ler_norm_add _ _)) // normr1. + by rewrite -ler_subr_addr (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1) // addrK. +have /andP[e10 e11] : 0 < e%:num - 1 <= 1 by rewrite subr_gt0 e1 /= ler_subl_addl. +apply locallyNKe. +have : (PosNum e10)%:num <= 1 by []. +move/(@locally_oo_up_e1 (-%E @` A) (PosNum e10)); apply. +move=> y ye; exists (- y)%E; last by rewrite oppeK. +apply reA. +rewrite contractN -opprD normrN. +move/lt_le_trans : ye; apply. +by rewrite (le_trans e11) // ltW. +Qed. + +Lemma locally_fin_out_above (r : R) (e : {posnum R}) (A : set {ereal R}) : + (fun y : {ereal R} => `|contract r%:E - contract y| < (e)%:num) `<=` A -> + - 1 < contract r%:E - e%:num -> + 1 <= contract r%:E + (e)%:num -> + locally r%:E A. +Proof. +move=> reA reN1 re1. +have X : `|contract r%:E - (e)%:num| < 1. + rewrite ltr_norml reN1 andTb ltr_subl_addl (@le_lt_trans _ _ 1) // ?ltr_addr //. + by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. +pose e' := r - real_of_er (expand (contract r%:E - e%:num)). +have e'0 : 0 < e'. + rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E) real_of_er_expand //. + apply: (expand_preserves_order _ (contract_le1 _)); first by rewrite inE ltW. + by rewrite ltr_subl_addl ltr_addr. +apply/locallyP; exists e' => // r' re'r'; apply reA. +rewrite /ball /= in re'r'. +have [rr'|r'r] := lerP r r'. + move: rr'; rewrite le_eqVlt => /orP[/eqP->|rr']; first by rewrite subrr normr0. + rewrite ltr0_norm ?subr_lt0// opprB in re'r'. + rewrite ltr0_norm; last first. + by rewrite subr_lt0; apply: contract_preserves_order; rewrite lte_fin. + rewrite opprB ltr_subl_addl (lt_le_trans _ re1) //. + by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. +rewrite gtr0_norm ?subr_gt0 //; last first. + by apply: contract_preserves_order; rewrite lte_fin. +move: re'r'. +rewrite gtr0_norm // ?subr_gt0// /e'. +rewrite -ltr_subl_addl addrAC subrr add0r ltr_oppl opprK -lte_fin real_of_er_expand //. +rewrite -[in X in X -> _](contractK r'%:E) => /contract_preserves_order r'e'r. +rewrite expandK in r'e'r; last by rewrite inE ltW. +rewrite expandK in r'e'r; last by rewrite inE contract_le1. +by rewrite ltr_subl_addl addrC -ltr_subl_addl. +Qed. + +Lemma locally_fin_out_below (r : R) (e : {posnum R}) (A : set {ereal R}) : + (fun y : {ereal R} => `|contract r%:E - contract y| < (e)%:num) `<=` A -> + contract r%:E - (e)%:num <= - 1 -> + contract r%:E + (e)%:num < 1 -> + locally r%:E A. +Proof. +move=> reA reN1 re1. +have ? : `|contract r%:E + (e)%:num| < 1. + rewrite ltr_norml re1 andbT (@lt_le_trans _ _ (contract r%:E)) // ?ler_addl //. + by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. +pose e' : R := real_of_er (expand (contract r%:E + e%:num)) - r. +have e'0 : 0 < e'. + rewrite /e'. + rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E) real_of_er_expand //. + apply: (expand_preserves_order (contract_le1 _)); last by rewrite ltr_addl. + by rewrite inE ltW. +apply/locallyP; exists e' => // r' r'e'r; apply reA. +rewrite /ball /= in r'e'r. +have [rr'|r'r] := lerP r r'. + move: rr'; rewrite le_eqVlt => /orP[/eqP->|rr']. + by rewrite subrr normr0. + rewrite ltr0_norm ?subr_lt0// opprB in r'e'r. + rewrite ltr0_norm; last first. + by rewrite subr_lt0; apply: contract_preserves_order; rewrite lte_fin. + rewrite opprB; move: r'e'r. + rewrite /e' -ltr_subl_addr opprK subrK -lte_fin real_of_er_expand //. + move=> r'e'r; rewrite ltr_subl_addl. + by move/contract_preserves_order : r'e'r; rewrite expandK // inE ltW. +rewrite gtr0_norm; last first. + by rewrite subr_gt0; apply contract_preserves_order; rewrite lte_fin. +rewrite ltr_subl_addl addrC -ltr_subl_addl (le_lt_trans reN1) //. +by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. +Qed. + +Lemma locally_fin_out_above_below (r : R) (e : {posnum R}) (A : set {ereal R}) : + (fun y : {ereal R} => `|contract r%:E - contract y| < (e)%:num) `<=` A -> + contract r%:E - e%:num < -1 -> + 1 < contract r%:E + (e)%:num -> + locally r%:E A. +Proof. +move=> reA reN1 re1; suff : A = setT by move=> ->; exists 1. +rewrite predeqE => x; split => // _; apply reA. +case: x => [r'| |] //. +- have [|r'r] := lerP r r'. + rewrite le_eqVlt => /orP[/eqP <-|rr']. + by rewrite subrr normr0. + rewrite ltr0_norm; last first. + by rewrite subr_lt0; apply: contract_preserves_order; rewrite lte_fin. + rewrite opprB ltr_subl_addl (le_lt_trans _ re1) //. + by move: (contract_le1 r'%:E); rewrite ler_norml => /andP[]. + rewrite gtr0_norm; last first. + by rewrite subr_gt0; apply contract_preserves_order; rewrite lte_fin. + rewrite ltr_subl_addl addrC -ltr_subl_addl (lt_le_trans reN1) //. + by move: (contract_le1 r'%:E); rewrite ler_norml => /andP[]. +- rewrite [contract +oo]/= ler0_norm; last first. + by rewrite subr_le0; move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. + by rewrite opprB ltr_subl_addl. +- rewrite [contract -oo]/= ger0_norm; last first. + by rewrite subr_ge0; move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. + by rewrite ltr_subl_addl addrC -ltr_subl_addl. +Qed. + +Lemma locally_fin_inbound (r : R) (e : {posnum R}) (A : set {ereal R}) : + (fun y : {ereal R} => `|contract r%:E - contract y| < (e)%:num) `<=` A -> + locally r%:E A. +Proof. +move=> reA. +have [|reN1] := boolP (contract r%:E - e%:num == -1). + rewrite subr_eq addrC => /eqP reN1. + have [re1|] := boolP (contract r%:E + e%:num == 1). + move/eqP : reN1; rewrite -(eqP re1) opprD addrCA subrr addr0 -subr_eq0. + rewrite opprK -mulr2n mulrn_eq0 orFb contract_eq0 => /eqP[r0]. + move: re1; rewrite r0 contract0 add0r => /eqP e1. + exists 1 => // r' /=; rewrite sub0r normrN => r'1. + by apply reA; rewrite r0 contract0 sub0r normrN e1 contract_lt1. + rewrite neq_lt => /orP[re1|re1]. + by apply (@locally_fin_out_below _ e) => //; rewrite reN1 addrAC subrr sub0r. + have e1 : 1 < e%:num. + move: re1; rewrite reN1 addrAC ltr_subr_addl -!mulr2n -(mulr_natl e%:num). + by rewrite -{1}(mulr1 2) => ?; rewrite -(@ltr_pmul2l _ 2). + have Aoo : setT `\ -oo%E `<=` A. + move=> x [_]; rewrite /set1 /= => xnoo; apply reA. + case: x xnoo => [r' _ | |//]. + have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E). + rewrite reN1 opprB addrA ltr_subl_addl ler_lt_add // (le_trans _ (ltW e1)) //. + by case/ler_normlP : (contract_le1 r'%:E). + rewrite reN1 -addrA -[X in _ < X]addr0 ltr_add2l ltr_subl_addl addr0. + by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. + rewrite [contract +oo]/= ltr0_norm ?subr_lt0; last first. + by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. + by rewrite opprB reN1 opprB addrA ltr_subl_addl ltr_add. + have : locally r%:E (setT `\ -oo%E) by exists 1. + case => _/posnumP[e'] /=; rewrite /ball_ => h. + by exists e'%:num => // y /h; apply: Aoo. +move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1]. + have [/eqP re1|re1] := boolP (contract r%:E + e%:num == 1). + by apply (@locally_fin_out_above _ e) => //; rewrite re1. + move: re1; rewrite neq_lt => /orP[re1|re1]. + have ? : `|contract r%:E - (e)%:num| < 1. + rewrite ltr_norml reN1 andTb ltr_subl_addl (@lt_le_trans _ _ 1) // ?ler_addr //. + by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. + have ? : `|contract r%:E + (e)%:num| < 1. + rewrite ltr_norml re1 andbT -(addr0 (-1)) ler_lt_add //. + by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. + pose e' : R := minr (r - real_of_er (expand (contract r%:E - e%:num))) + (real_of_er (expand (contract r%:E + e%:num)) - r). + have e'0 : 0 < e'. + rewrite /e' ltxI; apply/andP; split. + rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E) real_of_er_expand //. + apply: (expand_preserves_order _ (contract_le1 _)); first by rewrite inE ltW. + by rewrite ltr_subl_addl ltr_addr. + rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E) real_of_er_expand //. + apply: (expand_preserves_order (contract_le1 _)); last by rewrite ltr_addl. + by rewrite inE ltW. + apply/locallyP; exists e' => // r' re'r'; apply reA. + rewrite /ball /= in re'r'. + have [|r'r] := lerP r r'. + rewrite le_eqVlt => /orP[/eqP->|rr']. + by rewrite subrr normr0. + rewrite ltr0_norm ?subr_lt0// opprB in re'r'. + rewrite ltr0_norm; last first. + by rewrite subr_lt0; apply: contract_preserves_order; rewrite lte_fin. + rewrite opprB; move: re'r'. + rewrite /e' ltxI => /andP[_]. + rewrite -ltr_subl_addr opprK subrK -lte_fin real_of_er_expand //. + move=> r'e'r; rewrite ltr_subl_addl. + by move/contract_preserves_order : r'e'r; rewrite expandK // inE ltW. + move: re'r'; rewrite ltxI => /andP[]. + rewrite gtr0_norm ?subr_gt0 // -ltr_subl_addl addrAC subrr add0r ltr_oppl. + rewrite opprK -lte_fin real_of_er_expand // => r'e'r _. + rewrite gtr0_norm; last first. + by rewrite subr_gt0; apply contract_preserves_order; rewrite lte_fin. + rewrite ltr_subl_addl addrC -ltr_subl_addl. + by move/contract_preserves_order : r'e'r; rewrite expandK // inE ltW. + by apply (@locally_fin_out_above _ e) => //; rewrite ltW. +have [re1|re1] := ltrP 1 (contract r%:E + (e)%:num). + exact: (@locally_fin_out_above_below _ e). +move: re1; rewrite le_eqVlt => /orP[re1|re1]. + have {re1}re1 : contract r%:E = 1 - e%:num. + by move: re1; rewrite eq_sym -subr_eq => /eqP <-. + have e1 : 1 < e%:num. + move: reN1. + rewrite re1 -addrA -opprD ltr_subl_addl ltr_subr_addl -!mulr2n -(mulr_natl e%:num) -{1}(mulr1 2) => ?. + by rewrite -(@ltr_pmul2l _ 2). + have Aoo : setT `\ +oo%E `<=` A. + move=> x [_]; rewrite /set1 /= => xpoo; apply reA. + case: x xpoo => [r' _ | // |_]. + have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E). + rewrite re1 opprB addrCA -[X in _ < X]addr0 ltr_add2 subr_lt0. + by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. + rewrite re1 addrAC ltr_subl_addl ltr_add // (lt_trans _ e1) // ltr_oppl. + by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. + rewrite [contract -oo]/= opprK gtr0_norm ?subr_gt0; last first. + rewrite -ltr_subl_addl add0r ltr_oppl. + by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. + by rewrite re1 addrAC ltr_subl_addl ltr_add. + have : locally r%:E (setT `\ +oo%E) by exists 1. + case => _/posnumP[x] /=; rewrite /ball_ => h. + by exists x%:num => // y /h; exact: Aoo. +by apply (@locally_fin_out_below _ e) => //; rewrite ltW. +Qed. + +Lemma ereal_locally_locall_ : locally = locally_ ereal_ball. +Proof. +rewrite predeq2E => x A; split. +- rewrite {1}/locally /= /ereal_locally. + case: x => [/= r [_/posnumP[e] reA]| [M [/= Mreal MA]]| [M [/= Mreal MA]]]. + + pose e' : R := minr (contract r%:E - contract (r%:E - e%:num%:E)) + (contract (r%:E + e%:num%:E) - contract r%:E). + exists e'. + rewrite /e' ltxI; apply/andP; split. + by rewrite subr_gt0 contract_preserves_order //= lte_fin ltr_subl_addr ltr_addl. + rewrite subr_gt0; apply contract_preserves_order. + by rewrite lte_fin ltr_addl. + case=> [r' re'r'| |]. + * rewrite /ereal_ball in re'r'. + have [r'r|rr'] := lerP (contract r'%:E) (contract r%:E). + apply reA. + rewrite /ball_ real_ltr_norml // ?num_real //. + rewrite ger0_norm ?subr_ge0// in re'r'. + have H1 : contract (r%:E - e%:num%:E) < contract r'%:E. + move: re'r'; rewrite /e' mc_1_10.Num.Theory.ltr_minr => /andP[Hr'1 Hr'2]. + rewrite /e' ltr_subr_addl addrC -ltr_subr_addl in Hr'1. + by rewrite (lt_le_trans Hr'1) // opprB addrCA subrr addr0. + move: (expand_preserves_order (contract_le1 _) (contract_le1 _) H1). + rewrite !contractK => rer'. + rewrite lte_fin ltr_subl_addr addrC -ltr_subl_addr in rer'. + rewrite rer' /= andbT (@lt_le_trans _ _ 0) //. + by rewrite ltr_oppl oppr0. + rewrite subr_ge0 -lee_fin -(contractK r%:E) -(contractK r'%:E). + move: r'r; rewrite le_eqVlt => /orP[/eqP -> //|r'r]. + exact/ltW/(expand_preserves_order (contract_le1 _) (contract_le1 _)). + apply reA. + rewrite /ball_ real_ltr_norml // ?num_real //. + rewrite ltr0_norm ?subr_lt0// opprB in re'r'. + apply/andP; split; last first. + rewrite (@lt_trans _ _ 0) // subr_lt0 -lte_fin. + rewrite -(contractK r%:E) -(contractK r'%:E). + by apply: (expand_preserves_order (contract_le1 _) (contract_le1 _)). + rewrite ltr_oppl opprB. + rewrite /e' in re'r'. + have H2 : contract r'%:E < contract (r%:E + e%:num%:E). + move: re'r'; rewrite mc_1_10.Num.Theory.ltr_minr => /andP[Hr'1 Hr'2]. + by rewrite ltr_subl_addr subrK in Hr'2. + rewrite ltr_subl_addr -lte_fin -(contractK (_ + r)%:E). + rewrite addrC -(contractK r'%:E) //. + exact: (expand_preserves_order (contract_le1 _) (contract_le1 _)). + * rewrite /ereal_ball [contract +oo]/=. + rewrite ltxI => /andP[re'1 re'2]. + have [cr0|cr0] := lerP 0 (contract r%:E). + move: re'2; rewrite ler0_norm; last first. + rewrite subr_le0. + by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. + rewrite opprB ltr_subr_addl addrCA subrr addr0 => h. + exfalso. + move: h; apply/negP. + rewrite -leNgt. + by move: (contract_le1 (r%:E + e%:num%:E)); rewrite ler_norml => /andP[]. + move: re'2; rewrite ler0_norm; last first. + rewrite subr_le0. + by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. + rewrite opprB ltr_subr_addl addrCA subrr addr0 => h. + exfalso. + move: h; apply/negP. + rewrite -leNgt. + by move: (contract_le1 (r%:E + e%:num%:E)); rewrite ler_norml => /andP[]. + * rewrite /ereal_ball [contract -oo]/=; rewrite opprK. + rewrite ltxI => /andP[re'1 _]. + move: re'1. + rewrite ger0_norm; last first. + rewrite addrC -ler_subl_addl add0r. + by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. + rewrite ltr_add2l => h. + exfalso. + move: h; apply/negP; rewrite -leNgt -ler_oppl. + by move: (contract_le1 (r%:E - e%:num%:E)); rewrite ler_norml => /andP[]. + + exists (1 - contract M%:E). + by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm. + case=> [r| |]. + * rewrite /ereal_ball [_ +oo%E]/= => rM1. + apply MA. + rewrite lte_fin. + rewrite ger0_norm in rM1; last first. + by rewrite subr_ge0 // (le_trans _ (contract_le1 r%:E)) // ler_norm. + rewrite ltr_subl_addr addrC addrCA addrC -ltr_subl_addr subrr subr_gt0 in rM1. + rewrite -lte_fin -(contractK M%:E) -(contractK r%:E). + exact: (expand_preserves_order (contract_le1 _) (contract_le1 _)). + * rewrite /ereal_ball /= subrr normr0 => h. + exact: MA. + * rewrite /ereal_ball /= opprK => h {MA}. + exfalso. + move: h; apply/negP. + rewrite -leNgt [in X in _ <= X]ger0_norm // ler_subl_addr. + rewrite -/(contract M%:E) addrC -ler_subl_addr opprD addrA subrr sub0r. + by move: (contract_le1 M%:E); rewrite ler_norml => /andP[]. + + exists (1 + contract M%:E). + rewrite -ltr_subl_addl sub0r. + by move: (contract_lt1 M); rewrite ltr_norml => /andP[]. + case=> [r| |]. + * rewrite /ereal_ball [_ -oo%E]/= => rM1. + apply MA. + rewrite lte_fin. + rewrite ler0_norm in rM1; last first. + rewrite ler_subl_addl addr0 ltW //. + by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. + rewrite opprB opprK -ltr_subl_addl addrK in rM1. + rewrite -lte_fin -(contractK M%:E) -(contractK r%:E). + exact: (expand_preserves_order (contract_le1 _) (contract_le1 _)). + * rewrite /ereal_ball /= -opprD normrN => h {MA}. + exfalso. + move: h; apply/negP. + rewrite -leNgt [in X in _ <= X]ger0_norm// -ler_subl_addr addrAC. + rewrite subrr add0r -/(contract M%:E) (le_trans _ (ltW (contract_lt1 M))) //. + by rewrite ler_norm. + * rewrite /ereal_ball /= => _; exact: MA. +- case: x => [r [_/posnumP[e] reA]| [_/posnumP[e] reA] | [_/posnumP[e] reA]] //=. + + rewrite /ereal_ball in reA. + by apply locally_fin_inbound with e. + + rewrite /ereal_ball [contract +oo]/= in reA. + have [|] := boolP (e%:num <= 1); first exact: locally_oo_up_e1. + by rewrite -ltNge; apply: locally_oo_up_1e. + + rewrite /ereal_ball [contract -oo]/= in reA. + have [|] := boolP (e%:num <= 1); first exact: locally_oo_down_e1. + by rewrite -ltNge; apply: locally_oo_down_1e. +Qed. +Definition ereal_pseudoMetricType_mixin := + PseudoMetric.Mixin ereal_ball_center ereal_ball_sym ereal_ball_triangle + ereal_locally_locall_. +Canonical ereal_pseudoMetricType := + PseudoMetricType {ereal R} ereal_pseudoMetricType_mixin. +End ereal_PseudoMetric. + (** ** Modules with a norm *) Module NormedModule. From 6e7ad00e5846cf0d21c4b3ba95405d872834ee20 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 29 May 2020 23:00:15 +0900 Subject: [PATCH 2/6] divergence in R is convergence to +oo in {ereal R} --- theories/normedtype.v | 113 +++++++++++++++++++----------------------- theories/sequences.v | 47 ++++++++++++++++++ 2 files changed, 97 insertions(+), 63 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 11e295da38..691351e762 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -946,39 +946,26 @@ Qed. Lemma bijective_contract : {on [pred x| `|x| <= 1], bijective contract}. Proof. exists expand; [by move=> x _; rewrite contractK | exact: expandK]. Qed. -Lemma contract_preserves_order : {homo contract : x y / (x < y)%O}. -Proof. -move=> -[r0 | | ] [r1 | _ | _ ] //=. -- rewrite lte_fin => r0r1; rewrite ltr_pdivr_mulr; last first. - by rewrite -(addr0 0) ltr_le_add. - rewrite mulrAC ltr_pdivl_mulr 2?mulrDr 2?mulr1; last first. - by rewrite -(addr0 0) ltr_le_add. - have [r10|r10] := lerP 0 r1. - rewrite ger0_norm //. - have [r00|r00] := lerP 0 r0. - move: r00 r0r1; rewrite le_eqVlt => /orP[/eqP <-|r00]. - by rewrite add0r mul0r normr0 mulr0 addr0. - by move=> r0r1; rewrite gtr0_norm // mulrC ltr_add2r. - move: r10 r0r1; rewrite le_eqVlt => /orP[/eqP <-|r10 r0r1]. - by rewrite mulr0 addr0 add0r mul0r. - rewrite ltr0_norm // ltr_add // (@lt_trans _ _ 0) //. - by rewrite nmulr_rlt0. - by rewrite pmulr_lgt0 // oppr_gt0. - rewrite ltr0_norm //. - have [r00|r00] := lerP 0 r0. - by move: (le_lt_trans r00 r0r1) => /(lt_trans r10); rewrite ltxx. - by rewrite ltr0_norm // mulrC mulrN -mulNr ltr_add2r. -- rewrite ltr_pdivr_mulr; last by rewrite -(addr0 0) ltr_le_add. - by rewrite mul1r -{1}(add0r r0) ltr_le_add // ler_norm. -- rewrite ltr_pdivl_mulr ?mulN1r; last by rewrite -(addr0 0) ltr_le_add. - by rewrite ltr_oppl -(add0r (- r1)) ltr_le_add // -(normrN r1) ler_norm. -- by rewrite -subr_gt0 opprK (_ : 1 = 1%:R). -Qed. - -Lemma contract_preserves_le_order : {homo contract : x y / (x <= y)%O}. -Proof. exact/ltW_homo/contract_preserves_order. Qed. - -Lemma expand_preserves_order : +Lemma homo_contract_lt : {homo contract : x y / (x < y)%O}. +Proof. +move=> -[r0 | | ] [r1 | _ | _] //=. +- rewrite lte_fin => r0r1; rewrite ltr_pdivr_mulr ?ltr_paddr//. + rewrite mulrAC ltr_pdivl_mulr ?ltr_paddr// 2?mulrDr 2?mulr1. + have [r10|?] := ler0P r1; last first. + rewrite ltr_le_add // mulrC; have [r00|//] := ler0P r0. + by rewrite (@le_trans _ _ 0) // ?pmulr_lle0 // mulr_ge0 // ?oppr_ge0 // ltW. + have [?|r00] := ler0P r0; first by rewrite ltr_le_add // 2!mulrN mulrC. + by move: (le_lt_trans r10 (lt_trans r00 r0r1)); rewrite ltxx. +- by rewrite ltr_pdivr_mulr ?ltr_paddr// mul1r ltr_spaddl // ler_norm. +- rewrite ltr_pdivl_mulr ?mulN1r ?ltr_paddr// => _. + by rewrite ltr_oppl ltr_spaddl // ler_normr lexx orbT. +- by rewrite -subr_gt0 opprK. +Qed. + +Lemma homo_contract_le : {homo contract : x y / (x <= y)%O}. +Proof. exact/ltW_homo/homo_contract_lt. Qed. + +Lemma homo_expand_lt : {in [pred x| `|x| <= 1] & [pred x| `|x| <= 1], {homo expand : x y / (x < y)%O}}. Proof. move=> x y; rewrite !inE => x1 y1 xy; rewrite /expand. @@ -1067,7 +1054,7 @@ case => [r | | //]. by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. rewrite ltr_subl_addl addrC -ltr_subl_addl -[X in X < _]expandK; last first. by rewrite inE ger0_norm ?ler_subl_addl ?ler_addr // subr_ge0. - exact: contract_preserves_order. + exact: homo_contract_lt. - by move=> _; apply reA; rewrite /= subrr normr0. Qed. @@ -1145,7 +1132,7 @@ have X : `|contract r%:E - (e)%:num| < 1. pose e' := r - real_of_er (expand (contract r%:E - e%:num)). have e'0 : 0 < e'. rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E) real_of_er_expand //. - apply: (expand_preserves_order _ (contract_le1 _)); first by rewrite inE ltW. + apply: (homo_expand_lt _ (contract_le1 _)); first by rewrite inE ltW. by rewrite ltr_subl_addl ltr_addr. apply/locallyP; exists e' => // r' re'r'; apply reA. rewrite /ball /= in re'r'. @@ -1153,15 +1140,15 @@ have [rr'|r'r] := lerP r r'. move: rr'; rewrite le_eqVlt => /orP[/eqP->|rr']; first by rewrite subrr normr0. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. rewrite ltr0_norm; last first. - by rewrite subr_lt0; apply: contract_preserves_order; rewrite lte_fin. + by rewrite subr_lt0; apply: homo_contract_lt; rewrite lte_fin. rewrite opprB ltr_subl_addl (lt_le_trans _ re1) //. by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. rewrite gtr0_norm ?subr_gt0 //; last first. - by apply: contract_preserves_order; rewrite lte_fin. + by apply: homo_contract_lt; rewrite lte_fin. move: re'r'. rewrite gtr0_norm // ?subr_gt0// /e'. rewrite -ltr_subl_addl addrAC subrr add0r ltr_oppl opprK -lte_fin real_of_er_expand //. -rewrite -[in X in X -> _](contractK r'%:E) => /contract_preserves_order r'e'r. +rewrite -[in X in X -> _](contractK r'%:E) => /homo_contract_lt r'e'r. rewrite expandK in r'e'r; last by rewrite inE ltW. rewrite expandK in r'e'r; last by rewrite inE contract_le1. by rewrite ltr_subl_addl addrC -ltr_subl_addl. @@ -1181,7 +1168,7 @@ pose e' : R := real_of_er (expand (contract r%:E + e%:num)) - r. have e'0 : 0 < e'. rewrite /e'. rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E) real_of_er_expand //. - apply: (expand_preserves_order (contract_le1 _)); last by rewrite ltr_addl. + apply: (homo_expand_lt (contract_le1 _)); last by rewrite ltr_addl. by rewrite inE ltW. apply/locallyP; exists e' => // r' r'e'r; apply reA. rewrite /ball /= in r'e'r. @@ -1190,13 +1177,13 @@ have [rr'|r'r] := lerP r r'. by rewrite subrr normr0. rewrite ltr0_norm ?subr_lt0// opprB in r'e'r. rewrite ltr0_norm; last first. - by rewrite subr_lt0; apply: contract_preserves_order; rewrite lte_fin. + by rewrite subr_lt0; apply: homo_contract_lt; rewrite lte_fin. rewrite opprB; move: r'e'r. rewrite /e' -ltr_subl_addr opprK subrK -lte_fin real_of_er_expand //. move=> r'e'r; rewrite ltr_subl_addl. - by move/contract_preserves_order : r'e'r; rewrite expandK // inE ltW. + by move/homo_contract_lt : r'e'r; rewrite expandK // inE ltW. rewrite gtr0_norm; last first. - by rewrite subr_gt0; apply contract_preserves_order; rewrite lte_fin. + by rewrite subr_gt0; apply homo_contract_lt; rewrite lte_fin. rewrite ltr_subl_addl addrC -ltr_subl_addl (le_lt_trans reN1) //. by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. Qed. @@ -1214,11 +1201,11 @@ case: x => [r'| |] //. rewrite le_eqVlt => /orP[/eqP <-|rr']. by rewrite subrr normr0. rewrite ltr0_norm; last first. - by rewrite subr_lt0; apply: contract_preserves_order; rewrite lte_fin. + by rewrite subr_lt0; apply: homo_contract_lt; rewrite lte_fin. rewrite opprB ltr_subl_addl (le_lt_trans _ re1) //. by move: (contract_le1 r'%:E); rewrite ler_norml => /andP[]. rewrite gtr0_norm; last first. - by rewrite subr_gt0; apply contract_preserves_order; rewrite lte_fin. + by rewrite subr_gt0; apply homo_contract_lt; rewrite lte_fin. rewrite ltr_subl_addl addrC -ltr_subl_addl (lt_le_trans reN1) //. by move: (contract_le1 r'%:E); rewrite ler_norml => /andP[]. - rewrite [contract +oo]/= ler0_norm; last first. @@ -1276,10 +1263,10 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1]. have e'0 : 0 < e'. rewrite /e' ltxI; apply/andP; split. rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E) real_of_er_expand //. - apply: (expand_preserves_order _ (contract_le1 _)); first by rewrite inE ltW. + apply: (homo_expand_lt _ (contract_le1 _)); first by rewrite inE ltW. by rewrite ltr_subl_addl ltr_addr. rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E) real_of_er_expand //. - apply: (expand_preserves_order (contract_le1 _)); last by rewrite ltr_addl. + apply: (homo_expand_lt (contract_le1 _)); last by rewrite ltr_addl. by rewrite inE ltW. apply/locallyP; exists e' => // r' re'r'; apply reA. rewrite /ball /= in re'r'. @@ -1288,19 +1275,19 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1]. by rewrite subrr normr0. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. rewrite ltr0_norm; last first. - by rewrite subr_lt0; apply: contract_preserves_order; rewrite lte_fin. + by rewrite subr_lt0; apply: homo_contract_lt; rewrite lte_fin. rewrite opprB; move: re'r'. rewrite /e' ltxI => /andP[_]. rewrite -ltr_subl_addr opprK subrK -lte_fin real_of_er_expand //. move=> r'e'r; rewrite ltr_subl_addl. - by move/contract_preserves_order : r'e'r; rewrite expandK // inE ltW. + by move/homo_contract_lt : r'e'r; rewrite expandK // inE ltW. move: re'r'; rewrite ltxI => /andP[]. rewrite gtr0_norm ?subr_gt0 // -ltr_subl_addl addrAC subrr add0r ltr_oppl. rewrite opprK -lte_fin real_of_er_expand // => r'e'r _. rewrite gtr0_norm; last first. - by rewrite subr_gt0; apply contract_preserves_order; rewrite lte_fin. + by rewrite subr_gt0; apply homo_contract_lt; rewrite lte_fin. rewrite ltr_subl_addl addrC -ltr_subl_addl. - by move/contract_preserves_order : r'e'r; rewrite expandK // inE ltW. + by move/homo_contract_lt : r'e'r; rewrite expandK // inE ltW. by apply (@locally_fin_out_above _ e) => //; rewrite ltW. have [re1|re1] := ltrP 1 (contract r%:E + (e)%:num). exact: (@locally_fin_out_above_below _ e). @@ -1329,7 +1316,7 @@ move: re1; rewrite le_eqVlt => /orP[re1|re1]. by apply (@locally_fin_out_below _ e) => //; rewrite ltW. Qed. -Lemma ereal_locally_locall_ : locally = locally_ ereal_ball. +Lemma ereal_locallyE : locally = locally_ ereal_ball. Proof. rewrite predeq2E => x A; split. - rewrite {1}/locally /= /ereal_locally. @@ -1338,8 +1325,8 @@ rewrite predeq2E => x A; split. (contract (r%:E + e%:num%:E) - contract r%:E). exists e'. rewrite /e' ltxI; apply/andP; split. - by rewrite subr_gt0 contract_preserves_order //= lte_fin ltr_subl_addr ltr_addl. - rewrite subr_gt0; apply contract_preserves_order. + by rewrite subr_gt0 homo_contract_lt //= lte_fin ltr_subl_addr ltr_addl. + rewrite subr_gt0; apply homo_contract_lt. by rewrite lte_fin ltr_addl. case=> [r' re'r'| |]. * rewrite /ereal_ball in re'r'. @@ -1351,29 +1338,29 @@ rewrite predeq2E => x A; split. move: re'r'; rewrite /e' mc_1_10.Num.Theory.ltr_minr => /andP[Hr'1 Hr'2]. rewrite /e' ltr_subr_addl addrC -ltr_subr_addl in Hr'1. by rewrite (lt_le_trans Hr'1) // opprB addrCA subrr addr0. - move: (expand_preserves_order (contract_le1 _) (contract_le1 _) H1). + move: (homo_expand_lt (contract_le1 _) (contract_le1 _) H1). rewrite !contractK => rer'. rewrite lte_fin ltr_subl_addr addrC -ltr_subl_addr in rer'. rewrite rer' /= andbT (@lt_le_trans _ _ 0) //. by rewrite ltr_oppl oppr0. rewrite subr_ge0 -lee_fin -(contractK r%:E) -(contractK r'%:E). move: r'r; rewrite le_eqVlt => /orP[/eqP -> //|r'r]. - exact/ltW/(expand_preserves_order (contract_le1 _) (contract_le1 _)). + exact/ltW/(homo_expand_lt (contract_le1 _) (contract_le1 _)). apply reA. rewrite /ball_ real_ltr_norml // ?num_real //. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. apply/andP; split; last first. rewrite (@lt_trans _ _ 0) // subr_lt0 -lte_fin. rewrite -(contractK r%:E) -(contractK r'%:E). - by apply: (expand_preserves_order (contract_le1 _) (contract_le1 _)). + by apply: (homo_expand_lt (contract_le1 _) (contract_le1 _)). rewrite ltr_oppl opprB. rewrite /e' in re'r'. have H2 : contract r'%:E < contract (r%:E + e%:num%:E). - move: re'r'; rewrite mc_1_10.Num.Theory.ltr_minr => /andP[Hr'1 Hr'2]. + move: re'r'; rewrite ltxI => /andP[Hr'1 Hr'2]. by rewrite ltr_subl_addr subrK in Hr'2. rewrite ltr_subl_addr -lte_fin -(contractK (_ + r)%:E). rewrite addrC -(contractK r'%:E) //. - exact: (expand_preserves_order (contract_le1 _) (contract_le1 _)). + exact: (homo_expand_lt (contract_le1 _) (contract_le1 _)). * rewrite /ereal_ball [contract +oo]/=. rewrite ltxI => /andP[re'1 re'2]. have [cr0|cr0] := lerP 0 (contract r%:E). @@ -1413,7 +1400,7 @@ rewrite predeq2E => x A; split. by rewrite subr_ge0 // (le_trans _ (contract_le1 r%:E)) // ler_norm. rewrite ltr_subl_addr addrC addrCA addrC -ltr_subl_addr subrr subr_gt0 in rM1. rewrite -lte_fin -(contractK M%:E) -(contractK r%:E). - exact: (expand_preserves_order (contract_le1 _) (contract_le1 _)). + exact: (homo_expand_lt (contract_le1 _) (contract_le1 _)). * rewrite /ereal_ball /= subrr normr0 => h. exact: MA. * rewrite /ereal_ball /= opprK => h {MA}. @@ -1434,7 +1421,7 @@ rewrite predeq2E => x A; split. by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. rewrite opprB opprK -ltr_subl_addl addrK in rM1. rewrite -lte_fin -(contractK M%:E) -(contractK r%:E). - exact: (expand_preserves_order (contract_le1 _) (contract_le1 _)). + exact: (homo_expand_lt (contract_le1 _) (contract_le1 _)). * rewrite /ereal_ball /= -opprD normrN => h {MA}. exfalso. move: h; apply/negP. @@ -1454,7 +1441,7 @@ rewrite predeq2E => x A; split. Qed. Definition ereal_pseudoMetricType_mixin := PseudoMetric.Mixin ereal_ball_center ereal_ball_sym ereal_ball_triangle - ereal_locally_locall_. + ereal_locallyE. Canonical ereal_pseudoMetricType := PseudoMetricType {ereal R} ereal_pseudoMetricType_mixin. End ereal_PseudoMetric. @@ -3073,7 +3060,7 @@ have D_has_sup : has_sup D; first split. apply/downP; exists x. by near: x. by rewrite ler_distW 1?distrC 1?ltW ?andbT //; near: x. -- exists (x0 + 1); apply/ubP => x /(_ _ x01) /downP [y []]. +- exists (x0 + 1); apply/ubP => x /(_ _ x01) /downP [y]. rewrite -[ball _ _ _]/(_ (_ < _)) ltr_distl ltr_subl_addr => /andP[/ltW]. by move=> /(le_trans _) yx01 _ /yx01. exists (sup D). @@ -3082,7 +3069,7 @@ rewrite ler_distl; move/ubP: (sup_upper_bound D_has_sup) => -> //=. apply: sup_le_ub => //; first by case: D_has_sup. have Fxeps : F (ball_ [eta normr] x (eps)%:num). by near: x; apply: nearP_dep; apply: F_cauchy. - apply/ubP => y /(_ _ Fxeps) /downP[z []]. + apply/ubP => y /(_ _ Fxeps) /downP[z]. rewrite /ball_ ltr_distl ltr_subl_addr. by move=> /andP [/ltW /(le_trans _) le_xeps _ /le_xeps]. rewrite /D /= => A FA; near F => y. diff --git a/theories/sequences.v b/theories/sequences.v index f767b7e5d0..1205d382ef 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -687,3 +687,50 @@ apply/cauchy_cvgP/cauchy_seriesP => e /u_ncvg. apply: filterS => n /=; rewrite ger0_norm ?sumr_ge0//. by apply: le_lt_trans; apply: ler_norm_sum. Qed. + +Section sequences_of_extended_real_numbers. + +(* TODO: worth keeping in addition to cvgPpinfty? *) +Lemma cvgPpinfty_lt (R : realFieldType) (u_ : R^o ^nat) : + u_ --> +oo <-> forall A, A > 0 -> \forall n \near \oo, A < u_ n. +Proof. +split => [/cvgPpinfty uoo A A0|uoo]; last first. + by apply/cvgPpinfty => A {}/uoo [n _ uoo]; exists n => // m nm; apply/ltW/uoo. +have /uoo[n _ {}uoo] : 0 < A *+ 2 by rewrite pmulrn_lgt0. +exists n => // m nm; rewrite (@lt_le_trans _ _ (A *+ 2)) // ?mulr2n ?ltr_addr //. +exact: uoo. +Qed. + +Lemma dvg_ereal_cvg (R : realType) (u_ : (R^o) ^nat) : + u_ --> +oo -> (fun n => (u_ n)%:E) --> +oo%E. +Proof. +move/cvgPpinfty_lt => uoo; apply/cvg_ballP => _/posnumP[e]; rewrite near_map. +have [e1|e1] := lerP 1 e%:num. + case: (uoo _ ltr01) => k _ k1un; near=> n. + rewrite /ball /= /ereal_ball [contract +oo]/= ger0_norm ?subr_ge0; last first. + by move: (contract_le1 (u_ n)%:E); rewrite ler_norml => /andP[]. + rewrite ltr_subl_addr addrC -ltr_subl_addr. + suff : contract 1%:E < contract (u_ n)%:E. + apply/le_lt_trans. + by rewrite (@le_trans _ _ 0) // ?subr_le0 //= normr1 divr_ge0. + apply homo_contract_lt; rewrite lte_fin; apply k1un. + by near: n; exists k. +have onee1 : `|1 - e%:num| < 1. + by rewrite gtr0_norm // ?subr_gt0 // ltr_subl_addl addrC -ltr_subl_addl subrr. +have : 0 < real_of_er (expand (1 - e%:num)). + rewrite -lte_fin real_of_er_expand // -expand0. + apply homo_expand_lt; by + [rewrite inE normr0| rewrite inE ltW| rewrite subr_gt0]. +case/uoo => k _ k1un; near=> n. +rewrite /ball /= /ereal_ball [contract +oo]/= ger0_norm ?subr_ge0; last first. + by move: (contract_le1 (u_ n)%:E); rewrite ler_norml => /andP[]. +rewrite ltr_subl_addr addrC -ltr_subl_addr. +suff : `|1 - e%:num| < contract (u_ n)%:E by exact: le_lt_trans (ler_norm _). +rewrite gtr0_norm ?subr_gt0 // -(@expandK R (1 - e%:num)); last first. + by rewrite inE gtr0_norm ?subr_gt0// ler_subl_addr addrC -ler_subl_addr subrr. +rewrite -lte_fin; apply/homo_contract_lt. +rewrite -real_of_er_expand // lte_fin; apply k1un. +by near: n; exists k. +Grab Existential Variables. all: end_near. Qed. + +End sequences_of_extended_real_numbers. From 021e7a183191ce8a6fe199ed631101fc4297208b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 1 Jun 2020 23:53:56 +0900 Subject: [PATCH 3/6] a non-decreasing sequence of ereals converges to its sup --- theories/ereal.v | 18 ++++ theories/normedtype.v | 204 +++++++++++++++++++++++------------------- theories/sequences.v | 108 +++++++++++++++++++++- 3 files changed, 237 insertions(+), 93 deletions(-) diff --git a/theories/ereal.v b/theories/ereal.v index f947860ec1..d6df07a641 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -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. @@ -463,6 +465,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 *) @@ -529,6 +544,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 => /= [|_ _]. diff --git a/theories/normedtype.v b/theories/normedtype.v index 691351e762..4ec13060dc 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -845,12 +845,9 @@ Definition contract (x : {ereal R}) : R := Lemma contract_lt1 x : `|contract x%:E| < 1. Proof. -rewrite /= normrM normrV ?unitfE //; last first. - rewrite eq_sym lt_eqF // -ltr_subl_addr sub0r (@le_lt_trans _ _ 0) //. - by rewrite -ler_oppl oppr0. -rewrite ltr_pdivr_mulr // ?mul1r; last first. - by rewrite gtr0_norm (@lt_le_trans _ _ 1) // ler_addl. -by rewrite [X in _ < X]gtr0_norm ?ltr_addr// (@lt_le_trans _ _ 1)// ler_addl. +rewrite normrM normrV ?unitfE //; last by rewrite eq_sym lt_eqF // ltr_spaddl. +rewrite ltr_pdivr_mulr // ?mul1r; last by rewrite gtr0_norm ltr_spaddl. +by rewrite [X in _ < X]gtr0_norm ?ltr_addr// ltr_spaddl. Qed. Lemma contract_le1 x : `|contract x| <= 1. @@ -858,33 +855,55 @@ Proof. by case: x => [x| |] /=; rewrite ?normrN1 ?normr1 // (ltW (contract_lt1 _)). Qed. -Lemma contractN x : contract (- x) = - contract x. -Proof. by case: x => //= [r|]; [ rewrite normrN mulNr | rewrite opprK]. Qed. - Lemma contract0 : contract 0%:E = 0. Proof. by rewrite /contract mul0r. Qed. -Lemma contract_eq0 r : (contract r == 0) = (r == 0%:E). +Lemma contractN x : contract (- x) = - contract x. +Proof. by case: x => //= [r|]; [ rewrite normrN mulNr | rewrite opprK]. Qed. + +Lemma contract_eq0 x : (contract x == 0) = (x == 0%:E). Proof. -case: r => [r| |] /=. +case: x => [r| |] /=. - apply/idP/idP => [|/eqP[->]]; last by rewrite mul0r. rewrite mulf_eq0 => /orP[/eqP -> //|]. - rewrite invr_eq0 eq_sym -subr_eq add0r -eqr_opp opprK => r1. - by move: (normr_ge0 r); rewrite (eqP r1) /= oppr_ge0 leNgt /= ltr01. + by rewrite invr_eq0 paddr_eq0 // oner_eq0. - exact/idP/idP. - by rewrite -eqr_opp opprK oppr0 oner_eq0. Qed. +Lemma contract_eqN1 x : (contract x == -1) = (x == -oo%E). +Proof. +apply/eqP/eqP => [|->//]; move: x => -[r /= /eqP | /= | //]; last first. + by move/eqP; rewrite -subr_eq0 opprK (_ : _ + _ = 2%:R) // pnatr_eq0. +rewrite -eqr_oppLR -mulNr => /eqP/divr1_eq/eqP; rewrite eqr_oppLR => r1. +have r0 : r < 0 by rewrite (eqP r1) oppr_lt0 ltr_spaddl. +by move: r1; rewrite ltr0_norm // -subr_eq0 opprK addrCA subrr addr0 oner_eq0. +Qed. + +Lemma contract_eq1 x : (contract x == 1) = (x == +oo%E). +Proof. by rewrite -(oppeK x) contractN eqr_oppLR contract_eqN1; case: x. Qed. + Definition expand r : {ereal R} := if r == 1 then +oo%E else if r == -1 then -oo%E else (r / (1 - `|r|))%:E. +Lemma expand1 : expand 1 = +oo%E. Proof. by rewrite /expand eqxx. Qed. + +Lemma expandN1 : expand (-1) = -oo%E. +Proof. by rewrite /expand -subr_eq0 -opprD oppr_eq0 gt_eqF // eqxx. Qed. + Lemma expand0 : expand 0 = 0%:E. Proof. by rewrite /expand eq_sym oner_eq0 -eqr_oppLR oppr0 eq_sym oner_eq0 mul0r. Qed. +Lemma expand_eqoo (r : R) : (expand r == +oo%E) = (r == 1). +Proof. +apply/eqP/eqP => [|->]; last by rewrite expand1. +by rewrite /expand; case: ifPn => [/eqP//|?]; case: ifPn. +Qed. + Lemma contractK : cancel contract expand. Proof. case=> [r| |]; rewrite /expand /= ?eqxx //. @@ -907,40 +926,36 @@ case=> [r| |]; rewrite /expand /= ?eqxx //. by rewrite (_ : _ == 0 = false) //; apply/negP/negP. Qed. -Lemma lt1_neq1 (x : R) : `|x| < 1 -> x == 1 = false. +Lemma nlt_eqF (x y : R) : `|x| < y -> x == y = false. Proof. by move=> x1; rewrite lt_eqF // (le_lt_trans (ler_norm _) x1). Qed. -Lemma lt1_neqN1 (x : R) : `|x| < 1 -> x == -1 = false. +Lemma ngt_eqF (x y : R) : `|x| < y -> x == -y = false. Proof. by rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF. Qed. Lemma expandK : {in [pred x | `|x| <= 1], cancel expand contract}. Proof. -move=> x; rewrite inE => x1; rewrite /expand /contract. -move: x1; rewrite le_eqVlt => /orP[|x1]. - have [x0|x0] := lerP 0 x. - by rewrite ger0_norm // => x1; rewrite x1; apply/esym/eqP. - rewrite ltr0_norm // eqr_oppLR => /eqP ->. - by rewrite eqxx eq_sym -subr_eq0 opprK (_ : 1 = 1%:R) // -natrD pnatr_eq0. -rewrite lt1_neq1 // lt1_neqN1 //. +move=> x; rewrite inE le_eqVlt => /orP[|x1]. + by rewrite eqr_norml => /andP[/orP[]/eqP->{x}]; rewrite ?(expand1,expandN1). +rewrite /expand nlt_eqF // ngt_eqF //. 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 lt1_neq1. - by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym lt1_neq1. + by rewrite unitfE subr_eq0 eq_sym nlt_eqF. + by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym nlt_eqF. have x_nneq0 : 1 - x / (1 + x) != 0. rewrite -[X in X + _](@divrr _ (1 + x)) -?mulrBl; last first. - by rewrite unitfE addrC addr_eq0 lt1_neqN1. - by rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym lt1_neqN1. + by rewrite unitfE addrC addr_eq0 ngt_eqF. + by rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym ngt_eqF. 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 eqr_opp => /eqP. -rewrite !ger0_norm //; last first. + by move=> /eqP; rewrite NERFin contractN 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. rewrite -(mulrA (x / _)) mulVr ?unitfE // mulr1. rewrite -[X in X + _ / _](@divrr _ (1 - x)) -?mulrDl ?subrK ?div1r //. -by rewrite unitfE subr_eq0 eq_sym lt1_neq1. +by rewrite unitfE subr_eq0 eq_sym nlt_eqF. Qed. Lemma bijective_contract : {on [pred x| `|x| <= 1], bijective contract}. @@ -965,33 +980,27 @@ Qed. Lemma homo_contract_le : {homo contract : x y / (x <= y)%O}. Proof. exact/ltW_homo/homo_contract_lt. Qed. -Lemma homo_expand_lt : - {in [pred x| `|x| <= 1] & [pred x| `|x| <= 1], {homo expand : x y / (x < y)%O}}. +Lemma homo_expand_lt : {in [pred x| `|x| <= 1] & [pred x| `|x| <= 1], + {homo expand : x y / (x < y)%O}}. Proof. -move=> x y; rewrite !inE => x1 y1 xy; rewrite /expand. +move=> x y; rewrite !inE => x1 y1 xy. move: x1; rewrite le_eqVlt => /orP[|x1]. have [x0|x0] := lerP 0 x. - rewrite ger0_norm // => x1; exfalso. - move: xy; rewrite (eqP x1) ltNge => /negP; apply. - by rewrite (le_trans _ y1) // ler_norm. - rewrite ltr0_norm // eqr_oppLR => x1. - rewrite (eqP x1) eqxx eq_sym -subr_eq0 opprK (_ : 1 = 1%:R) // -natrD. - rewrite pnatr_eq0 //=; case: ifPn => // y_neq1. - rewrite -mulNrn -mulr_natr mulr1 ifF; last first. - apply: contraNF y_neq1 => y_eq1. - by move: xy; rewrite (eqP x1) (eqP y_eq1) ltxx. - by rewrite lte_ninfty. + rewrite ger0_norm // => /eqP x1; exfalso. + move: y1; rewrite ler_norml => /andP[_]/(lt_le_trans xy). + by rewrite x1 ltxx. + rewrite ltr0_norm // eqr_oppLR => /eqP x1. + rewrite x1 expandN1 /expand; case: ifPn => // y_neq1. + case: ifPn => [/eqP y_neqN1|?]; last by rewrite lte_ninfty. + by move: xy; rewrite x1 y_neqN1 ltxx. move: y1; rewrite le_eqVlt => /orP[|y1]. have [y0|y0] := lerP 0 y. - rewrite ger0_norm // => y1; rewrite y1. - by rewrite lt1_neq1 // lt1_neqN1 // lte_pinfty. - rewrite ltr0_norm // eqr_oppLR => y1; exfalso. - move: xy; rewrite (eqP y1) {y1 y0} ltNge => /negP; apply. - have [x0|x0] := lerP 0 x. - by rewrite (le_trans _ x0) // ler_oppl oppr0. - rewrite ltr0_norm // ltr_oppl in x1. - exact: ltW. -rewrite !lt1_neq1 // !lt1_neqN1 //. + rewrite ger0_norm // => /eqP y1; rewrite y1 expand1. + by rewrite /expand nlt_eqF // ngt_eqF // lte_pinfty. + rewrite ltr0_norm // eqr_oppLR => /eqP y1; exfalso. + move: x1; rewrite ltr_norml => /andP[x1 _]. + by move: xy; rewrite y1 => /(lt_trans x1); rewrite ltxx. +rewrite /expand (nlt_eqF x1) (nlt_eqF y1) (ngt_eqF x1) (ngt_eqF y1). have [x0|x0] := lerP 0 x. move: (x0); rewrite le_eqVlt => /orP[/eqP <-|{x0}x0]. by rewrite mul0r lte_fin divr_gt0 // ?subr_gt0 // (le_lt_trans x0). @@ -1009,15 +1018,20 @@ have [|y0] := lerP 0 y. rewrite le_eqVlt => /orP[/eqP <-|y0]. by rewrite normr0 mul0r subr0 mulr1. rewrite gtr0_norm // (@le_lt_trans _ _ 0) //. - rewrite mulrC nmulr_lle0 // subr_ge0 ltW //. - by rewrite (le_lt_trans _ y1) // ler_norm. + by rewrite nmulr_rle0 // subr_ge0 (le_trans _ (ltW y1)) // ler_norm. rewrite mulr_gt0 // -ltr_subl_addl sub0r ltr_oppl. by rewrite (le_lt_trans _ x1) // ler0_norm // ltW. by rewrite ltr0_norm // opprK !mulrDr !mulr1 mulrC ltr_add2r. Qed. +Lemma homo_expand_le : {in [pred x| `|x| <= 1] & + [pred x| `|x| <= 1], {homo expand : x y / (x <= y)%O}}. +Proof. +by apply/homoW_in => //= x y x1 y1; rewrite -2!lt_neqAle; apply/homo_expand_lt. +Qed. + Lemma real_of_er_expand x : `|x| < 1 -> (real_of_er (expand x))%:E = expand x. -Proof. by move=> x1; rewrite /expand lt1_neq1 // lt1_neqN1. Qed. +Proof. by move=> x1; rewrite /expand nlt_eqF // ngt_eqF. Qed. End contract_expand. @@ -1051,7 +1065,7 @@ case => [r | | //]. - rewrite real_of_er_expand; last first. by rewrite ger0_norm ?ltr_subl_addl ?ltr_addr // subr_ge0. move=> h; apply reA; rewrite gtr0_norm ?subr_gt0; last first. - by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. + by case/ltr_normlP : (contract_lt1 r). rewrite ltr_subl_addl addrC -ltr_subl_addl -[X in X < _]expandK; last first. by rewrite inE ger0_norm ?ler_subl_addl ?ler_addr // subr_ge0. exact: homo_contract_lt. @@ -1084,8 +1098,10 @@ have [e2{e1}|e2] := ltrP 2 e%:num. suff -> : A = setT by exists 0; rewrite real0. rewrite predeqE => x; split => // _; apply reA. rewrite (le_lt_trans _ e2) // (le_trans (ler_norm_sub _ _)) // normr1. - by rewrite addrC -ler_subr_addr (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1) // addrK. -have /andP[e10 e11] : 0 < e%:num - 1 <= 1 by rewrite subr_gt0 e1 /= ler_subl_addl. + rewrite addrC -ler_subr_addr (le_trans (contract_le1 _)) //. + by rewrite (_ : 2 = 1 + 1) // addrK. +have /andP[e10 e11] : 0 < e%:num - 1 <= 1. + by rewrite subr_gt0 e1 /= ler_subl_addl. apply locallyNKe. have : (PosNum e10)%:num <= 1 by []. move/(@locally_oo_down_e1 (-%E @` A) (PosNum e10)); apply. @@ -1106,9 +1122,11 @@ move=> reA e1. have [e2{e1}|e2] := ltrP 2 e%:num. suff -> : A = setT by exists 0; rewrite real0. rewrite predeqE => x; split => // _; apply reA. - rewrite (le_lt_trans _ e2) // -opprB normrN opprK (le_trans (ler_norm_add _ _)) // normr1. - by rewrite -ler_subr_addr (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1) // addrK. -have /andP[e10 e11] : 0 < e%:num - 1 <= 1 by rewrite subr_gt0 e1 /= ler_subl_addl. + rewrite (le_lt_trans _ e2) // -opprB normrN opprK. + rewrite (le_trans (ler_norm_add _ _)) // normr1 -ler_subr_addr. + by rewrite (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1) // addrK. +have /andP[e10 e11] : 0 < e%:num - 1 <= 1. + by rewrite subr_gt0 e1 /= ler_subl_addl. apply locallyNKe. have : (PosNum e10)%:num <= 1 by []. move/(@locally_oo_up_e1 (-%E @` A) (PosNum e10)); apply. @@ -1127,11 +1145,12 @@ Lemma locally_fin_out_above (r : R) (e : {posnum R}) (A : set {ereal R}) : Proof. move=> reA reN1 re1. have X : `|contract r%:E - (e)%:num| < 1. - rewrite ltr_norml reN1 andTb ltr_subl_addl (@le_lt_trans _ _ 1) // ?ltr_addr //. + rewrite ltr_norml reN1 andTb ltr_subl_addl ltr_spaddl //. by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. pose e' := r - real_of_er (expand (contract r%:E - e%:num)). have e'0 : 0 < e'. - rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E) real_of_er_expand //. + rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E). + rewrite real_of_er_expand //. apply: (homo_expand_lt _ (contract_le1 _)); first by rewrite inE ltW. by rewrite ltr_subl_addl ltr_addr. apply/locallyP; exists e' => // r' re'r'; apply reA. @@ -1142,12 +1161,12 @@ have [rr'|r'r] := lerP r r'. rewrite ltr0_norm; last first. by rewrite subr_lt0; apply: homo_contract_lt; rewrite lte_fin. rewrite opprB ltr_subl_addl (lt_le_trans _ re1) //. - by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. -rewrite gtr0_norm ?subr_gt0 //; last first. - by apply: homo_contract_lt; rewrite lte_fin. + by case/ltr_normlP : (contract_lt1 r'). +rewrite gtr0_norm ?subr_gt0//; last by apply: homo_contract_lt; rewrite lte_fin. move: re'r'. rewrite gtr0_norm // ?subr_gt0// /e'. -rewrite -ltr_subl_addl addrAC subrr add0r ltr_oppl opprK -lte_fin real_of_er_expand //. +rewrite -ltr_subl_addl addrAC subrr add0r ltr_oppl opprK -lte_fin. +rewrite real_of_er_expand //. rewrite -[in X in X -> _](contractK r'%:E) => /homo_contract_lt r'e'r. rewrite expandK in r'e'r; last by rewrite inE ltW. rewrite expandK in r'e'r; last by rewrite inE contract_le1. @@ -1167,7 +1186,8 @@ have ? : `|contract r%:E + (e)%:num| < 1. pose e' : R := real_of_er (expand (contract r%:E + e%:num)) - r. have e'0 : 0 < e'. rewrite /e'. - rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E) real_of_er_expand //. + rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E). + rewrite real_of_er_expand //. apply: (homo_expand_lt (contract_le1 _)); last by rewrite ltr_addl. by rewrite inE ltW. apply/locallyP; exists e' => // r' r'e'r; apply reA. @@ -1209,7 +1229,7 @@ case: x => [r'| |] //. rewrite ltr_subl_addl addrC -ltr_subl_addl (lt_le_trans reN1) //. by move: (contract_le1 r'%:E); rewrite ler_norml => /andP[]. - rewrite [contract +oo]/= ler0_norm; last first. - by rewrite subr_le0; move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. + by rewrite subr_le0; case/ler_normlP: (contract_le1 r%:E). by rewrite opprB ltr_subl_addl. - rewrite [contract -oo]/= ger0_norm; last first. by rewrite subr_ge0; move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. @@ -1238,12 +1258,13 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1). move=> x [_]; rewrite /set1 /= => xnoo; apply reA. case: x xnoo => [r' _ | |//]. have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E). - rewrite reN1 opprB addrA ltr_subl_addl ler_lt_add // (le_trans _ (ltW e1)) //. + rewrite reN1 opprB addrA ltr_subl_addl ler_lt_add //. + rewrite (le_trans _ (ltW e1)) //. by case/ler_normlP : (contract_le1 r'%:E). rewrite reN1 -addrA -[X in _ < X]addr0 ltr_add2l ltr_subl_addl addr0. by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. rewrite [contract +oo]/= ltr0_norm ?subr_lt0; last first. - by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. + by case/ltr_normlP : (contract_lt1 r). by rewrite opprB reN1 opprB addrA ltr_subl_addl ltr_add. have : locally r%:E (setT `\ -oo%E) by exists 1. case => _/posnumP[e'] /=; rewrite /ball_ => h. @@ -1253,8 +1274,9 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1]. by apply (@locally_fin_out_above _ e) => //; rewrite re1. move: re1; rewrite neq_lt => /orP[re1|re1]. have ? : `|contract r%:E - (e)%:num| < 1. - rewrite ltr_norml reN1 andTb ltr_subl_addl (@lt_le_trans _ _ 1) // ?ler_addr //. - by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. + rewrite ltr_norml reN1 andTb ltr_subl_addl. + rewrite (@lt_le_trans _ _ 1) // ?ler_addr //. + by case/ltr_normlP : (contract_lt1 r). have ? : `|contract r%:E + (e)%:num| < 1. rewrite ltr_norml re1 andbT -(addr0 (-1)) ler_lt_add //. by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. @@ -1262,10 +1284,12 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1]. (real_of_er (expand (contract r%:E + e%:num)) - r). have e'0 : 0 < e'. rewrite /e' ltxI; apply/andP; split. - rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E) real_of_er_expand //. + rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E). + rewrite real_of_er_expand //. apply: (homo_expand_lt _ (contract_le1 _)); first by rewrite inE ltW. by rewrite ltr_subl_addl ltr_addr. - rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E) real_of_er_expand //. + rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E). + rewrite real_of_er_expand //. apply: (homo_expand_lt (contract_le1 _)); last by rewrite ltr_addl. by rewrite inE ltW. apply/locallyP; exists e' => // r' re'r'; apply reA. @@ -1296,14 +1320,15 @@ move: re1; rewrite le_eqVlt => /orP[re1|re1]. by move: re1; rewrite eq_sym -subr_eq => /eqP <-. have e1 : 1 < e%:num. move: reN1. - rewrite re1 -addrA -opprD ltr_subl_addl ltr_subr_addl -!mulr2n -(mulr_natl e%:num) -{1}(mulr1 2) => ?. + rewrite re1 -addrA -opprD ltr_subl_addl ltr_subr_addl -!mulr2n. + rewrite -(mulr_natl e%:num) -{1}(mulr1 2) => ?. by rewrite -(@ltr_pmul2l _ 2). have Aoo : setT `\ +oo%E `<=` A. move=> x [_]; rewrite /set1 /= => xpoo; apply reA. case: x xpoo => [r' _ | // |_]. have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E). rewrite re1 opprB addrCA -[X in _ < X]addr0 ltr_add2 subr_lt0. - by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. + by case/ltr_normlP : (contract_lt1 r'). rewrite re1 addrAC ltr_subl_addl ltr_add // (lt_trans _ e1) // ltr_oppl. by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. rewrite [contract -oo]/= opprK gtr0_norm ?subr_gt0; last first. @@ -1335,7 +1360,7 @@ rewrite predeq2E => x A; split. rewrite /ball_ real_ltr_norml // ?num_real //. rewrite ger0_norm ?subr_ge0// in re'r'. have H1 : contract (r%:E - e%:num%:E) < contract r'%:E. - move: re'r'; rewrite /e' mc_1_10.Num.Theory.ltr_minr => /andP[Hr'1 Hr'2]. + move: re'r'; rewrite /e' ltxI => /andP[Hr'1 Hr'2]. rewrite /e' ltr_subr_addl addrC -ltr_subr_addl in Hr'1. by rewrite (lt_le_trans Hr'1) // opprB addrCA subrr addr0. move: (homo_expand_lt (contract_le1 _) (contract_le1 _) H1). @@ -1344,15 +1369,14 @@ rewrite predeq2E => x A; split. rewrite rer' /= andbT (@lt_le_trans _ _ 0) //. by rewrite ltr_oppl oppr0. rewrite subr_ge0 -lee_fin -(contractK r%:E) -(contractK r'%:E). - move: r'r; rewrite le_eqVlt => /orP[/eqP -> //|r'r]. - exact/ltW/(homo_expand_lt (contract_le1 _) (contract_le1 _)). + exact/(homo_expand_le (contract_le1 _) (contract_le1 _)). apply reA. rewrite /ball_ real_ltr_norml // ?num_real //. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. apply/andP; split; last first. rewrite (@lt_trans _ _ 0) // subr_lt0 -lte_fin. rewrite -(contractK r%:E) -(contractK r'%:E). - by apply: (homo_expand_lt (contract_le1 _) (contract_le1 _)). + exact: (homo_expand_lt (contract_le1 _) (contract_le1 _)). rewrite ltr_oppl opprB. rewrite /e' in re'r'. have H2 : contract r'%:E < contract (r%:E + e%:num%:E). @@ -1365,21 +1389,17 @@ rewrite predeq2E => x A; split. rewrite ltxI => /andP[re'1 re'2]. have [cr0|cr0] := lerP 0 (contract r%:E). move: re'2; rewrite ler0_norm; last first. - rewrite subr_le0. - by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. + by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E). rewrite opprB ltr_subr_addl addrCA subrr addr0 => h. exfalso. - move: h; apply/negP. - rewrite -leNgt. - by move: (contract_le1 (r%:E + e%:num%:E)); rewrite ler_norml => /andP[]. + move: h; apply/negP; rewrite -leNgt. + by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)). move: re'2; rewrite ler0_norm; last first. - rewrite subr_le0. - by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. + by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E). rewrite opprB ltr_subr_addl addrCA subrr addr0 => h. exfalso. - move: h; apply/negP. - rewrite -leNgt. - by move: (contract_le1 (r%:E + e%:num%:E)); rewrite ler_norml => /andP[]. + move: h; apply/negP; rewrite -leNgt. + by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)). * rewrite /ereal_ball [contract -oo]/=; rewrite opprK. rewrite ltxI => /andP[re'1 _]. move: re'1. @@ -1426,8 +1446,8 @@ rewrite predeq2E => x A; split. exfalso. move: h; apply/negP. rewrite -leNgt [in X in _ <= X]ger0_norm// -ler_subl_addr addrAC. - rewrite subrr add0r -/(contract M%:E) (le_trans _ (ltW (contract_lt1 M))) //. - by rewrite ler_norm. + rewrite subrr add0r -/(contract M%:E). + by rewrite (le_trans _ (ltW (contract_lt1 M))) // ler_norm. * rewrite /ereal_ball /= => _; exact: MA. - case: x => [r [_/posnumP[e] reA]| [_/posnumP[e] reA] | [_/posnumP[e] reA]] //=. + rewrite /ereal_ball in reA. diff --git a/theories/sequences.v b/theories/sequences.v index 1205d382ef..d94571009b 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -65,7 +65,7 @@ Arguments mk_sequence R f /. Notation "[ 'sequence' E ]_ n" := (mk_sequence (fun n => E)) : ring_scope. Notation "R ^nat" := (sequence R) : type_scope. -Notation "'nondecreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> n <= m}) +Notation "'nondecreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> (n <= m)%O}) (at level 10). Notation "'nonincreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> n >= m}) (at level 10). @@ -733,4 +733,110 @@ rewrite -real_of_er_expand // lte_fin; apply k1un. by near: n; exists k. Grab Existential Variables. all: end_near. Qed. +Lemma nondecreasing_seq_ereal_cvg (R : realType) (u_ : nat -> {ereal R}) : + nondecreasing_seq u_ -> u_ --> ereal_sup (u_ @` setT). +Proof. +move=> nd_u_; set S := u_ @` setT; set l := ereal_sup S. +have [Spoo|Spoo] := pselect (S +oo%E). + have [N Nu] : exists N, forall n, (n >= N)%nat -> u_ n = +oo%E. + case: Spoo => N _ uNoo; exists N => n Nn. + by move: (nd_u_ _ _ Nn); rewrite uNoo lee_pinfty_eq => /eqP. + have -> : l = +oo%E by rewrite /l /ereal_sup; exact: supremum_pinfty. + rewrite -(cvg_comp_addn N); set f := (X in X --> _). + rewrite (_ : f = (fun=> +oo%E)); first exact: cvg_cst. + by rewrite funeqE => n; rewrite /f /= Nu // leq_addl. +have [Snoo|Snoo] := pselect (u_ = fun=> -oo%E). + suff : l = -oo%E by move=> ->; rewrite Snoo; exact: cvg_cst. + rewrite /l. + suff -> : S = [set -oo%E] by rewrite ereal_sup_set1. + rewrite predeqE => x; split => [-[n _ <-]|->]. + by rewrite Snoo. + by exists O => //; rewrite Snoo. +have [/eqP|lnoo] := boolP (l == -oo%E). + move/ereal_sup_ninfty => loo. + suff : u_ = (fun=> -oo%E) by []. + by rewrite funeqE => m; apply (loo (u_ m)); exists m. +apply/cvg_ballP => _/posnumP[e]. +have [/eqP {lnoo}loo|lpoo] := boolP (l == +oo%E). + rewrite near_map; near=> n; rewrite /ball /= /ereal_ball. + have unoo : u_ n != -oo%E. + near: n. + have [m /eqP umoo] : exists m, u_ m <> -oo%E. + apply/existsNP => uoo. + by apply/Snoo; rewrite funeqE => ?; rewrite uoo. + exists m => // k mk; apply: contra umoo => /eqP ukoo. + by move/nd_u_ : mk; rewrite ukoo lee_ninfty_eq. + rewrite loo ger0_norm ?subr_ge0; last by case/ler_normlP : (contract_le1 (u_ n)). + have [e2|e2] := lerP 2 e%:num. + rewrite /= ltr_subl_addr addrC -ltr_subl_addr. + case/ler_normlP : (contract_le1 (u_ n)); rewrite ler_oppl => un1 _. + rewrite (@le_lt_trans _ _ (-1)) //. + by rewrite ler_subl_addr addrC -ler_subl_addr opprK (le_trans e2). + by move: un1; rewrite le_eqVlt eq_sym contract_eqN1 (negbTE unoo). + rewrite ltNge; apply/negP. + rewrite ler_subr_addl addrC -ler_subr_addl. + move/homo_expand_le. + rewrite 2!inE. + have leun : (expand (contract +oo - (e)%:num)%R < u_ n)%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. + 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. + have e1 : `| 1 - e%:num | <= 1. + have [e1|e1] := ltrP 1 e%:num. + by rewrite ler_subl_addr (le_trans (ltW e2)). + by rewrite ler_subl_addr ler_addl. + by move/(_ (contract_le1 _) e1); rewrite contractK; apply/negP; rewrite -ltNge. +have [r lr] : exists r, l = r%:E by move: l lnoo lpoo => [] // r' _ _; exists r'. +have [re1|re1] := ltrP (`|contract l - (e)%:num|) 1; last first. + rewrite near_map; near=> n; rewrite /ball /= /ereal_ball /=. + have unoo : u_ n != -oo%E. + near: n. + have [m /eqP umoo] : exists m, u_ m <> -oo%E. + apply/existsNP => uoo. + by apply/Snoo; rewrite funeqE => ?; rewrite uoo. + exists m => // k mk; apply: contra umoo => /eqP ukoo. + by move/nd_u_ : mk; rewrite ukoo lee_ninfty_eq. + rewrite ger0_norm; last first. + by rewrite subr_ge0; apply/homo_contract_le/ereal_sup_ub; exists n. + have [l0|l0] := ger0P (contract l). + have ? : e%:num > contract r%:E. + rewrite ltNge; apply/negP => er. + rewrite lr ger0_norm ?subr_ge0// -ler_subl_addr opprK in re1. + case/ler_normlP : (contract_le1 r%:E) => _ /(le_trans re1); apply/negP. + by rewrite -ltNge ltr_addl. + rewrite lr ltr0_norm ?subr_lt0// opprB in re1. + rewrite ltr_subl_addr addrC -ltr_subl_addr -opprB ltr_oppl lr. + rewrite (lt_le_trans _ re1) // lt_neqAle eqr_oppLR contract_eqN1 unoo /=. + by case/ler_normlP : (contract_le1 (u_ n)). + rewrite ler0_norm in re1; last first. + by rewrite subr_le0 (le_trans (ltW l0)). + rewrite opprB ler_subr_addr addrC -ler_subr_addr in re1. + rewrite ltr_subl_addr (le_lt_trans re1) // -ltr_subl_addl addrAC subrr add0r. + rewrite ltr_neqAle eq_sym contract_eqN1 unoo /=. + by case/ler_normlP : (contract_le1 (u_ n)); rewrite ler_oppl. +pose e' := r - real_of_er (expand (contract l - e%:num)). +have e'0 : 0 < e'. + rewrite /e' subr_gt0 -lte_fin real_of_er_expand //. + rewrite -[in X in (_ < X)%E](contractK r%:E); apply homo_expand_lt. + by rewrite inE ltW. + by rewrite inE; exact: contract_le1. + by rewrite lr ltr_subl_addr // ltr_addl. +have [y [[m _] umx] Se'y] := @ub_ereal_sup_adherent _ S (PosNum e'0) _ lr. +rewrite near_map; near=> n; rewrite /ball /= /ereal_ball /=. +rewrite ger0_norm; last first. + by rewrite subr_ge0; apply/homo_contract_le/ereal_sup_ub; exists n. +move: Se'y; rewrite -{}umx {y} /= => le'um. +have leum : contract l - e%:num < contract (u_ m). + move: le'um; rewrite /e' NERFin -/l [in X in (X - _ < _)%E -> _]lr /= opprB. + rewrite addrCA subrr addr0 real_of_er_expand // => /homo_contract_lt. + by rewrite expandK // inE // ltW // lr. +rewrite ltr_subl_addr addrC -ltr_subl_addr (lt_le_trans leum) //. +by apply/homo_contract_le/nd_u_; near: n; exists m. +Grab Existential Variables. all: end_near. Qed. + End sequences_of_extended_real_numbers. From 25d840876cfa851b07f3920822ca8372468520ba Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 2 Jun 2020 05:42:19 +0200 Subject: [PATCH 4/6] exploiting fully the monotonicity of contract and expand --- theories/normedtype.v | 385 +++++++++++++++++++++++------------------- theories/sequences.v | 46 ++--- 2 files changed, 229 insertions(+), 202 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 4ec13060dc..a919c4dcc5 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -83,6 +83,122 @@ Require Import classical_sets posnum topology prodnormedzmodule. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. + +(********************************) +(* Missing lemmas for mathcommp *) +(********************************) + +Section MonoHomoMorphismTheory_in. + +Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}). +Variables (f : aT -> rT) (g : rT -> aT) (aR : rel aT) (rR : rel rT). + +Hypothesis fgK : {in rD, {on aD, cancel g & f}}. +Hypothesis mem_g : {homo g : x / x \in rD >-> x \in aD}. + +Lemma homoRL_in : + {in aD &, {homo f : x y / aR x y >-> rR x y}} -> + {in rD & aD, forall x y, aR (g x) y -> rR x (f y)}. +Proof. by move=> Hf x y hx hy /Hf; rewrite fgK ?mem_g// ?inE; apply. Qed. + +Lemma homoLR_in : + {in aD &, {homo f : x y / aR x y >-> rR x y}} -> + {in aD & rD, forall x y, aR x (g y) -> rR (f x) y}. +Proof. by move=> Hf x y hx hy /Hf; rewrite fgK ?mem_g// ?inE; apply. Qed. + +Lemma homo_mono_in : + {in aD &, {homo f : x y / aR x y >-> rR x y}} -> + {in rD &, {homo g : x y / rR x y >-> aR x y}} -> + {in rD &, {mono g : x y / rR x y >-> aR x y}}. +Proof. +move=> mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact. +by apply: contraNF=> /mf; rewrite !fgK ?mem_g//; apply. +Qed. + +Lemma monoLR_in : + {in aD &, {mono f : x y / aR x y >-> rR x y}} -> + {in aD & rD, forall x y, rR (f x) y = aR x (g y)}. +Proof. by move=> mf x y hx hy; rewrite -{1}[y]fgK ?mem_g// mf ?mem_g. Qed. + +Lemma monoRL_in : + {in aD &, {mono f : x y / aR x y >-> rR x y}} -> + {in rD & aD, forall x y, rR x (f y) = aR (g x) y}. +Proof. by move=> mf x y hx hy; rewrite -{1}[x]fgK ?mem_g// mf ?mem_g. Qed. + +Lemma can_mono_in : + {in aD &, {mono f : x y / aR x y >-> rR x y}} -> + {in rD &, {mono g : x y / rR x y >-> aR x y}}. +Proof. by move=> mf x y hx hy; rewrite -mf ?mem_g// !fgK ?mem_g. Qed. + +End MonoHomoMorphismTheory_in. +Arguments homoRL_in {aT rT aD rD f g aR rR}. +Arguments homoLR_in {aT rT aD rD f g aR rR}. +Arguments homo_mono_in {aT rT aD rD f g aR rR}. +Arguments monoLR_in {aT rT aD rD f g aR rR}. +Arguments monoRL_in {aT rT aD rD f g aR rR}. +Arguments can_mono_in {aT rT aD rD f g aR rR}. + +Section onW_can. + +Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}). +Variables (f : aT -> rT) (g : rT -> aT). + +Lemma onW_can : cancel g f -> {on aD, cancel g & f}. +Proof. by move=> fgK x xaD; apply: fgK. Qed. + +Lemma onW_can_in : {in rD, cancel g f} -> {in rD, {on aD, cancel g & f}}. +Proof. by move=> fgK x xrD xaD; apply: fgK. Qed. + +Lemma in_onW_can : cancel g f -> {in rD, {on aD, cancel g & f}}. +Proof. by move=> fgK x xrD xaD; apply: fgK. Qed. + +Lemma onT_can : (forall x, g x \in aD) -> {on aD, cancel g & f} -> cancel g f. +Proof. by move=> mem_g fgK x; apply: fgK. Qed. + +Lemma onT_can_in : {homo g : x / x \in rD >-> x \in aD} -> + {in rD, {on aD, cancel g & f}} -> {in rD, cancel g f}. +Proof. by move=> mem_g fgK x x_rD; apply/fgK/mem_g. Qed. + +Lemma in_onT_can : (forall x, g x \in aD) -> + {in rT, {on aD, cancel g & f}} -> cancel g f. +Proof. by move=> mem_g fgK x; apply/fgK. Qed. + + +End onW_can. +Arguments onW_can {aT rT} aD {f g}. +Arguments onW_can_in {aT rT} aD {rD f g}. +Arguments in_onW_can {aT rT} aD rD {f g}. +Arguments onT_can {aT rT} aD {f g}. +Arguments onW_can_in {aT rT} aD {rD f g}. +Arguments in_onT_can {aT rT} aD {f g}. + +Section inj_can_sym_in_on. +Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}). +Variables (f : aT -> rT) (g : rT -> aT). + +Lemma inj_can_sym_in_on : {homo f : x / x \in aD >-> x \in rD} -> + {in aD, {on rD, cancel f & g}} -> + {in [pred x | x \in rD & g x \in aD], injective g} -> + {in rD, {on aD, cancel g & f}}. +Proof. by move=> fD fK gI x x_rD gx_aD; apply: gI; rewrite ?inE ?fK ?fD. Qed. + +Lemma inj_can_sym_on : {in aD, cancel f g} -> + {in [pred x | g x \in aD], injective g} -> {on aD, cancel g & f}. +Proof. by move=> fK gI x gx_aD; apply: gI; rewrite ?inE ?fK. Qed. + +Lemma inj_can_sym_in : {homo f \o g : x / x \in rD} -> {on rD, cancel f & g} -> + {in rD, injective g} -> {in rD, cancel g f}. +Proof. by move=> fgD fK gI x x_rD; apply: gI; rewrite ?fK ?fgD. Qed. + +End inj_can_sym_in_on. +Arguments inj_can_sym_in_on {aT rT aD rD f g}. +Arguments inj_can_sym_on {aT rT aD f g}. +Arguments inj_can_sym_in {aT rT rD f g}. + +(*************************) +(* Mathcomp analysis now *) +(*************************) + Import Order.TTheory GRing.Theory Num.Def Num.Theory. Local Open Scope ring_scope. @@ -861,31 +977,9 @@ Proof. by rewrite /contract mul0r. Qed. Lemma contractN x : contract (- x) = - contract x. Proof. by case: x => //= [r|]; [ rewrite normrN mulNr | rewrite opprK]. Qed. -Lemma contract_eq0 x : (contract x == 0) = (x == 0%:E). -Proof. -case: x => [r| |] /=. -- apply/idP/idP => [|/eqP[->]]; last by rewrite mul0r. - rewrite mulf_eq0 => /orP[/eqP -> //|]. - by rewrite invr_eq0 paddr_eq0 // oner_eq0. -- exact/idP/idP. -- by rewrite -eqr_opp opprK oppr0 oner_eq0. -Qed. - -Lemma contract_eqN1 x : (contract x == -1) = (x == -oo%E). -Proof. -apply/eqP/eqP => [|->//]; move: x => -[r /= /eqP | /= | //]; last first. - by move/eqP; rewrite -subr_eq0 opprK (_ : _ + _ = 2%:R) // pnatr_eq0. -rewrite -eqr_oppLR -mulNr => /eqP/divr1_eq/eqP; rewrite eqr_oppLR => r1. -have r0 : r < 0 by rewrite (eqP r1) oppr_lt0 ltr_spaddl. -by move: r1; rewrite ltr0_norm // -subr_eq0 opprK addrCA subrr addr0 oner_eq0. -Qed. - -Lemma contract_eq1 x : (contract x == 1) = (x == +oo%E). -Proof. by rewrite -(oppeK x) contractN eqr_oppLR contract_eqN1; case: x. Qed. - Definition expand r : {ereal R} := - if r == 1 then +oo%E else - if r == -1 then -oo%E else + 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 expand1 : expand 1 = +oo%E. Proof. by rewrite /expand eqxx. Qed. @@ -898,54 +992,27 @@ Proof. by rewrite /expand eq_sym oner_eq0 -eqr_oppLR oppr0 eq_sym oner_eq0 mul0r. Qed. -Lemma expand_eqoo (r : R) : (expand r == +oo%E) = (r == 1). +(* Cyril: TODO: add to ssrnum *) +Lemma nlt_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false). Proof. -apply/eqP/eqP => [|->]; last by rewrite expand1. -by rewrite /expand; case: ifPn => [/eqP//|?]; case: ifPn. +move=> x1; split; last by rewrite lt_eqF // (le_lt_trans (ler_norm _) x1). +by move: x1; rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF. Qed. -Lemma contractK : cancel contract expand. -Proof. -case=> [r| |]; rewrite /expand /= ?eqxx //. -- rewrite (_ : _ == 1 = false); last first. - apply/negP => /eqP/divr1_eq; apply/eqP; rewrite lt_eqF //. - by rewrite -{1}(add0r r) ltr_le_add // real_ler_norm // num_real. - rewrite (_ : _ == -1 = false); last first. - apply/negP; rewrite -eqr_oppLR -mulrN -invrN => /eqP/divr1_eq/eqP. - rewrite -eqr_oppLR lt_eqF // -{1}(add0r (- r)) ltr_le_add //. - by rewrite real_ler_normr ?num_real // lexx orbT. - congr (_ %:E). - have ? : 1 + `|r| != 0 by rewrite lt0r_neq0 // -(addr0 0) ltr_le_add. - rewrite -[RHS]mulr1 -mulrA; congr (r * _). - rewrite normrM normrV ?unitfE // (@ger0_norm _ (1 + `|r|)) ?addr_ge0 //. - rewrite -{2}(@divrr _ (1 + `|r|)) ?unitfE // -mulrBl invrM; last 2 first. - by rewrite addrK unitfE. - by rewrite unitfE invr_eq0. - by rewrite invrK mulrA mulVr ?unitfE // addrK divr1. -- rewrite eq_sym -subr_eq0 opprK {1 2}(_ : 1 = 1%:R) // -natrD /= addn1 /=. - by rewrite (_ : _ == 0 = false) //; apply/negP/negP. -Qed. - -Lemma nlt_eqF (x y : R) : `|x| < y -> x == y = false. -Proof. by move=> x1; rewrite lt_eqF // (le_lt_trans (ler_norm _) x1). Qed. - -Lemma ngt_eqF (x y : R) : `|x| < y -> x == -y = false. -Proof. by rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF. Qed. - Lemma expandK : {in [pred x | `|x| <= 1], cancel expand contract}. Proof. -move=> x; rewrite inE le_eqVlt => /orP[|x1]. +move=> x. rewrite inE le_eqVlt => /orP[|x1]. by rewrite eqr_norml => /andP[/orP[]/eqP->{x}]; rewrite ?(expand1,expandN1). -rewrite /expand nlt_eqF // ngt_eqF //. +rewrite /expand nlt_eqF // nlt_eqF //. 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. by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym nlt_eqF. have x_nneq0 : 1 - x / (1 + x) != 0. rewrite -[X in X + _](@divrr _ (1 + x)) -?mulrBl; last first. - by rewrite unitfE addrC addr_eq0 ngt_eqF. - by rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym ngt_eqF. -wlog : x x1 x_pneq0 x_nneq0 / (0 <= x) => wlog_x0. + rewrite unitfE addrC addr_eq0 nlt_eqF//. + by rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym nlt_eqF. +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)). @@ -958,12 +1025,9 @@ rewrite -[X in X + _ / _](@divrr _ (1 - x)) -?mulrDl ?subrK ?div1r //. by rewrite unitfE subr_eq0 eq_sym nlt_eqF. Qed. -Lemma bijective_contract : {on [pred x| `|x| <= 1], bijective contract}. -Proof. exists expand; [by move=> x _; rewrite contractK | exact: expandK]. Qed. - -Lemma homo_contract_lt : {homo contract : x y / (x < y)%O}. +Lemma le_contract : {mono contract : x y / (x <= y)%O}. Proof. -move=> -[r0 | | ] [r1 | _ | _] //=. +apply: le_mono; move=> -[r0 | | ] [r1 | _ | _] //=. - rewrite lte_fin => r0r1; rewrite ltr_pdivr_mulr ?ltr_paddr//. rewrite mulrAC ltr_pdivl_mulr ?ltr_paddr// 2?mulrDr 2?mulr1. have [r10|?] := ler0P r1; last first. @@ -977,61 +1041,65 @@ move=> -[r0 | | ] [r1 | _ | _] //=. - by rewrite -subr_gt0 opprK. Qed. -Lemma homo_contract_le : {homo contract : x y / (x <= y)%O}. -Proof. exact/ltW_homo/homo_contract_lt. Qed. - -Lemma homo_expand_lt : {in [pred x| `|x| <= 1] & [pred x| `|x| <= 1], - {homo expand : x y / (x < y)%O}}. -Proof. -move=> x y; rewrite !inE => x1 y1 xy. -move: x1; rewrite le_eqVlt => /orP[|x1]. - have [x0|x0] := lerP 0 x. - rewrite ger0_norm // => /eqP x1; exfalso. - move: y1; rewrite ler_norml => /andP[_]/(lt_le_trans xy). - by rewrite x1 ltxx. - rewrite ltr0_norm // eqr_oppLR => /eqP x1. - rewrite x1 expandN1 /expand; case: ifPn => // y_neq1. - case: ifPn => [/eqP y_neqN1|?]; last by rewrite lte_ninfty. - by move: xy; rewrite x1 y_neqN1 ltxx. -move: y1; rewrite le_eqVlt => /orP[|y1]. - have [y0|y0] := lerP 0 y. - rewrite ger0_norm // => /eqP y1; rewrite y1 expand1. - by rewrite /expand nlt_eqF // ngt_eqF // lte_pinfty. - rewrite ltr0_norm // eqr_oppLR => /eqP y1; exfalso. - move: x1; rewrite ltr_norml => /andP[x1 _]. - by move: xy; rewrite y1 => /(lt_trans x1); rewrite ltxx. -rewrite /expand (nlt_eqF x1) (nlt_eqF y1) (ngt_eqF x1) (ngt_eqF y1). -have [x0|x0] := lerP 0 x. - move: (x0); rewrite le_eqVlt => /orP[/eqP <-|{x0}x0]. - by rewrite mul0r lte_fin divr_gt0 // ?subr_gt0 // (le_lt_trans x0). - rewrite lte_fin gtr0_norm // gtr0_norm; last by rewrite (lt_trans x0). - rewrite ltr_pdivr_mulr; last first. - by rewrite subr_gt0 (le_lt_trans _ x1) // ler_norm. - rewrite mulrAC -ltr_pdivr_mulr; last first. - by rewrite invr_gt0 // subr_gt0 (le_lt_trans _ y1) // ler_norm. - by rewrite invrK !(mulrBr,mulr1) mulrC ltr_le_sub. -rewrite ltr0_norm // opprK lte_fin ltr_pdivr_mulr; last first. - by rewrite -ltr_subl_addr sub0r -(ltr0_norm x0). -rewrite mulrAC -ltr_pdivr_mulr; last by rewrite invr_gt0 subr_gt0. -rewrite invrK. -have [|y0] := lerP 0 y. - rewrite le_eqVlt => /orP[/eqP <-|y0]. - by rewrite normr0 mul0r subr0 mulr1. - rewrite gtr0_norm // (@le_lt_trans _ _ 0) //. - by rewrite nmulr_rle0 // subr_ge0 (le_trans _ (ltW y1)) // ler_norm. - rewrite mulr_gt0 // -ltr_subl_addl sub0r ltr_oppl. - by rewrite (le_lt_trans _ x1) // ler0_norm // ltW. -by rewrite ltr0_norm // opprK !mulrDr !mulr1 mulrC ltr_add2r. -Qed. - -Lemma homo_expand_le : {in [pred x| `|x| <= 1] & - [pred x| `|x| <= 1], {homo expand : x y / (x <= y)%O}}. -Proof. -by apply/homoW_in => //= x y x1 y1; rewrite -2!lt_neqAle; apply/homo_expand_lt. -Qed. +Definition lt_contract := leW_mono le_contract. +Definition contract_inj := mono_inj lexx le_anti le_contract. + +Lemma le_expand : {in [pred x| `|x| <= 1] &, {mono expand : x y / (x <= y)%O}}. +Proof. exact: can_mono_in (onW_can_in predT expandK) _ (in2W le_contract). Qed. + +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 // ngt_eqF. Qed. +Proof. by move=> x1; rewrite /expand nlt_eqF // nlt_eqF. Qed. + +Lemma contractK : cancel contract expand. +Proof. +apply: (onT_can [pred x | `|x| <= 1] contract_le1). +exact: inj_can_sym_on expandK (in1W contract_inj). +Qed. + +Lemma bijective_contract : {on [pred x| `|x| <= 1], bijective contract}. +Proof. exists expand; [exact: in1W contractK | exact: expandK]. Qed. + +Definition le_expandLR := monoLR_in + (in_onW_can _ predT contractK) (fun x _ => contract_le1 x) le_expand. +Definition lt_expandLR := monoLR_in + (in_onW_can _ predT contractK) (fun x _ => contract_le1 x) lt_expand. +Definition le_expandRL := monoRL_in + (in_onW_can _ predT contractK) (fun x _ => contract_le1 x) le_expand. +Definition lt_expandRL := monoRL_in + (in_onW_can _ predT contractK) (fun x _ => contract_le1 x) lt_expand. +Definition le_contractLR := monoLR_in + (onW_can_in predT expandK) (fun x _ => isT) (in2W le_contract). +Definition lt_contractLR := monoLR_in + (onW_can_in predT expandK) (fun x _ => isT) (in2W lt_contract). +Definition le_contractRL := monoRL_in + (onW_can_in predT expandK) (fun x _ => isT) (in2W lt_contract). +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. + +Lemma contract_eqN1 x : (contract x == -1) = (x == -oo%E). +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_eqNoo (r : R) : (expand r == -oo%E) = (r == -1). +Proof. +apply/eqP/eqP => [|->]; last by rewrite expandN1. +by rewrite /expand; do![case: (altP eqP) => ?]. +Qed. End contract_expand. @@ -1066,9 +1134,8 @@ case => [r | | //]. by rewrite ger0_norm ?ltr_subl_addl ?ltr_addr // subr_ge0. move=> h; apply reA; rewrite gtr0_norm ?subr_gt0; last first. by case/ltr_normlP : (contract_lt1 r). - rewrite ltr_subl_addl addrC -ltr_subl_addl -[X in X < _]expandK; last first. - by rewrite inE ger0_norm ?ler_subl_addl ?ler_addr // subr_ge0. - exact: homo_contract_lt. + rewrite ltr_subl_addl addrC -ltr_subl_addl -[X in X < _]expandK ?lt_contract//. + by rewrite inE ger0_norm ?ler_subl_addl ?ler_addr // subr_ge0. - by move=> _; apply reA; rewrite /= subrr normr0. Qed. @@ -1150,26 +1217,21 @@ have X : `|contract r%:E - (e)%:num| < 1. pose e' := r - real_of_er (expand (contract r%:E - e%:num)). have e'0 : 0 < e'. rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E). - rewrite real_of_er_expand //. - apply: (homo_expand_lt _ (contract_le1 _)); first by rewrite inE ltW. + rewrite real_of_er_expand // lt_expand ?inE ?contract_le1// ?ltW//. by rewrite ltr_subl_addl ltr_addr. apply/locallyP; exists e' => // r' re'r'; apply reA. rewrite /ball /= in re'r'. have [rr'|r'r] := lerP r r'. move: rr'; rewrite le_eqVlt => /orP[/eqP->|rr']; first by rewrite subrr normr0. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. - rewrite ltr0_norm; last first. - by rewrite subr_lt0; apply: homo_contract_lt; rewrite lte_fin. + rewrite ltr0_norm; last by rewrite subr_lt0 lt_contract lte_fin. rewrite opprB ltr_subl_addl (lt_le_trans _ re1) //. by case/ltr_normlP : (contract_lt1 r'). -rewrite gtr0_norm ?subr_gt0//; last by apply: homo_contract_lt; rewrite lte_fin. +rewrite gtr0_norm ?subr_gt0// ?lt_contract ?lte_fin//. move: re'r'. rewrite gtr0_norm // ?subr_gt0// /e'. rewrite -ltr_subl_addl addrAC subrr add0r ltr_oppl opprK -lte_fin. -rewrite real_of_er_expand //. -rewrite -[in X in X -> _](contractK r'%:E) => /homo_contract_lt r'e'r. -rewrite expandK in r'e'r; last by rewrite inE ltW. -rewrite expandK in r'e'r; last by rewrite inE contract_le1. +rewrite real_of_er_expand // lt_expandLR ?inE ?ltW//. by rewrite ltr_subl_addl addrC -ltr_subl_addl. Qed. @@ -1187,23 +1249,18 @@ pose e' : R := real_of_er (expand (contract r%:E + e%:num)) - r. have e'0 : 0 < e'. rewrite /e'. rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E). - rewrite real_of_er_expand //. - apply: (homo_expand_lt (contract_le1 _)); last by rewrite ltr_addl. - by rewrite inE ltW. + by rewrite real_of_er_expand // lt_expand ?inE ?contract_le1 ?ltr_addl ?ltW. apply/locallyP; exists e' => // r' r'e'r; apply reA. rewrite /ball /= in r'e'r. have [rr'|r'r] := lerP r r'. move: rr'; rewrite le_eqVlt => /orP[/eqP->|rr']. by rewrite subrr normr0. rewrite ltr0_norm ?subr_lt0// opprB in r'e'r. - rewrite ltr0_norm; last first. - by rewrite subr_lt0; apply: homo_contract_lt; rewrite lte_fin. + rewrite ltr0_norm ?subr_lt0 ?lt_contract ?lte_fin//. rewrite opprB; move: r'e'r. rewrite /e' -ltr_subl_addr opprK subrK -lte_fin real_of_er_expand //. - move=> r'e'r; rewrite ltr_subl_addl. - by move/homo_contract_lt : r'e'r; rewrite expandK // inE ltW. -rewrite gtr0_norm; last first. - by rewrite subr_gt0; apply homo_contract_lt; rewrite lte_fin. + by rewrite lt_expandRL ?inE ?ltW// ltr_subl_addl. +rewrite gtr0_norm ?subr_gt0 ?lt_contract ?lte_fin//. rewrite ltr_subl_addl addrC -ltr_subl_addl (le_lt_trans reN1) //. by move: (contract_lt1 r'); rewrite ltr_norml => /andP[]. Qed. @@ -1220,12 +1277,10 @@ case: x => [r'| |] //. - have [|r'r] := lerP r r'. rewrite le_eqVlt => /orP[/eqP <-|rr']. by rewrite subrr normr0. - rewrite ltr0_norm; last first. - by rewrite subr_lt0; apply: homo_contract_lt; rewrite lte_fin. + rewrite ltr0_norm ?subr_lt0 ?lt_contract ?lte_fin//. rewrite opprB ltr_subl_addl (le_lt_trans _ re1) //. by move: (contract_le1 r'%:E); rewrite ler_norml => /andP[]. - rewrite gtr0_norm; last first. - by rewrite subr_gt0; apply homo_contract_lt; rewrite lte_fin. + rewrite gtr0_norm ?subr_gt0 ?lt_contract ?lte_fin //. rewrite ltr_subl_addl addrC -ltr_subl_addl (lt_le_trans reN1) //. by move: (contract_le1 r'%:E); rewrite ler_norml => /andP[]. - rewrite [contract +oo]/= ler0_norm; last first. @@ -1285,33 +1340,27 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1]. have e'0 : 0 < e'. rewrite /e' ltxI; apply/andP; split. rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E). - rewrite real_of_er_expand //. - apply: (homo_expand_lt _ (contract_le1 _)); first by rewrite inE ltW. + rewrite real_of_er_expand // lt_expand// ?inE ?contract_le1 ?ltW//. by rewrite ltr_subl_addl ltr_addr. rewrite subr_gt0 -lte_fin -[in X in (X < _)%E](contractK r%:E). - rewrite real_of_er_expand //. - apply: (homo_expand_lt (contract_le1 _)); last by rewrite ltr_addl. - by rewrite inE ltW. + rewrite real_of_er_expand//. + by rewrite lt_expand ?inE ?contract_le1 ?ltr_addl ?ltW. apply/locallyP; exists e' => // r' re'r'; apply reA. rewrite /ball /= in re'r'. have [|r'r] := lerP r r'. rewrite le_eqVlt => /orP[/eqP->|rr']. by rewrite subrr normr0. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. - rewrite ltr0_norm; last first. - by rewrite subr_lt0; apply: homo_contract_lt; rewrite lte_fin. + rewrite ltr0_norm ?subr_lt0 ?lt_contract ?lte_fin//. rewrite opprB; move: re'r'. rewrite /e' ltxI => /andP[_]. rewrite -ltr_subl_addr opprK subrK -lte_fin real_of_er_expand //. - move=> r'e'r; rewrite ltr_subl_addl. - by move/homo_contract_lt : r'e'r; rewrite expandK // inE ltW. + by move=> r'e'r; rewrite ltr_subl_addl lt_contractLR ?inE ?ltW. move: re'r'; rewrite ltxI => /andP[]. rewrite gtr0_norm ?subr_gt0 // -ltr_subl_addl addrAC subrr add0r ltr_oppl. rewrite opprK -lte_fin real_of_er_expand // => r'e'r _. - rewrite gtr0_norm; last first. - by rewrite subr_gt0; apply homo_contract_lt; rewrite lte_fin. - rewrite ltr_subl_addl addrC -ltr_subl_addl. - by move/homo_contract_lt : r'e'r; rewrite expandK // inE ltW. + rewrite gtr0_norm ?subr_gt0 ?lt_contract ?lte_fin//. + by rewrite ltr_subl_addl addrC -ltr_subl_addl lt_contractRL ?inE ?ltW. by apply (@locally_fin_out_above _ e) => //; rewrite ltW. have [re1|re1] := ltrP 1 (contract r%:E + (e)%:num). exact: (@locally_fin_out_above_below _ e). @@ -1350,9 +1399,8 @@ rewrite predeq2E => x A; split. (contract (r%:E + e%:num%:E) - contract r%:E). exists e'. rewrite /e' ltxI; apply/andP; split. - by rewrite subr_gt0 homo_contract_lt //= lte_fin ltr_subl_addr ltr_addl. - rewrite subr_gt0; apply homo_contract_lt. - by rewrite lte_fin ltr_addl. + by rewrite subr_gt0 lt_contract lte_fin ltr_subl_addr ltr_addl. + by rewrite subr_gt0 lt_contract lte_fin ltr_addl. case=> [r' re'r'| |]. * rewrite /ereal_ball in re'r'. have [r'r|rr'] := lerP (contract r'%:E) (contract r%:E). @@ -1363,20 +1411,17 @@ rewrite predeq2E => x A; split. move: re'r'; rewrite /e' ltxI => /andP[Hr'1 Hr'2]. rewrite /e' ltr_subr_addl addrC -ltr_subr_addl in Hr'1. by rewrite (lt_le_trans Hr'1) // opprB addrCA subrr addr0. - move: (homo_expand_lt (contract_le1 _) (contract_le1 _) H1). + have := H1; rewrite lt_contractLR ?inE ?contract_le1 //. rewrite !contractK => rer'. rewrite lte_fin ltr_subl_addr addrC -ltr_subl_addr in rer'. rewrite rer' /= andbT (@lt_le_trans _ _ 0) //. by rewrite ltr_oppl oppr0. - rewrite subr_ge0 -lee_fin -(contractK r%:E) -(contractK r'%:E). - exact/(homo_expand_le (contract_le1 _) (contract_le1 _)). + by rewrite subr_ge0 -lee_fin -le_contract. apply reA. rewrite /ball_ real_ltr_norml // ?num_real //. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. apply/andP; split; last first. - rewrite (@lt_trans _ _ 0) // subr_lt0 -lte_fin. - rewrite -(contractK r%:E) -(contractK r'%:E). - exact: (homo_expand_lt (contract_le1 _) (contract_le1 _)). + by rewrite (@lt_trans _ _ 0) // subr_lt0 -lte_fin -lt_contract//. rewrite ltr_oppl opprB. rewrite /e' in re'r'. have H2 : contract r'%:E < contract (r%:E + e%:num%:E). @@ -1384,7 +1429,7 @@ rewrite predeq2E => x A; split. by rewrite ltr_subl_addr subrK in Hr'2. rewrite ltr_subl_addr -lte_fin -(contractK (_ + r)%:E). rewrite addrC -(contractK r'%:E) //. - exact: (homo_expand_lt (contract_le1 _) (contract_le1 _)). + by rewrite lt_expand ?inE ?contract_le1. * rewrite /ereal_ball [contract +oo]/=. rewrite ltxI => /andP[re'1 re'2]. have [cr0|cr0] := lerP 0 (contract r%:E). @@ -1419,8 +1464,7 @@ rewrite predeq2E => x A; split. rewrite ger0_norm in rM1; last first. by rewrite subr_ge0 // (le_trans _ (contract_le1 r%:E)) // ler_norm. rewrite ltr_subl_addr addrC addrCA addrC -ltr_subl_addr subrr subr_gt0 in rM1. - rewrite -lte_fin -(contractK M%:E) -(contractK r%:E). - exact: (homo_expand_lt (contract_le1 _) (contract_le1 _)). + by rewrite -lte_fin -lt_contract. * rewrite /ereal_ball /= subrr normr0 => h. exact: MA. * rewrite /ereal_ball /= opprK => h {MA}. @@ -1440,8 +1484,7 @@ rewrite predeq2E => x A; split. rewrite ler_subl_addl addr0 ltW //. by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. rewrite opprB opprK -ltr_subl_addl addrK in rM1. - rewrite -lte_fin -(contractK M%:E) -(contractK r%:E). - exact: (homo_expand_lt (contract_le1 _) (contract_le1 _)). + by rewrite -lte_fin -lt_contract. * rewrite /ereal_ball /= -opprD normrN => h {MA}. exfalso. move: h; apply/negP. @@ -1579,7 +1622,7 @@ Definition numFieldType_NormedModMixin (R : numFieldType) := NormedModMixin (@R_normZ R). Canonical numFieldType_normedModType (R : numFieldType) := NormedModType R R^o (numFieldType_NormedModMixin R). - + Section NormedModule_numDomainType. Variables (R : numDomainType) (V : normedModType R). diff --git a/theories/sequences.v b/theories/sequences.v index d94571009b..68f633e21a 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -710,27 +710,21 @@ have [e1|e1] := lerP 1 e%:num. rewrite /ball /= /ereal_ball [contract +oo]/= ger0_norm ?subr_ge0; last first. by move: (contract_le1 (u_ n)%:E); rewrite ler_norml => /andP[]. rewrite ltr_subl_addr addrC -ltr_subl_addr. - suff : contract 1%:E < contract (u_ n)%:E. - apply/le_lt_trans. - by rewrite (@le_trans _ _ 0) // ?subr_le0 //= normr1 divr_ge0. - apply homo_contract_lt; rewrite lte_fin; apply k1un. - by near: n; exists k. + have /le_lt_trans->//: contract 1%:E < contract (u_ n)%:E. + by rewrite lt_contract lte_fin k1un//; near: n; exists k. + by rewrite (@le_trans _ _ 0) // ?subr_le0 //= normr1 divr_ge0. have onee1 : `|1 - e%:num| < 1. by rewrite gtr0_norm // ?subr_gt0 // ltr_subl_addl addrC -ltr_subl_addl subrr. have : 0 < real_of_er (expand (1 - e%:num)). - rewrite -lte_fin real_of_er_expand // -expand0. - apply homo_expand_lt; by - [rewrite inE normr0| rewrite inE ltW| rewrite subr_gt0]. + rewrite -lte_fin real_of_er_expand //. + by rewrite lt_expandRL ?inE ?ltW// contract0 subr_gt0. case/uoo => k _ k1un; near=> n. rewrite /ball /= /ereal_ball [contract +oo]/= ger0_norm ?subr_ge0; last first. by move: (contract_le1 (u_ n)%:E); rewrite ler_norml => /andP[]. rewrite ltr_subl_addr addrC -ltr_subl_addr. suff : `|1 - e%:num| < contract (u_ n)%:E by exact: le_lt_trans (ler_norm _). -rewrite gtr0_norm ?subr_gt0 // -(@expandK R (1 - e%:num)); last first. - by rewrite inE gtr0_norm ?subr_gt0// ler_subl_addr addrC -ler_subl_addr subrr. -rewrite -lte_fin; apply/homo_contract_lt. -rewrite -real_of_er_expand // lte_fin; apply k1un. -by near: n; exists k. +rewrite gtr0_norm ?subr_gt0 // lt_contractRL ?inE ?ltW//. +by rewrite -real_of_er_expand // lte_fin k1un//; near: n; exists k. Grab Existential Variables. all: end_near. Qed. Lemma nondecreasing_seq_ereal_cvg (R : realType) (u_ : nat -> {ereal R}) : @@ -773,11 +767,7 @@ have [/eqP {lnoo}loo|lpoo] := boolP (l == +oo%E). rewrite (@le_lt_trans _ _ (-1)) //. by rewrite ler_subl_addr addrC -ler_subl_addr opprK (le_trans e2). by move: un1; rewrite le_eqVlt eq_sym contract_eqN1 (negbTE unoo). - rewrite ltNge; apply/negP. - rewrite ler_subr_addl addrC -ler_subr_addl. - move/homo_expand_le. - rewrite 2!inE. - have leun : (expand (contract +oo - (e)%:num)%R < u_ n)%E. + rewrite ltr_subl_addr addrC -ltr_subl_addr lt_contractRL ?inE//=. 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_. @@ -786,11 +776,9 @@ have [/eqP {lnoo}loo|lpoo] := boolP (l == +oo%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. - have e1 : `| 1 - e%:num | <= 1. have [e1|e1] := ltrP 1 e%:num. - by rewrite ler_subl_addr (le_trans (ltW e2)). + by rewrite ler_subl_addr (le_trans (ltW e2)). by rewrite ler_subl_addr ler_addl. - by move/(_ (contract_le1 _) e1); rewrite contractK; apply/negP; rewrite -ltNge. have [r lr] : exists r, l = r%:E by move: l lnoo lpoo => [] // r' _ _; exists r'. have [re1|re1] := ltrP (`|contract l - (e)%:num|) 1; last first. rewrite near_map; near=> n; rewrite /ball /= /ereal_ball /=. @@ -801,8 +789,7 @@ have [re1|re1] := ltrP (`|contract l - (e)%:num|) 1; last first. by apply/Snoo; rewrite funeqE => ?; rewrite uoo. exists m => // k mk; apply: contra umoo => /eqP ukoo. by move/nd_u_ : mk; rewrite ukoo lee_ninfty_eq. - rewrite ger0_norm; last first. - by rewrite subr_ge0; apply/homo_contract_le/ereal_sup_ub; exists n. + rewrite ger0_norm ?subr_ge0 ?le_contract ?ereal_sup_ub//; last by exists n. have [l0|l0] := ger0P (contract l). have ? : e%:num > contract r%:E. rewrite ltNge; apply/negP => er. @@ -822,21 +809,18 @@ have [re1|re1] := ltrP (`|contract l - (e)%:num|) 1; last first. pose e' := r - real_of_er (expand (contract l - e%:num)). have e'0 : 0 < e'. rewrite /e' subr_gt0 -lte_fin real_of_er_expand //. - rewrite -[in X in (_ < X)%E](contractK r%:E); apply homo_expand_lt. - by rewrite inE ltW. - by rewrite inE; exact: contract_le1. + rewrite lt_expandLR ?inE ?ltW//. by rewrite lr ltr_subl_addr // ltr_addl. have [y [[m _] umx] Se'y] := @ub_ereal_sup_adherent _ S (PosNum e'0) _ lr. rewrite near_map; near=> n; rewrite /ball /= /ereal_ball /=. -rewrite ger0_norm; last first. - by rewrite subr_ge0; apply/homo_contract_le/ereal_sup_ub; exists n. +rewrite ger0_norm ?subr_ge0 ?le_contract ?ereal_sup_ub//; last by exists n. move: Se'y; rewrite -{}umx {y} /= => le'um. have leum : contract l - e%:num < contract (u_ m). + rewrite lt_contractRL ?inE ?ltW//. move: le'um; rewrite /e' NERFin -/l [in X in (X - _ < _)%E -> _]lr /= opprB. - rewrite addrCA subrr addr0 real_of_er_expand // => /homo_contract_lt. - by rewrite expandK // inE // ltW // lr. + by rewrite addrCA subrr addr0 real_of_er_expand //. rewrite ltr_subl_addr addrC -ltr_subl_addr (lt_le_trans leum) //. -by apply/homo_contract_le/nd_u_; near: n; exists m. +by rewrite le_contract nd_u_//; near: n; exists m. Grab Existential Variables. all: end_near. Qed. End sequences_of_extended_real_numbers. From ff2de7d67b739ac14567e5413a197cf40b2c15e1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 2 Jun 2020 17:23:08 +0900 Subject: [PATCH 5/6] 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 cae19b75e0..688e3f66f2 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 a919c4dcc5..de98e14929 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 68f633e21a..1ee2e6ba44 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. From 861a90d32f7108f79b881c7eab525db0ef2feaff Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 9 Jun 2020 19:01:17 +0900 Subject: [PATCH 6/6] minor fixes --- CHANGELOG_UNRELEASED.md | 3 ++- theories/ereal.v | 3 +++ theories/normedtype.v | 45 +++++++++++++++++++++++++++++++---------- theories/sequences.v | 6 +++--- 4 files changed, 42 insertions(+), 15 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 688e3f66f2..2e0084a7ac 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -9,7 +9,7 @@ - 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` @@ -17,6 +17,7 @@ * `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 diff --git a/theories/ereal.v b/theories/ereal.v index d6df07a641..c624a0316d 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -354,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. diff --git a/theories/normedtype.v b/theories/normedtype.v index de98e14929..6b43fe80a3 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -75,19 +75,23 @@ Require Import classical_sets posnum topology prodnormedzmodule. (* ereal_loc_seq x == sequence that converges to x in the set *) (* of extended real numbers. *) (* *) +(* --> 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. *) +(* *) (* * 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] *) +(* from extended real numbers to [-1; 1] *) +(* expand == function from real numbers to extended *) +(* real numbers that cancels contract in *) +(* [-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. *) (******************************************************************************) Set Implicit Arguments. @@ -1004,16 +1008,24 @@ Definition expand r : {ereal R} := Lemma expand1 x : 1 <= x -> expand x = +oo%E. Proof. by move=> x1; rewrite /expand x1. Qed. +Lemma expandN r : expand (- r) = (- expand r)%E. +Proof. +rewrite /expand; case: ifPn => [r1|]. + rewrite ifF; [by rewrite ifT // -ler_oppr|apply/negbTE]. + by rewrite -ltNge -(opprK r) -ltr_oppl (lt_le_trans _ r1) // -subr_gt0 opprK. +rewrite -ltNge => r1; case: ifPn; rewrite ler_oppl opprK; [by move=> ->|]. +by rewrite -ltNge leNgt => ->; rewrite leNgt -ltr_oppl r1 /= mulNr normrN. +Qed. + Lemma expandN1 x : x <= -1 -> expand x = -oo%E. Proof. -move=> x1; rewrite /expand x1 ifF //; apply/negP => /le_trans/(_ x1). -by apply/negP; rewrite -ltNge -subr_gt0 opprK. +by rewrite ler_oppr => /expand1/eqP; rewrite expandN eqe_oppLR => /eqP. Qed. Lemma expand0 : expand 0 = 0%:E. Proof. by rewrite /expand leNgt ltr01 /= oppr_ge0 leNgt ltr01 /= mul0r. Qed. -(* Cyril: TODO: add to ssrnum *) +(* TODO: added in mathcomp-1.11.0 ssrnum *) Lemma nlt_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false). Proof. move=> x1; split; last by rewrite lt_eqF // (le_lt_trans (ler_norm _) x1). @@ -1103,6 +1115,19 @@ Definition le_contractRL := monoRL_in Definition lt_contractRL := monoRL_in (onW_can_in predT expandK) (fun x _ => isT) (in2W lt_contract). +Lemma homo_le_expand : {homo expand : x y / (x <= y)%O}. +Proof. +move=> x y xy; have [x1|] := lerP `|x| 1. + rewrite le_expandLR //; have [y1|] := lerP `|y| 1; first by rewrite expandK. + case/ler_normlP : x1 => xN1 x1; rewrite ltr_normr => /orP[y1|]. + by rewrite expand1 //= ltW. + rewrite ltr_oppr => y1; move: xN1; rewrite ler_oppl => /(lt_le_trans y1). + by rewrite ltNge xy. +rewrite ltr_normr => /orP[|] x1; last first. + by rewrite expandN1 // ?lee_ninfty // ler_oppr ltW. +by rewrite expand1; [rewrite expand1 // (le_trans _ xy) // ltW | exact: ltW]. +Qed. + Lemma contract_eq0 x : (contract x == 0) = (x == 0%:E). Proof. by rewrite -(can_eq contractK) contract0. Qed. @@ -1153,8 +1178,7 @@ suff [y [ysupS ?]] : exists y, (y < ereal_sup S)%E /\ ub S y. 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. + by rewrite -(contractK y) homo_le_expand //; 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. @@ -1502,8 +1526,7 @@ rewrite predeq2E => x A; split. move: re'r'; rewrite ltxI => /andP[Hr'1 Hr'2]. by rewrite ltr_subl_addr subrK in Hr'2. rewrite ltr_subl_addr -lte_fin -(contractK (_ + r)%:E). - rewrite addrC -(contractK r'%:E) //. - by rewrite lt_expand ?inE ?contract_le1. + by rewrite addrC -(contractK r'%:E) // lt_expand ?inE ?contract_le1. * rewrite /ereal_ball [contract +oo]/=. rewrite ltxI => /andP[re'1 re'2]. have [cr0|cr0] := lerP 0 (contract r%:E). diff --git a/theories/sequences.v b/theories/sequences.v index 1ee2e6ba44..d0787a0463 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -67,11 +67,11 @@ Notation "R ^nat" := (sequence R) : type_scope. Notation "'nondecreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> (n <= m)%O}) (at level 10). -Notation "'nonincreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> n >= m}) +Notation "'nonincreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> (n >= m)%O}) (at level 10). -Notation "'increasing_seq' f" := ({mono f : n m / (n <= m)%nat >-> n <= m}) +Notation "'increasing_seq' f" := ({mono f : n m / (n <= m)%nat >-> (n <= m)%O}) (at level 10). -Notation "'decreasing_seq' f" := ({mono f : n m / (n <= m)%nat >-> n >= m}) +Notation "'decreasing_seq' f" := ({mono f : n m / (n <= m)%nat >-> (n >= m)%O}) (at level 10). (* TODO: the "strict" versions with mono instead of homo should also have notations*)