From 899c14175215cd7f0942eae93321c23ea0a92d7e Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 25 Jul 2024 12:11:03 +0900 Subject: [PATCH] missing lemmas about ereal (#1264) * missing lemmas about ereal * dual variants * renamings * minor generalization --------- Co-authored-by: Pierre Roux --- CHANGELOG_UNRELEASED.md | 42 ++++++++ theories/constructive_ereal.v | 189 ++++++++++++++++++++++++---------- theories/lebesgue_measure.v | 6 +- theories/realfun.v | 3 +- 4 files changed, 179 insertions(+), 61 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 197692e10..542d716f8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -39,6 +39,10 @@ - in `realfun.v`: + lemma `nondecreasing_at_left_is_cvgr` +- in `constructive_ereal.v`: + + lemmas `lteD2rE`, `leeD2rE` + + lemmas `lte_dD2rE`, `lee_dD2rE` + ### Changed - in `topology.v`: @@ -87,8 +91,43 @@ - in `measure.v`: + `setD_closed` -> `setSD_closed` +- in `constructive_ereal.v`: + + `lte_dadd` -> `lte_dD` + + `lee_daddl` -> `lee_dDl` + + `lee_daddr` -> `lee_dDr` + + `gee_daddl` -> `gee_dDl` + + `gee_daddr` -> `gee_dDr` + + `lte_daddl` -> `lte_dDl` + + `lte_daddr` -> `lte_dDr` + + `gte_dsubl` -> `gte_dBl` + + `gte_dsubr` -> `gte_dBr` + + `gte_daddl` -> `gte_dDl` + + `gte_daddr` -> `gte_dDr` + + `lee_dadd2lE` -> `lee_dD2lE` + + `lte_dadd2lE` -> `lte_dD2lE` + + `lee_dadd2rE` -> `lee_dD2rE` + + `lee_dadd2l` -> `lee_dD2l` + + `lee_dadd2r` -> `lee_dD2r` + + `lee_dadd` -> `lee_dD` + + `lee_dsub` -> `lee_dB` + + `lte_dsubl_addr` -> `lte_dBlDr` + + `lte_dsubl_addl` -> `lte_dBlDl` + + `lte_dsubr_addr` -> `lte_dBrDr` + + `lte_dsubr_addl` -> `lte_dBrDl` + + `gte_opp` -> `gteN` + + `gte_dopp` -> `gte_dN` + + `lte_le_add` -> `lte_leD` + + `lee_lt_add` -> `lee_ltD` + + `lte_le_dadd` -> `lte_le_dD` + + `lee_lt_dadd` -> `lee_lt_dD` + + `lte_le_sub` -> `lte_leB` + + `lte_le_dsub` -> `lte_le_dB` + ### Generalized +- in `constructive_ereal.v`: + + lemmas `leeN2`, `lteN2` generalized from `realDomainType` to `numDomainType` + ### Deprecated - in `reals.v`: @@ -96,6 +135,9 @@ + `le_floor` (use `Num.Theory.floor_le` instead) + `le_ceil` (use `ceil_ge` instead) +- in `constructive_ereal.v`: + + lemmas `lte_opp2`, `lee_opp2` (use `lteN2`, `leeN2` instead) + ### Removed - in `reals.v`: diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 831e91b69..b5a5822f6 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -620,6 +620,20 @@ Lemma mule2n x : x *+ 2 = x + x. Proof. by []. Qed. Lemma expe2 x : x ^+ 2 = x * x. Proof. by []. Qed. +Lemma leeN2 : {mono @oppe R : x y /~ x <= y}. +Proof. +move=> x y; case: x y => [?||] [?||] //; first by rewrite !lee_fin !lerN2. + by rewrite /Order.le/= realN. +by rewrite /Order.le/= realN. +Qed. + +Lemma lteN2 : {mono @oppe R : x y /~ x < y}. +Proof. +move=> x y; case: x y => [?||] [?||] //; first by rewrite !lte_fin !ltrN2. + by rewrite /Order.lt/= realN. +by rewrite /Order.lt/= realN. +Qed. + End ERealOrderTheory. #[global] Hint Resolve leeN10 lteN10 : core. @@ -1191,7 +1205,7 @@ Qed. Lemma mule_lt0_gt0 x y : x < 0 -> 0 < y -> x * y < 0. Proof. by move=> x0 y0; rewrite muleC mule_gt0_lt0. Qed. -Lemma gte_opp x : 0 < x -> - x < x. +Lemma gteN x : 0 < x -> - x < x. Proof. by case: x => //= r; rewrite !lte_fin; apply: gtrN. Qed. Lemma realMe x y : (0%E >=< x)%O -> (0%E >=< y)%O -> (0%E >=< x * y)%O. @@ -1244,6 +1258,9 @@ Notation mine := (@Order.min ereal_display _). Notation "@ 'mine' R" := (@Order.min ereal_display R) (at level 10, R at level 8, only parsing) : function_scope. +#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `gteN`")] +Notation gte_opp := gteN (only parsing). + Module DualAddTheoryNumDomain. Section DualERealArithTh_numDomainType. @@ -1459,7 +1476,7 @@ move=> u0 l; rewrite dual_sumeE oppe_le0 sume_ge0 // => t Pt. rewrite oppe_ge0; exact: u0. Qed. -Lemma gte_dopp (r : \bar^d R) : (0 < r)%E -> (- r < r)%E. +Lemma gte_dN (r : \bar^d R) : (0 < r)%E -> (- r < r)%E. Proof. by case: r => //= r; rewrite !lte_fin; apply: gtrN. Qed. Lemma ednatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar^d R. @@ -1490,6 +1507,9 @@ Qed. End DualERealArithTh_numDomainType. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dN`")] +Notation gte_dopp := gte_dN (only parsing). + End DualAddTheoryNumDomain. Section ERealArithTh_realDomainType. @@ -1727,8 +1747,6 @@ have := mule_eq_pinfty x (- y); rewrite muleN eqe_oppLR => ->. by rewrite !eqe_oppLR lteNr lteNl oppe0 (orbC _ ((x == -oo) && _)). Qed. -Lemma lteN2 x y : (- x < - y) = (y < x). Proof. by rewrite lteNl oppeK. Qed. - Lemma lteD a b x y : a < b -> x < y -> a + x < b + y. Proof. move: a b x y=> [a| |] [b| |] [x| |] [y| |]; rewrite ?(ltry,ltNyr)//. @@ -1783,6 +1801,9 @@ move: a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(ltry, ltNyr)//. by rewrite !lte_fin ltrD2l. Qed. +Lemma lteD2rE x a b : x \is a fin_num -> (a + x < b + x) = (a < b). +Proof. by rewrite -!(addeC x); exact: lteD2lE. Qed. + Lemma leeD2l x a b : a <= b -> x + a <= x + b. Proof. move: a b x => -[a [b [x /=|//|//] | []// |//] | []// | ]. @@ -1797,6 +1818,9 @@ move: a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(leey, leNye)//. by rewrite !lee_fin lerD2l. Qed. +Lemma leeD2rE x a b : x \is a fin_num -> (a + x <= b + x) = (a <= b). +Proof. by rewrite -!(addeC x); exact: leeD2lE. Qed. + Lemma leeD2r x a b : a <= b -> a + x <= b + x. Proof. rewrite addeC (addeC b); exact: leeD2l. Qed. @@ -1806,14 +1830,14 @@ move: a b x y => [a| |] [b| |] [x| |] [y| |]; rewrite ?(leey, leNye)//. by rewrite !lee_fin; exact: lerD. Qed. -Lemma lte_le_add a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y. +Lemma lte_leD a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y. Proof. move: x y a b => [x| |] [y| |] [a| |] [b| |] _ //=; rewrite ?(ltry, ltNyr)//. by rewrite !lte_fin; exact: ltr_leD. Qed. -Lemma lee_lt_add a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y. -Proof. by move=> afin xa yb; rewrite (addeC a) (addeC x) lte_le_add. Qed. +Lemma lee_ltD a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y. +Proof. by move=> afin xa yb; rewrite (addeC a) (addeC x) lte_leD. Qed. Lemma leeB x y z u : x <= y -> u <= z -> x - z <= y - u. Proof. @@ -1821,7 +1845,7 @@ move: x y z u => -[x| |] -[y| |] -[z| |] -[u| |] //=; rewrite ?(leey,leNye)//. by rewrite !lee_fin; exact: lerB. Qed. -Lemma lte_le_sub z u x y : u \is a fin_num -> +Lemma lte_leB z u x y : u \is a fin_num -> x < z -> u <= y -> x - y < z - u. Proof. move: z u x y => [z| |] [u| |] [x| |] [y| |] _ //=; rewrite ?(ltry, ltNyr)//. @@ -2309,8 +2333,6 @@ move=> *; apply: (can_inj oppeK); apply: eq_infty => r. by rewrite leeNr -EFinN. Qed. -Lemma leeN2 x y : (- x <= - y) = (y <= x). Proof. by rewrite leeNl oppeK. Qed. - Lemma lee_abs x : x <= `|x|. Proof. by move: x => [x| |]//=; rewrite lee_fin ler_norm. Qed. @@ -2688,6 +2710,16 @@ Notation lee_subl_addl := leeBlDl (only parsing). Notation lee_subr_addr := leeBrDr (only parsing). #[deprecated(since="mathcomp-analysis 1.2.0", note="Use leeBrDl instead.")] Notation lee_subr_addl := leeBrDl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lte_leD` instead.")] +Notation lte_le_add := lte_leD (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lee_ltD` instead.")] +Notation lee_lt_add := lee_ltD (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lte_leB` instead.")] +Notation lte_le_sub := lte_leB (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="Use leeN2 instead.")] +Notation lee_opp2 := leeN2 (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="Use lteN2 instead.")] +Notation lte_opp2 := lteN2 (only parsing). Module DualAddTheoryRealDomain. @@ -2720,67 +2752,79 @@ Lemma dsube_le0 x y : (x \is a fin_num) || (y \is a fin_num) -> (y - x <= 0) = (y <= x). Proof. by move=> /orP[?|?]; [rewrite dsuber_le0|rewrite dsubre_le0]. Qed. -Lemma lte_dadd a b x y : a < b -> x < y -> a + x < b + y. +Lemma lte_dD a b x y : a < b -> x < y -> a + x < b + y. Proof. rewrite !dual_addeE lteN2 -lteN2 -(lteN2 y); exact: lteD. Qed. -Lemma lee_daddl x y : 0 <= y -> x <= x + y. +Lemma lee_dDl x y : 0 <= y -> x <= x + y. Proof. rewrite dual_addeE leeNr -oppe_le0; exact: geeDl. Qed. -Lemma lee_daddr x y : 0 <= y -> x <= y + x. +Lemma lee_dDr x y : 0 <= y -> x <= y + x. Proof. rewrite dual_addeE leeNr -oppe_le0; exact: geeDr. Qed. -Lemma gee_daddl x y : y <= 0 -> x + y <= x. +Lemma gee_dDl x y : y <= 0 -> x + y <= x. Proof. rewrite dual_addeE leeNl -oppe_ge0; exact: leeDl. Qed. -Lemma gee_daddr x y : y <= 0 -> y + x <= x. +Lemma gee_dDr x y : y <= 0 -> y + x <= x. Proof. rewrite dual_addeE leeNl -oppe_ge0; exact: leeDr. Qed. -Lemma lte_daddl y x : y \is a fin_num -> (y < y + x) = (0 < x). +Lemma lte_dDl y x : y \is a fin_num -> (y < y + x) = (0 < x). Proof. by rewrite -fin_numN dual_addeE lteNr; exact: gte_subl. Qed. -Lemma lte_daddr y x : y \is a fin_num -> (y < x + y) = (0 < x). +Lemma lte_dDr y x : y \is a fin_num -> (y < x + y) = (0 < x). Proof. by rewrite -fin_numN dual_addeE lteNr addeC; exact: gte_subl. Qed. -Lemma gte_dsubl y x : y \is a fin_num -> (y - x < y) = (0 < x). +Lemma gte_dBl y x : y \is a fin_num -> (y - x < y) = (0 < x). Proof. by rewrite -fin_numN dual_addeE lteNl oppeK; exact: lteDl. Qed. -Lemma gte_dsubr y x : y \is a fin_num -> (- x + y < y) = (0 < x). +Lemma gte_dBr y x : y \is a fin_num -> (- x + y < y) = (0 < x). Proof. by rewrite -fin_numN dual_addeE lteNl oppeK; exact: lteDr. Qed. -Lemma gte_daddl x y : x \is a fin_num -> (x + y < x) = (y < 0). +Lemma gte_dDl x y : x \is a fin_num -> (x + y < x) = (y < 0). Proof. by rewrite -fin_numN dual_addeE lteNl -[0]oppe0 lteNr; exact: lteDl. Qed. -Lemma gte_daddr x y : x \is a fin_num -> (y + x < x) = (y < 0). -Proof. by rewrite daddeC; exact: gte_daddl. Qed. +Lemma gte_dDr x y : x \is a fin_num -> (y + x < x) = (y < 0). +Proof. by rewrite daddeC; exact: gte_dDl. Qed. -Lemma lte_dadd2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b). +Lemma lte_dD2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b). Proof. by move=> ?; rewrite !dual_addeE lteN2 lteD2lE ?fin_numN// lteN2. Qed. -Lemma lee_dadd2l x a b : a <= b -> x + a <= x + b. +Lemma lte_dD2rE x a b : x \is a fin_num -> (a + x < b + x) = (a < b). +Proof. +move=> ?; rewrite !dual_addeE lteN2 -[RHS]lteN2. +by rewrite -[RHS](@lteD2rE _ (- x))// fin_numN. +Qed. + +Lemma lee_dD2rE x a b : x \is a fin_num -> (a + x <= b + x) = (a <= b). +Proof. +move=> ?; rewrite !dual_addeE leeN2 -[RHS]leeN2. +by rewrite -[RHS](@leeD2rE _ (- x))// fin_numN. +Qed. + +Lemma lee_dD2l x a b : a <= b -> x + a <= x + b. Proof. rewrite !dual_addeE leeN2 -leeN2; exact: leeD2l. Qed. -Lemma lee_dadd2lE x a b : x \is a fin_num -> (x + a <= x + b) = (a <= b). +Lemma lee_dD2lE x a b : x \is a fin_num -> (x + a <= x + b) = (a <= b). Proof. by move=> ?; rewrite !dual_addeE leeN2 leeD2lE ?fin_numN// leeN2. Qed. -Lemma lee_dadd2r x a b : a <= b -> a + x <= b + x. +Lemma lee_dD2r x a b : a <= b -> a + x <= b + x. Proof. rewrite !dual_addeE leeN2 -leeN2; exact: leeD2r. Qed. -Lemma lee_dadd a b x y : a <= b -> x <= y -> a + x <= b + y. +Lemma lee_dD a b x y : a <= b -> x <= y -> a + x <= b + y. Proof. rewrite !dual_addeE leeN2 -leeN2 -(leeN2 y); exact: leeD. Qed. -Lemma lte_le_dadd a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y. -Proof. rewrite !dual_addeE lteN2 -lteN2; exact: lte_le_sub. Qed. +Lemma lte_le_dD a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y. +Proof. by rewrite !dual_addeE lteN2 -lteN2; exact: lte_leB. Qed. -Lemma lee_lt_dadd a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y. -Proof. by move=> afin xa yb; rewrite (daddeC a) (daddeC x) lte_le_dadd. Qed. +Lemma lee_lt_dD a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y. +Proof. by move=> afin xa yb; rewrite (daddeC a) (daddeC x) lte_le_dD. Qed. -Lemma lee_dsub x y z t : x <= y -> t <= z -> x - z <= y - t. +Lemma lee_dB x y z t : x <= y -> t <= z -> x - z <= y - t. Proof. rewrite !dual_addeE leeNl oppeK -leeN2 !oppeK; exact: leeD. Qed. -Lemma lte_le_dsub z u x y : u \is a fin_num -> x < z -> u <= y -> x - y < z - u. -Proof. by rewrite !dual_addeE lteN2 !oppeK -lteN2; exact: lte_le_add. Qed. +Lemma lte_le_dB z u x y : u \is a fin_num -> x < z -> u <= y -> x - y < z - u. +Proof. by rewrite !dual_addeE lteN2 !oppeK -lteN2; exact: lte_leD. Qed. Lemma lee_dsum I (f g : I -> \bar^d R) s (P : pred I) : (forall i, P i -> f i <= g i) -> @@ -2890,16 +2934,16 @@ move=> AB f0; rewrite !dual_sumeE leeN2. apply: lee_sum_nneg_subfset => [//|? ? ?]; rewrite oppe_ge0; exact: f0. Qed. -Lemma lte_dsubl_addr x y z : y \is a fin_num -> (x - y < z) = (x < z + y). +Lemma lte_dBlDr x y z : y \is a fin_num -> (x - y < z) = (x < z + y). Proof. by move=> ?; rewrite !dual_addeE lteNl lteNr oppeK lteBlDr. Qed. -Lemma lte_dsubl_addl x y z : y \is a fin_num -> (x - y < z) = (x < y + z). +Lemma lte_dBlDl x y z : y \is a fin_num -> (x - y < z) = (x < y + z). Proof. by move=> ?; rewrite !dual_addeE lteNl lteNr lteBrDl ?fin_numN. Qed. -Lemma lte_dsubr_addr x y z : z \is a fin_num -> (x < y - z) = (x + z < y). +Lemma lte_dBrDr x y z : z \is a fin_num -> (x < y - z) = (x + z < y). Proof. by move=> ?; rewrite !dual_addeE lteNl lteNr lteBlDr ?fin_numN. Qed. -Lemma lte_dsubr_addl x y z : z \is a fin_num -> (x < y - z) = (z + x < y). +Lemma lte_dBrDl x y z : z \is a fin_num -> (x < y - z) = (z + x < y). Proof. by move=> ?; rewrite !dual_addeE lteNl lteNr lteBlDl ?fin_numN. Qed. Lemma lte_dsuber_addr x y z : y \is a fin_num -> (x < y - z) = (x + z < y). @@ -2955,7 +2999,7 @@ by move=> ?; rewrite !dual_addeE leeNl leeNr lee_subel_addl ?fin_numN. Qed. Lemma dsuber_gt0 x y : x \is a fin_num -> (0 < y - x) = (x < y). -Proof. by move=> ?; rewrite lte_dsubr_addl// dadde0. Qed. +Proof. by move=> ?; rewrite lte_dBrDl// dadde0. Qed. Lemma dsubre_gt0 x y : y \is a fin_num -> (0 < y - x) = (x < y). Proof. by move=> ?; rewrite lte_dsuber_addl// dadde0. Qed. @@ -3029,7 +3073,7 @@ Lemma lee_abs_dsum (I : Type) (s : seq I) (F : I -> \bar^d R) (P : pred I) : `|\sum_(i <- s | P i) F i| <= \sum_(i <- s | P i) `|F i|. Proof. elim/big_ind2 : _ => //; first by rewrite abse0. -by move=> *; exact/(le_trans (lee_abs_dadd _ _) (lee_dadd _ _)). +by move=> *; exact/(le_trans (lee_abs_dadd _ _) (lee_dD _ _)). Qed. Lemma lee_abs_dsub x y : `|x - y| <= `|x| + `|y|. @@ -3047,7 +3091,7 @@ Lemma dmule_natl x n : n%:R%:E * x = x *+ n. Proof. by rewrite mule_natl ednatmulE. Qed. Lemma lee_pdaddl y x z : 0 <= x -> y <= z -> y <= x + z. -Proof. by move=> *; rewrite -[y]dadd0e lee_dadd. Qed. +Proof. by move=> *; rewrite -[y]dadd0e lee_dD. Qed. Lemma lte_pdaddl y x z : 0 <= x -> y < z -> y < x + z. Proof. by move=> x0 /lt_le_trans; apply; rewrite lee_pdaddl. Qed. @@ -3078,21 +3122,56 @@ Arguments lee_dsum_npos_natr {R}. Arguments lee_dsum_nneg_natl {R}. Arguments lee_dsum_npos_natl {R}. -End DualAddTheoryRealDomain. - -Lemma lee_opp2 {R : numDomainType} : {mono @oppe R : x y /~ x <= y}. -Proof. -move=> x y; case: x y => [?||] [?||] //; first by rewrite !lee_fin !lerN2. - by rewrite /Order.le/= realN. -by rewrite /Order.le/= realN. -Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dD`")] +Notation lte_dadd := lte_dD (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dDl`")] +Notation lee_daddl := lee_dDl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dDr`")] +Notation lee_daddr := lee_dDr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gee_dDl`")] +Notation gee_daddl := gee_dDl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gee_dDr`")] +Notation gee_daddr := gee_dDr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dDl`")] +Notation lte_daddl := lte_dDl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dDr`")] +Notation lte_daddr := lte_dDr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dBl`")] +Notation gte_dsubl := gte_dBl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dBr`")] +Notation gte_dsubr := gte_dBr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dDl`")] +Notation gte_daddl := gte_dDl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dDr`")] +Notation gte_daddr := gte_dDr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dD2lE`")] +Notation lte_dadd2lE := lte_dD2lE (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2rE`")] +Notation lee_dadd2rE := lee_dD2rE (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2l`")] +Notation lee_dadd2l := lee_dD2l (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2r`")] +Notation lee_dadd2r := lee_dD2r (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD`")] +Notation lee_dadd := lee_dD (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dB`")] +Notation lee_dsub := lee_dB (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBlDr`")] +Notation lte_dsubl_addr := lte_dBlDr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBlDl`")] +Notation lte_dsubl_addl := lte_dBlDl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBrDr`")] +Notation lte_dsubr_addr := lte_dBrDr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBrDl`")] +Notation lte_dsubr_addl := lte_dBrDl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_le_dD`")] +Notation lte_le_dadd := lte_le_dD (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_lt_dD`")] +Notation lee_lt_dadd := lee_lt_dD (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_le_dB`")] +Notation lte_le_dsub := lte_le_dD (only parsing). -Lemma lte_opp2 {R : numDomainType} : {mono @oppe R : x y /~ x < y}. -Proof. -move=> x y; case: x y => [?||] [?||] //; first by rewrite !lte_fin !ltrN2. - by rewrite /Order.lt/= realN. -by rewrite /Order.lt/= realN. -Qed. +End DualAddTheoryRealDomain. Section realFieldType_lemmas. Variable R : realFieldType. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 2190aa44c..0f9a8eb96 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2224,11 +2224,9 @@ move=> V [/[dup] /compact_measurable mV cptV VFND] FDV1 M1FD. rewrite (@le_trans _ _ (mu V))//; last first. apply: ereal_sup_ub; exists V => //=; split => //. exact: (subset_trans VFND (@subIsetr _ _ _)). -rewrite -(@leeD2lE _ 1)// {1}addeC -EFinD (le_trans M1FD)//. +rewrite -(@leeD2rE _ 1)// -EFinD (le_trans M1FD)//. rewrite /mu (@measureDI _ _ _ _ (F N `&` D) _ _ mV)/=; last exact: measurableI. -rewrite ltW// lte_le_add // ?ge0_fin_numE //; last first. - by rewrite measureIr//; apply: measurableI. -by rewrite -setIA (le_lt_trans _ (ffin N).2)// measureIl//; exact: measurableI. +by rewrite addeC leeD//; [rewrite measureIr//; exact: measurableI|exact/ltW]. Qed. End lebesgue_regularity. diff --git a/theories/realfun.v b/theories/realfun.v index 8a5bdd953..c3e8f3927 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -2358,8 +2358,7 @@ rewrite {1}variation_prev; last exact: itv_partition1. rewrite /= -addeA -lteBrDr; last by rewrite fin_numD; apply/andP. rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA. move/lt_trans; apply. -rewrite [x in (_ < x%:E)%E]splitr EFinD addeC lteD2lE //. -rewrite -addeA. +rewrite [in ltRHS](splitr (eps%:num)) EFinD lteD2rE// -addeA. apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E). rewrite [in leRHS]variation_prev; last exact: itv_partition1. rewrite geeDl// sube_le0; apply: ereal_sup_ub => /=.