From 7da865547861fd6937802e1f6e99f3c6d7f4b7b6 Mon Sep 17 00:00:00 2001 From: zstone1 Date: Tue, 25 Jul 2023 23:49:49 -0400 Subject: [PATCH] extended distance (#986) * extended distance * adding docs * shorten computations, factor out lemmas --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 16 ++++ classical/boolp.v | 13 ++- theories/constructive_ereal.v | 24 +++++ theories/normedtype.v | 173 ++++++++++++++++++++++++++++++++++ theories/reals.v | 41 ++++++++ theories/topology.v | 3 + 6 files changed, 266 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8a0ca059d..455a55a98 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -63,6 +63,22 @@ - in `classical_sets.v`: + lemma `Zorn_bigcup` +- in file `boolp.v`, + + lemmas `notP`, `notE` + + new lemma `implyE`. +- in file `reals.v`: + + lemmas `sup_sumE`, `inf_sumE` +- in file `topology.v`: + + lemma `ball_symE` +- in file `normedtype.v`, + + new definition `edist`. + + new lemmas `edist_ge0`, `edist_lt_ball`, + `edist_fin`, `edist_pinftyP`, `edist_finP`, `edist_fin_open`, + `edist_fin_closed`, `edist_pinfty_open`, `edist_sym`, `edist_triangle`, + `edist_continuous`, `edist_closeP`, and `edist_refl`. +- in `constructive_ereal.v`: + + lemmas `lte_pmulr`, `lte_pmull`, `lte_nmulr`, `lte_nmull` + + lemmas `lte0n`, `lee0n`, `lte1n`, `lee1n` ### Changed diff --git a/classical/boolp.v b/classical/boolp.v index 4e6177046..ba8fab556 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -586,15 +586,20 @@ by rewrite 2!negb_and -3!asbool_neg => /or3_asboolP. by rewrite 3!asbool_neg -2!negb_and => /and3_asboolP. Qed. +Lemma notP (P : Prop) : ~ ~ P <-> P. +Proof. by split => [|p]; [exact: contrapT|exact]. Qed. + +Lemma notE (P : Prop) : (~ ~ P) = P. Proof. by rewrite propeqE notP. Qed. + Lemma not_orP (P Q : Prop) : ~ (P \/ Q) <-> ~ P /\ ~ Q. -Proof. -split; [apply: contra_notP => /not_andP|apply: contraPnot => AB; apply/not_andP]; - by rewrite 2!notK. -Qed. +Proof. by rewrite -(notP (_ /\ _)) not_andP 2!notE. Qed. Lemma not_implyE (P Q : Prop) : (~ (P -> Q)) = (P /\ ~ Q). Proof. by rewrite propeqE not_implyP. Qed. +Lemma implyE (P Q : Prop) : (P -> Q) = (~ P \/ Q). +Proof. by rewrite -[LHS]notE not_implyE propeqE not_andP notE. Qed. + Lemma orC (P Q : Prop) : (P \/ Q) = (Q \/ P). Proof. by rewrite propeqE; split=> [[]|[]]; [right|left|right|left]. Qed. diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 9bff25544..9c39fd60b 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -529,6 +529,18 @@ Proof. by rewrite lte_fin ltrN10. Qed. Lemma leeN10 : - 1%E <= 0 :> \bar R. Proof. by rewrite lee_fin lerN10. Qed. +Lemma lte0n n : (0 < n%:R%:E :> \bar R) = (0 < n)%N. +Proof. by rewrite lte_fin ltr0n. Qed. + +Lemma lee0n n : (0 <= n%:R%:E :> \bar R) = (0 <= n)%N. +Proof. by rewrite lee_fin ler0n. Qed. + +Lemma lte1n n : (1 < n%:R%:E :> \bar R) = (1 < n)%N. +Proof. by rewrite lte_fin ltr1n. Qed. + +Lemma lee1n n : (1 <= n%:R%:E :> \bar R) = (1 <= n)%N. +Proof. by rewrite lee_fin ler1n. Qed. + Lemma fine_ge0 x : 0 <= x -> (0 <= fine x)%R. Proof. by case: x. Qed. @@ -1790,6 +1802,18 @@ Qed. Lemma lte_nmul2r z : z \is a fin_num -> z < 0 -> {mono *%E^~ z : x y /~ x < y}. Proof. by move=> zfin z0 x y; rewrite -!(muleC z) lte_nmul2l. Qed. +Lemma lte_pmulr x y : y \is a fin_num -> 0 < y -> (y < y * x) = (1 < x). +Proof. by move=> yfin y0; rewrite -[X in X < _ = _]mule1 lte_pmul2l. Qed. + +Lemma lte_pmull x y : y \is a fin_num -> 0 < y -> (y < x * y) = (1 < x). +Proof. by move=> yfin y0; rewrite muleC lte_pmulr. Qed. + +Lemma lte_nmulr x y : y \is a fin_num -> y < 0 -> (y < y * x) = (x < 1). +Proof. by move=> yfin y0; rewrite -[X in X < _ = _]mule1 lte_nmul2l. Qed. + +Lemma lte_nmull x y : y \is a fin_num -> y < 0 -> (y < x * y) = (x < 1). +Proof. by move=> yfin y0; rewrite muleC lte_nmulr. Qed. + Lemma lee_sum I (f g : I -> \bar R) s (P : pred I) : (forall i, P i -> f i <= g i) -> \sum_(i <- s | P i) f i <= \sum_(i <- s | P i) g i. diff --git a/theories/normedtype.v b/theories/normedtype.v index c26abcb60..55a5cb339 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -36,6 +36,8 @@ Require Import ereal reals signed topology prodnormedzmodule. (* structure on T. *) (* `|x| == the norm of x (notation from ssrnum). *) (* ball_norm == balls defined by the norm. *) +(* edist == the extended distance function for a *) +(* pseudometric X, from X*X -> \bar R *) (* nbhs_norm == neighborhoods defined by the norm. *) (* closed_ball == closure of a ball. *) (* f @`[ a , b ], f @`] a , b [ == notations for images of intervals, *) @@ -3593,6 +3595,177 @@ Notation ereal_is_cvgMr := is_cvgeMr. note="renamed to cvgeM, and generalized to a realFieldType")] Notation ereal_cvgM := cvgeM. +Section pseudoMetricDist. +Context {R : realType} {X : pseudoMetricType R}. +Implicit Types r : R. + +Definition edist (xy : X * X) : \bar R := + ereal_inf (EFin @` [set r | 0 < r /\ ball xy.1 r xy.2]). + +Lemma edist_ge0 (xy : X * X) : (0 <= edist xy)%E. +Proof. +by apply: lb_ereal_inf => z [+ []] => _/posnumP[r] _ <-; rewrite lee_fin. +Qed. +Hint Resolve edist_ge0 : core. + +Lemma edist_lt_ball r (xy : X * X) : (edist xy < r%:E)%E -> ball xy.1 r xy.2. +Proof. +case/ereal_inf_lt => ? [+ []] => _/posnumP[eps] bxye <-; rewrite lte_fin. +by move/ltW/le_ball; exact. +Qed. + +Lemma edist_fin r (xy : X * X) : + 0 < r -> ball xy.1 r xy.2 -> (edist xy <= r%:E)%E. +Proof. +move: r => _/posnumP[r] => ?; rewrite -(ereal_inf1 r%:num%:E) le_ereal_inf //. +by move=> ? -> /=; exists r%:num; split. +Qed. + +Lemma edist_pinftyP (xy : X * X) : + (edist xy = +oo)%E <-> (forall r, 0 < r -> ~ ball xy.1 r xy.2). +Proof. +split. + move/ereal_inf_pinfty => xrb r rpos rb; move: (ltry r); rewrite ltey => /eqP. + by apply; apply: xrb; exists r. +rewrite /edist=> nrb; suff -> : [set r | 0 < r /\ ball xy.1 r xy.2] = set0. + by rewrite image_set0 ereal_inf0. +by rewrite -subset0 => r [?] rb; apply: nrb; last exact: rb. +Qed. + +Lemma edist_finP (xy : X * X) : + (edist xy \is a fin_num)%E <-> exists2 r, 0 < r & ball xy.1 r xy.2. +Proof. +rewrite ge0_fin_numE ?edist_ge0// ltey. +rewrite -(rwP (negPP eqP)); apply/iff_not2; rewrite notE. +apply: (iff_trans (edist_pinftyP _)); apply: (iff_trans _ (forall2NP _ _)). +by under eq_forall => ? do rewrite implyE. +Qed. + +Lemma edist_fin_open : open [set xy : X * X | edist xy \is a fin_num]. +Proof. +move=> z /= /edist_finP [] _/posnumP[r] bzr. +exists (ball z.1 r%:num, ball z.2 r%:num); first by split; exact: nbhsx_ballx. +case=> a b [bza bzb]; apply/edist_finP; exists (r%:num + r%:num + r%:num) => //. +exact/(ball_triangle _ bzb)/(ball_triangle _ bzr)/ball_sym. +Qed. + +Lemma edist_fin_closed : closed [set xy : X * X | edist xy \is a fin_num]. +Proof. +move=> z /= /(_ (ball z 1)) []; first exact: nbhsx_ballx. +move=> w [/edist_finP [] _/posnumP[r] babr [bz1w1 bz2w2]]; apply/edist_finP. +exists (1 + (r%:num + 1)) => //. +exact/(ball_triangle bz1w1)/(ball_triangle babr)/ball_sym. +Qed. + +Lemma edist_pinfty_open : open [set xy : X * X | edist xy = +oo]%E. +Proof. +rewrite -closedC; have := edist_fin_closed; congr (_ _). +by rewrite eqEsubset; split => z; rewrite /= ?ge0_fin_numE // ltey; move/eqP. +Qed. + +Lemma edist_sym (x y : X) : edist (x, y) = edist (y, x). +Proof. by rewrite /edist /=; under eq_fun do rewrite ball_symE. Qed. + +Lemma edist_triangle (x y z : X) : + (edist (x, z) <= edist (x, y) + edist (y, z))%E. +Proof. +have [|] := eqVneq (edist (x, z)) +oo%E. + have [-> ->|] := eqVneq (edist (x, y)) +oo%E. + by rewrite addye ?lexx// -lteNye (lt_le_trans _ (edist_ge0 _)). + have [-> ? ->|] := eqVneq (edist (y, z)) +oo%E. + by rewrite addey ?lexx// -lteNye (lt_le_trans _ (edist_ge0 _)). + rewrite -?ltey -?ge0_fin_numE//. + move=> /edist_finP [_/posnumP[r2] /= yz] /edist_finP [_/posnumP[r1] /= xy]. + move/edist_pinftyP /(_ (r1%:num + r2%:num) _) => -[//|]. + exact: (ball_triangle xy). +rewrite -ltey -ge0_fin_numE// => /[dup] xzfin. +move/edist_finP => [_/posnumP[del] /= xz]. +have [->|] := eqVneq (edist (x, y)) +oo%E. + by rewrite addye ?leey// -lteNye (lt_le_trans _ (edist_ge0 _)). +have [->|] := eqVneq (edist (y, z)) +oo%E. + by rewrite addey ?leey// -lteNye (lt_le_trans _ (edist_ge0 _)). +rewrite -?ltey -?ge0_fin_numE //. +move=> /edist_finP [_/posnumP[r2] /= yz] /edist_finP [_/posnumP[r1] /= xy]. +rewrite /edist /= ?ereal_inf_EFin; first last. +- by exists (r1%:num + r2%:num); split => //; apply: (ball_triangle xy). +- by exists 0 => ? /= [/ltW]. +- by exists r1%:num; split. +- by exists 0 => ? /= [/ltW]. +- by exists r2%:num; split. +- by exists 0 => ? /= [/ltW]. +rewrite -EFinD lee_fin -inf_sumE //; first last. +- by split; [exists r2%:num; split| exists 0 => ? /= [/ltW]]. +- by split; [exists r1%:num; split| exists 0 => ? /= [/ltW]]. +apply: lb_le_inf. + by exists (r1%:num + r2%:num); exists r1%:num => //; exists r2%:num. +move=> ? [+ []] => _/posnumP[p] xpy [+ []] => _/posnumP[q] yqz <-. +apply: inf_lb; first by exists 0 => ? /= [/ltW]. +by split => //; apply: (ball_triangle xpy). +Qed. + +Lemma edist_continuous : continuous edist. +Proof. +case=> x y; have [pE U /= Upinf|] := eqVneq (edist (x, y)) +oo%E. + rewrite nbhs_simpl /=; apply (@filterS _ _ _ [set xy | edist xy = +oo]%E). + by move=> z /= ->; apply: nbhs_singleton; move: pE Upinf => ->. + by apply: open_nbhs_nbhs; split => //; exact: edist_pinfty_open. +rewrite -ltey -ge0_fin_numE// => efin. +rewrite -[edist (x, y)]fineK//; apply: cvg_EFin. + by have := edist_fin_open efin; apply: filter_app; near=> w. +move=> U /=; rewrite nbhs_simpl/= -nbhs_ballE. +move=> [] _/posnumP[r] distrU; rewrite nbhs_simpl /=. +have r2p : 0 < r%:num / 4 by rewrite divr_gt0// ltr0n. +exists (ball x (r%:num / 4), ball y (r%:num / 4)). + by split => //=; rewrite nbhs_ballE; + exact: (@nbhsx_ballx _ _ _ (@PosNum _ _ r2p)). +case => a b /= [/ball_sym xar yar]; apply: distrU => /=. +have abxy : (edist (a, b) <= edist (a, x) + edist (x, y) + edist (y, b))%E. + by rewrite -addeA (le_trans (@edist_triangle _ x _)) ?lee_add ?edist_triangle. +have abfin : edist (a, b) \is a fin_num. + rewrite ge0_fin_numE// (le_lt_trans abxy)//. + by apply: lte_add_pinfty; [apply: lte_add_pinfty|]; + rewrite -ge0_fin_numE //; apply/edist_finP; exists (r%:num / 4). +have xyabfin : `|edist (x, y) - edist (a, b)|%E \is a fin_num. + by rewrite abse_fin_num fin_numB abfin efin. +have daxr : edist (a, x) \is a fin_num by apply/edist_finP; exists (r%:num / 4). +have dybr : edist (y, b) \is a fin_num by apply/edist_finP; exists (r%:num / 4). +rewrite -fineB// -fine_abse ?fin_numB ?abfin ?efin//. +rewrite (@le_lt_trans _ _ (fine (edist (a, x) + edist (y, b))))//. + rewrite fine_le// ?fin_numD ?daxr ?dybr//. + have [xyab|xyab] := leP (edist (a, b)) (edist (x, y)). + rewrite gee0_abs ?subre_ge0// lee_subl_addr//. + rewrite (le_trans (@edist_triangle _ a _))// (edist_sym a x) -addeA. + by rewrite lee_add// addeC (edist_sym y) edist_triangle. + rewrite lte0_abs ?subre_lt0// oppeB ?fin_num_adde_defr// addeC. + by rewrite lee_subl_addr// addeAC. +rewrite fineD // [_%:num]splitr. +have r42 : r%:num / 4 < r%:num / 2. + by rewrite ltr_pmul2l// ltf_pinv ?posrE ?ltr0n// ltr_nat. +by apply: ltr_add; rewrite (le_lt_trans _ r42)// -lee_fin fineK // edist_fin. +Unshelve. end_near. Qed. + +Lemma edist_closeP x y : close x y <-> edist (x, y) = 0%E. +Proof. +rewrite ball_close; split; first last. + by move=> edist0 eps; apply: (@edist_lt_ball _ (x, y)); rewrite edist0. +move=> bxy; apply: le_anti; rewrite edist_ge0 andbT leNgt; apply/negP => dpos. +have xxfin : edist (x, y) \is a fin_num. + by rewrite ge0_fin_numE// (@le_lt_trans _ _ 1%:E) ?ltey// edist_fin. +move: (dpos); rewrite -[edist _]fineK // lte_fin => dpose. +pose eps := PosNum dpose. +have : (edist (x, y) <= (eps%:num / 2)%:E)%E. + apply: ereal_inf_lb; exists (eps%:num / 2) => //; split => //. + exact: (bxy (@PosNum R (eps%:num / 2) ltac:(done))). +rewrite leNgt; move/negP; apply. +by rewrite /= EFinM fineK// lte_pdivr_mulr// lte_pmulr// lte1n. +Qed. + +Lemma edist_refl x : edist (x, x) = 0%E. Proof. exact/edist_closeP. Qed. + +End pseudoMetricDist. +#[global] +Hint Resolve edist_ge0 : core. + Section open_closed_sets_ereal. Variable R : realFieldType (* TODO: generalize to numFieldType? *). Local Open Scope ereal_scope. diff --git a/theories/reals.v b/theories/reals.v index 248f65307..62bd83734 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -444,6 +444,47 @@ Qed. End RealLemmas. +Section sup_sum. +Context {R : realType}. + +Lemma sup_sumE (A B : set R) : + has_sup A -> has_sup B -> sup [set x + y | x in A & y in B] = sup A + sup B. +Proof. +move=> /[dup] supA [[a Aa] ubA] /[dup] supB [[b Bb] ubB]. +have ABsup : has_sup [set x + y | x in A & y in B]. + split; first by exists (a + b), a => //; exists b. + case: ubA ubB => p up [q uq]; exists (p + q) => ? [r Ar [s Bs] <-]. + by apply: ler_add; [exact: up | exact: uq]. +apply: le_anti; apply/andP; split. + apply: sup_le_ub; first by case: ABsup. + by move=> ? [p Ap [q Bq] <-]; apply: ler_add; exact: sup_ub. +rewrite real_leNgt ?num_real// -subr_gt0; apply/negP. +set eps := (_ + _ - _) => epos. +have e2pos : 0 < eps / 2 by rewrite divr_gt0// ltr0n. +have [r Ar supBr] := sup_adherent e2pos supA. +have [s Bs supAs] := sup_adherent e2pos supB. +have := ltr_add supBr supAs. +rewrite -addrA [-_+_]addrC -addrA -opprD -splitr addrA /= opprD opprK addrA. +rewrite subrr add0r; apply/negP; rewrite -real_leNgt ?num_real//. +by apply: sup_upper_bound => //; exists r => //; exists s. +Qed. + +Lemma inf_sumE (A B : set R) : + has_inf A -> has_inf B -> inf [set x + y | x in A & y in B] = inf A + inf B. +Proof. +move/has_inf_supN => ? /has_inf_supN ?; rewrite /inf. +rewrite [X in - sup X = _](_ : _ = + [set x + y | x in [set - x | x in A ] & y in [set - x | x in B]]). + rewrite eqEsubset; split => /= t [] /= x []a Aa. + case => b Bb <- <-; exists (- a); first by exists a. + by exists (- b); [exists b|rewrite opprD]. + move=> <- [y] [b Bb] <- <-; exists (a + b); last by rewrite opprD. + by exists a => //; exists b. +by rewrite sup_sumE // -opprD. +Qed. + +End sup_sum. + (* -------------------------------------------------------------------- *) Section InfTheory. diff --git a/theories/topology.v b/theories/topology.v index 29d6f29f8..0d7d90f8d 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -5001,6 +5001,9 @@ Proof. by move=> e_gt0; apply: ball_center (PosNum e_gt0). Qed. Lemma ball_sym (x y : M) (e : R) : ball x e y -> ball y e x. Proof. exact: PseudoMetric.ball_sym. Qed. +Lemma ball_symE (x y : M) (e : R) : ball x e y = ball y e x. +Proof. by rewrite propeqE; split; exact/ball_sym. Qed. + Lemma ball_triangle (y x z : M) (e1 e2 : R) : ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z. Proof. exact: PseudoMetric.ball_triangle. Qed.