From 98b7b35a4b7eb42ca0c275b1144c9c27b83095be Mon Sep 17 00:00:00 2001 From: Holger Thies Date: Tue, 12 May 2026 11:03:58 +0900 Subject: [PATCH 1/3] added a few lemmas about sup --- CHANGELOG_UNRELEASED.md | 3 ++ reals/reals.v | 71 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 74 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c934f4375f..0e61ee4fbc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -93,6 +93,9 @@ + lemma `is_diff_mx` + instance `is_diff_mx` +- in `reals.v`: + + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn` + ### Changed - moved from `measurable_structure.v` to `classical_sets.v`: diff --git a/reals/reals.v b/reals/reals.v index 67f0fd21fc..5971918ea0 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -632,7 +632,78 @@ move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrC subrK => ltFxl. by exists x => //; rewrite (ge_inf hs.2)//; exists x. Qed. + +Lemma sup_ge0 (A : set R) : (forall x, A x -> 0 <= x) -> 0 <= sup A. +Proof. +move=> Ax. +have [->|/set0P[a Aa]] := eqVneq A set0; first by rewrite sup0. +have [[A0 Aub]|supA] := pselect (has_sup A). + by rewrite (le_trans (Ax _ Aa))// ub_le_sup. +by rewrite sup_out. +Qed. + +Lemma has_sup_wpZl (A : set R) (a : R) : 0 <= a -> has_sup A -> has_sup [set a * x | x in A ]. +Proof. +move => a0 [[x Ax] [b ub]]. +split;first by exists (a*x); exists x. +exists (a * b) => _ [y Ay <-]. +by rewrite ler_wpM2l //; apply ub. +Qed. + +Lemma gt0_has_supZl (A : set R) (a : R) : 0 < a -> has_sup [set a * x | x in A ] -> has_sup A. +Proof. +move => a0 [[_ [x Ax _]] [b ub]]. +split;first by exists x. +exists (b/a). +move => y Ay. +rewrite ler_pdivlMr // mulrC. +by apply ub;exists y. +Qed. +Lemma ge0_supZl (A : set R) (a : R) : + 0 <= a -> sup [set a * x | x in A ] = a * sup A . +Proof. +move =>a0. +have [->|an0] := eqVneq a 0. + have [->| /negPf Anonempty] := eqVneq A set0; first by rewrite image_set0 sup0 mulr0. + suff -> : [set 0*x | x in A] = [set 0] by rewrite sup1 mul0r. + under eq_fun do rewrite mul0r. + by rewrite set_cst Anonempty. +have [->|/set0P Anonempty] := eqVneq A set0; first by rewrite image_set0 sup0 mulr0. +have [ex_sup | not_ex_sup] := pselect (has_sup A); last by rewrite !sup_out ?mulr0 // => -h;apply not_ex_sup; apply: gt0_has_supZl h;rewrite lt0r an0. +have [[x Ax] ub] := ex_sup. +apply /eqP;rewrite eq_le;apply /andP;split. + apply ge_sup; first by exists (a * x), x. + move => _ [x0 Axo <-]. + by rewrite ler_wpM2l// ub_le_sup. +rewrite -ler_pdivlMl; last by rewrite lt0r an0. +apply ge_sup; first by apply ex_sup. +move => x0 Ax0. +rewrite ler_pdivlMl; last by rewrite lt0r an0. +rewrite ub_le_sup //; last by exists x0. +have [x1 ubx1] := ub. +exists (a * x1) => _ [x2 Ax2 <-]. +by rewrite ler_wpM2l// ubx1. +Qed. + +Lemma has_sup_Mn (A : set R) n : + has_sup A -> has_sup [set x *+n | x in A ]. +Proof. +move => [-[] x Ax [y uby]]. +split; first by exists (x *+ n), x. +exists (y *+ n). +move => _ [y0 Ay0 <-] . +by rewrite lerMn2r uby// orbT. +Qed. + +Lemma sup_Mn (A : set R) n : + sup [set x *+n | x in A ] = sup A *+ n. +Proof. +rewrite -mulr_natl [X in sup X = _](_ : _ = [set n%:R * x | x in A]); first exact: ge0_supZl. +by under eq_fun do rewrite -mulr_natl. +Qed. + End Sup. + #[deprecated(since="mathcomp-analysis 1.14.0", note="Renamed `inf_le`.")] Notation le_inf := inf_le (only parsing). #[deprecated(since="mathcomp-analysis 1.14.0", note="Renamed `sup_le`.")] From d65157774ac97abd47adbaf4d01f0c692a4d42e9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 19 May 2026 18:52:08 +0900 Subject: [PATCH 2/3] linting --- reals/reals.v | 102 ++++++++++++++++++++++---------------------------- 1 file changed, 44 insertions(+), 58 deletions(-) diff --git a/reals/reals.v b/reals/reals.v index 5971918ea0..3a0bd97c69 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -632,73 +632,59 @@ move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrC subrK => ltFxl. by exists x => //; rewrite (ge_inf hs.2)//; exists x. Qed. - -Lemma sup_ge0 (A : set R) : (forall x, A x -> 0 <= x) -> 0 <= sup A. +(** This is a specialization of the lemma `ub_le_sup` exploiting the fact + that `sup` is 0 when there is no supremum. *) +Lemma sup_ge0 A : (forall x, A x -> 0 <= x) -> 0 <= sup A. Proof. -move=> Ax. -have [->|/set0P[a Aa]] := eqVneq A set0; first by rewrite sup0. -have [[A0 Aub]|supA] := pselect (has_sup A). - by rewrite (le_trans (Ax _ Aa))// ub_le_sup. -by rewrite sup_out. +move=> A0; have [->|/set0P[a Aa]] := eqVneq A set0; first by rewrite sup0. +have [[_ Aub]|supA] := pselect (has_sup A); last by rewrite sup_out. +by rewrite (le_trans (A0 _ Aa))// ub_le_sup. Qed. -Lemma has_sup_wpZl (A : set R) (a : R) : 0 <= a -> has_sup A -> has_sup [set a * x | x in A ]. -Proof. -move => a0 [[x Ax] [b ub]]. -split;first by exists (a*x); exists x. -exists (a * b) => _ [y Ay <-]. -by rewrite ler_wpM2l //; apply ub. +Lemma has_sup_wpZl A (a : R) : 0 <= a -> has_sup A -> + has_sup [set a * x | x in A ]. +Proof. +move=> a0 [[x Ax] [b ub]]; split; first by exists (a * x), x. +by exists (a * b) => _ [y Ay <-]; rewrite ler_wpM2l// ub. Qed. -Lemma gt0_has_supZl (A : set R) (a : R) : 0 < a -> has_sup [set a * x | x in A ] -> has_sup A. +Lemma gt0_has_supZl A (a : R) : 0 < a -> has_sup [set a * x | x in A ] -> + has_sup A. Proof. -move => a0 [[_ [x Ax _]] [b ub]]. -split;first by exists x. -exists (b/a). -move => y Ay. -rewrite ler_pdivlMr // mulrC. -by apply ub;exists y. +move=> a0 [[_ [x Ax _]] [b ub]]; split; first by exists x. +by exists (b / a) => y Ay; rewrite ler_pdivlMr// mulrC ub//; exists y. Qed. -Lemma ge0_supZl (A : set R) (a : R) : - 0 <= a -> sup [set a * x | x in A ] = a * sup A . + +Lemma ge0_supZl A (a : R) : 0 <= a -> sup [set a * x | x in A ] = a * sup A. Proof. -move =>a0. -have [->|an0] := eqVneq a 0. - have [->| /negPf Anonempty] := eqVneq A set0; first by rewrite image_set0 sup0 mulr0. - suff -> : [set 0*x | x in A] = [set 0] by rewrite sup1 mul0r. +rewrite le_eqVlt => /predU1P[<-|an0]. + have [->|A0] := eqVneq A set0; first by rewrite image_set0 sup0 mulr0. + suff -> : [set 0 * x | x in A] = [set 0] by rewrite sup1 mul0r. under eq_fun do rewrite mul0r. - by rewrite set_cst Anonempty. -have [->|/set0P Anonempty] := eqVneq A set0; first by rewrite image_set0 sup0 mulr0. -have [ex_sup | not_ex_sup] := pselect (has_sup A); last by rewrite !sup_out ?mulr0 // => -h;apply not_ex_sup; apply: gt0_has_supZl h;rewrite lt0r an0. -have [[x Ax] ub] := ex_sup. -apply /eqP;rewrite eq_le;apply /andP;split. - apply ge_sup; first by exists (a * x), x. - move => _ [x0 Axo <-]. - by rewrite ler_wpM2l// ub_le_sup. -rewrite -ler_pdivlMl; last by rewrite lt0r an0. -apply ge_sup; first by apply ex_sup. -move => x0 Ax0. -rewrite ler_pdivlMl; last by rewrite lt0r an0. -rewrite ub_le_sup //; last by exists x0. -have [x1 ubx1] := ub. -exists (a * x1) => _ [x2 Ax2 <-]. -by rewrite ler_wpM2l// ubx1. -Qed. - -Lemma has_sup_Mn (A : set R) n : - has_sup A -> has_sup [set x *+n | x in A ]. -Proof. -move => [-[] x Ax [y uby]]. -split; first by exists (x *+ n), x. -exists (y *+ n). -move => _ [y0 Ay0 <-] . -by rewrite lerMn2r uby// orbT. -Qed. - -Lemma sup_Mn (A : set R) n : - sup [set x *+n | x in A ] = sup A *+ n. -Proof. -rewrite -mulr_natl [X in sup X = _](_ : _ = [set n%:R * x | x in A]); first exact: ge0_supZl. + by rewrite set_cst (negbTE A0). +have [->|A0] := eqVneq A set0; first by rewrite image_set0 sup0 mulr0. +have [[[x Ax] ubA]|not_ex_sup] := pselect (has_sup A); last first. + rewrite !sup_out ?mulr0//. + by apply: contra_not not_ex_sup; exact: gt0_has_supZl. +apply/eqP; rewrite eq_le; apply/andP; split. + apply: ge_sup; first by exists (a * x), x. + by move=> _ [x0 Axo <-]; rewrite ler_pM2l// ub_le_sup. +rewrite -ler_pdivlMl// ge_sup//; first exact/set0P. +move=> x0 Ax0; rewrite ler_pdivlMl// ub_le_sup//; last by exists x0. +have [x1 ubx1] := ubA. +by exists (a * x1) => _ [x2 Ax2 <-]; rewrite ler_pM2l// ubx1. +Qed. + +Lemma has_sup_Mn A n : has_sup A -> has_sup [set x *+n | x in A]. +Proof. +move=> [[x Ax] [y Ay]]; split; first by exists (x *+ n), x. +by exists (y *+ n) => _ [y0 Ay0 <-]; rewrite lerMn2r Ay// orbT. +Qed. + +Lemma sup_Mn A n : sup [set x *+n | x in A ] = sup A *+ n. +Proof. +rewrite -mulr_natl (_ : [set _ | _ in _] = [set n%:R * x | x in A]). + exact: ge0_supZl. by under eq_fun do rewrite -mulr_natl. Qed. From f0e9b9152466ef96a8992e74af0b86e6f6e3afda Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 20 May 2026 09:27:52 +0900 Subject: [PATCH 3/3] fix --- reals/reals.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/reals/reals.v b/reals/reals.v index 3a0bd97c69..c05603f075 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -684,8 +684,8 @@ Qed. Lemma sup_Mn A n : sup [set x *+n | x in A ] = sup A *+ n. Proof. rewrite -mulr_natl (_ : [set _ | _ in _] = [set n%:R * x | x in A]). - exact: ge0_supZl. -by under eq_fun do rewrite -mulr_natl. + by under eq_fun do rewrite -mulr_natl. +exact: ge0_supZl. Qed. End Sup.