From e6b2a8711ddc0ce15d97b2f51601dc0a3a7594cc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 3 Jul 2025 01:14:07 +0900 Subject: [PATCH] less unitfE Co-authored-by: Kazuhiko Sakaguchi --- reals/constructive_ereal.v | 53 +++++++++---------- theories/charge.v | 6 +-- theories/derive.v | 13 ++--- theories/exp.v | 2 +- theories/hoelder.v | 4 +- theories/landau.v | 4 +- theories/lebesgue_measure.v | 5 +- theories/measurable_realfun.v | 2 +- theories/measure.v | 2 +- theories/normedtype_theory/normed_module.v | 2 +- theories/normedtype_theory/num_normedtype.v | 12 ++--- .../pseudometric_normed_Zmodule.v | 3 +- theories/normedtype_theory/vitali_lemma.v | 2 +- theories/numfun.v | 8 +-- theories/probability.v | 2 +- theories/sequences.v | 11 ++-- 16 files changed, 61 insertions(+), 70 deletions(-) diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 5f8b5d4a76..0e8ea79d9e 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -3533,21 +3533,21 @@ move=> x0; apply/(iffP idP) => [xy r /andP[r0 r1]|h]. move: x0 xy; rewrite le_eqVlt => /predU1P[<-|x0 xy]; first by rewrite mule0. by rewrite (le_trans _ xy)// gee_pMl// ltW. have h01 : (0 < (2^-1 : R) < 1)%R by rewrite invr_gt0 ?invf_lt1 ?ltr0n ?ltr1n. -move: x y => [x||] [y||] // in x0 h *. -- move: (x0); rewrite lee_fin le_eqVlt => /predU1P[<-|{}x0]. - by rewrite (le_trans _ (h _ h01))// mule_ge0// lee_fin. - have y0 : (0 < y)%R. - by rewrite -lte_fin (lt_le_trans _ (h _ h01))// mule_gt0// lte_fin. - rewrite lee_fin leNgt; apply/negP => yx. - have /h : (0 < (y + x) / (2 * x) < 1)%R. - rewrite ltr_pdivlMr ?ltr_pdivrMr ?mulr_gt0// mul0r mul1r. - by rewrite mulr_natl mulr2n ltrD2r yx addr_gt0. - rewrite -(EFinM _ x) lee_fin invrM ?unitfE// ?gt_eqF// -mulrA mulrAC. - by rewrite mulVr ?unitfE ?gt_eqF// mul1r; apply/negP; rewrite -ltNge midf_lt. +move: x y => [x||] [y||] // in x0 h *; last 4 first. - by rewrite leey. - by have := h _ h01. - by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e. - by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e. +move: (x0); rewrite lee_fin le_eqVlt => /predU1P[<-|{}x0]. + by rewrite (le_trans _ (h _ h01))// mule_ge0// lee_fin. +have y0 : (0 < y)%R. + by rewrite -lte_fin (lt_le_trans _ (h _ h01))// mule_gt0// lte_fin. +rewrite lee_fin leNgt; apply/negP => yx. +have /h : (0 < (y + x) / (2 * x) < 1)%R. + apply/andP; split; first by rewrite divr_gt0 // ?addr_gt0// ?mulr_gt0. + by rewrite ltr_pdivrMr ?mulr_gt0// mul1r mulr_natl mulr2n ltrD2r. +rewrite -EFinM lee_fin invfM -mulrA divfK ?gt_eqF//. +by apply/negP; rewrite -ltNge midf_lt. Qed. Lemma lte_pdivrMl r x y : (0 < r)%R -> (r^-1%:E * y < x) = (y < r%:E * x). @@ -3606,9 +3606,9 @@ Lemma lee_pdivrMl r x y : (0 < r)%R -> (r^-1%:E * y <= x) = (y <= r%:E * x). Proof. move=> r0; apply/idP/idP. - rewrite le_eqVlt => /predU1P[<-|]; last by rewrite lte_pdivrMl// => /ltW. - by rewrite muleA -EFinM divrr ?mul1e// unitfE gt_eqF. + by rewrite muleA -EFinM divff ?mul1e// gt_eqF. - rewrite le_eqVlt => /predU1P[->|]; last by rewrite -lte_pdivrMl// => /ltW. - by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF. + by rewrite muleA -EFinM mulVf ?mul1e// gt_eqF. Qed. Lemma lee_pdivrMr r x y : (0 < r)%R -> (y * r^-1%:E <= x) = (y <= x * r%:E). @@ -3618,9 +3618,9 @@ Lemma lee_pdivlMl r y x : (0 < r)%R -> (x <= r^-1%:E * y) = (r%:E * x <= y). Proof. move=> r0; apply/idP/idP. - rewrite le_eqVlt => /predU1P[->|]; last by rewrite lte_pdivlMl// => /ltW. - by rewrite muleA -EFinM divrr ?mul1e// unitfE gt_eqF. + by rewrite muleA -EFinM divff ?mul1e// gt_eqF. - rewrite le_eqVlt => /predU1P[<-|]; last by rewrite -lte_pdivlMl// => /ltW. - by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF. + by rewrite muleA -EFinM mulVf ?mul1e// gt_eqF. Qed. Lemma lee_pdivlMr r x y : (0 < r)%R -> (x <= y * r^-1%:E) = (x * r%:E <= y). @@ -4512,8 +4512,7 @@ Definition contract x : R := Lemma contract_lt1 r : (`|contract r%:E| < 1)%R. Proof. -rewrite normrM normrV ?unitfE //. -rewrite ltr_pdivrMr // ?mul1r//; last by rewrite gtr0_norm. +rewrite normrM normfV// ltr_pdivrMr // ?mul1r//; last by rewrite gtr0_norm. by rewrite [ltRHS]gtr0_norm ?ltrDr// ltr_pwDl. Qed. @@ -4561,25 +4560,23 @@ move=> r; rewrite inE le_eqVlt => /orP[|r1]. by [rewrite expand1|rewrite expandN1]. rewrite /expand 2!leNgt ltrNl; case/ltr_normlP : (r1) => -> -> /=. have r_pneq0 : (1 + r / (1 - r) != 0)%R. - rewrite -[X in (X + _)%R](@divrr _ (1 - r)%R) -?mulrDl; last first. - by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW. + rewrite -[X in (X + _)%R](@divff _ (1 - r)%R) -?mulrDl; last first. + by rewrite subr_eq0 eq_sym lt_eqF // ltr_normlW. by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym lt_eqF // ltr_normlW. have r_nneq0 : (1 - r / (1 + r) != 0)%R. - rewrite -[X in (X + _)%R](@divrr _ (1 + r)%R) -?mulrBl; last first. - by rewrite unitfE addrC addr_eq0 gt_eqF // ltrNnormlW. - rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym gt_eqF //. - exact: ltrNnormlW. + rewrite -[X in (X + _)%R](@divff _ (1 + r)%R) -?mulrBl; last first. + by rewrite addrC addr_eq0 gt_eqF // ltrNnormlW. + by rewrite addrK mulf_neq0// invr_eq0 addr_eq0 -eqr_oppLR lt_eqF// ltrNnormlW. wlog : r r1 r_pneq0 r_nneq0 / (0 <= r)%R => wlog_r0. have [r0|r0] := lerP 0 r; first by rewrite wlog_r0. move: (wlog_r0 (- r)%R). rewrite !(normrN, opprK, mulNr) oppr_ge0 => /(_ r1 r_nneq0 r_pneq0 (ltW r0)). - by move/eqP; rewrite eqr_opp => /eqP. + by move/oppr_inj. rewrite /contract !ger0_norm //; last first. by rewrite divr_ge0 // subr_ge0 (le_trans _ (ltW r1)) // ler_norm. -apply: (@mulIr _ (1 + r / (1 - r))%R); first by rewrite unitfE. -rewrite -(mulrA (r / _)%R) mulVr ?unitfE // mulr1. -rewrite -[X in (X + _ / _)%R](@divrr _ (1 - r)%R) -?mulrDl ?subrK ?div1r //. -by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW. +apply: (@mulIf _ (1 + r / (1 - r))%R); rewrite // divfK//. +rewrite -[X in (X + _ / _)%R](@divff _ (1 - r)%R) -?mulrDl ?subrK ?div1r //. +by rewrite subr_eq0 eq_sym lt_eqF // ltr_normlW. Qed. Lemma le_contract : {mono contract : x y / (x <= y)%O}. diff --git a/theories/charge.v b/theories/charge.v index aedd8f8e14..e635c77927 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -864,7 +864,7 @@ have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n --> move/cvg_series_cvg_0 => maxe_cvg_0. apply: not_s_cvg_0. rewrite (_ : _ \o _ = (fun n => z_ (v n) * 2^-1%:E) \* cst 2%:E); last first. - by apply/funext => n/=; rewrite -muleA -EFinM mulVr ?mule1// unitfE. + by apply/funext => n/=; rewrite -muleA -EFinM mulVf ?mule1. rewrite (_ : 0 = 0 * 2%:E); last by rewrite mul0e. apply: cvgeM; [by rewrite mule_def_fin| |exact: cvg_cst]. apply/fine_cvgP; split. @@ -1586,8 +1586,8 @@ exists (PosNum e_gt0); rewrite ge0_integralD//; last 2 first. rewrite integral_cst// -lteBrDr//; last first. by rewrite fin_numM// fin_num_measure. rewrite -[X in _ * X](@fineK _ (mu A)) ?fin_num_measure//. -rewrite -EFinM -mulrA mulVr ?mulr1; last first. - by rewrite unitfE gt_eqF// fine_gt0// muA_gt0/= ltey_eq fin_num_measure. +rewrite -EFinM -mulrA mulVf ?mulr1; last first. + by rewrite gt_eqF// fine_gt0// muA_gt0/= ltey_eq fin_num_measure. rewrite lteBrDl// addeC -lteBrDl//; last first. rewrite -(@fineK _ (nu A))// ?fin_num_measure// -[X in _ - X](@fineK _)//. rewrite -EFinB lte_fin /mid ltr_pdivrMr// ltr_pMr// ?ltr1n// subr_gt0. diff --git a/theories/derive.v b/theories/derive.v index db9062fc37..9494425809 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -341,8 +341,7 @@ rewrite add0r normrN normrZ -ltr_pdivlMl ?normr_gt0 ?invr_neq0 //. have /Hi/le_lt_trans -> // : ball 0 i (j *: v). by rewrite -ball_normE/= add0r normrN (le_lt_trans _ jvi) // normrZ. rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulrA mulVf ?gt_eqF//. -rewrite normrV ?unitfE // div1r invrK ltr_pdivrMl; last first. - by rewrite pmulr_rgt0 // normr_gt0. +rewrite normfV div1r invrK ltr_pdivrMl; last by rewrite pmulr_rgt0 // normr_gt0. rewrite normrZ mulrC -mulrA. by rewrite ltr_pMl ?ltr1n // pmulr_rgt0 ?normm_gt0 // normr_gt0. Qed. @@ -709,8 +708,8 @@ suff /he : ball 0 e%:num (k^-1 *: x). rewrite -ball_normE /= distrC subr0 => /ltW /le_trans; apply. by rewrite ger0_norm /k // mulVf. rewrite -ball_normE /= distrC subr0 normrZ. -rewrite normfV ger0_norm /k // invrM ?unitfE // mulrAC mulVf //. -by rewrite invf_div mul1r [ltRHS]splitr; apply: ltr_pwDr. +rewrite normfV ger0_norm /k // invfM/= -mulrA mulVf ?gt_eqF//. +by rewrite mulr1 invf_div gtr_pMr// invf_lt1// ltr1n. Qed. Lemma linear_eqO (V' W' : normedModType R) (f : {linear V' -> W'}) : @@ -784,10 +783,8 @@ suff /he : ball 0 e%:num (ku^-1 *: u, kv^-1 *: v). by rewrite mulrA [ku * _]mulrAC expr2. rewrite -ball_normE /= distrC subr0. have -> : (ku^-1 *: u, kv^-1 *: v) = - (e%:num / 2) *: ((PosNum un0)%:num ^-1 *: u, (PosNum vn0)%:num ^-1 *: v). - rewrite invrM ?unitfE // [kv ^-1]invrM ?unitfE //. - rewrite mulrC -[_ *: u]scalerA [X in X *: v]mulrC -[_ *: v]scalerA. - by rewrite invf_div. + (e%:num / 2) *: ((PosNum un0)%:num ^-1 *: u, (PosNum vn0)%:num ^-1 *: v). + by rewrite invfM [kv ^-1]invfM invf_div -[_ *: u]scalerA -[_ *: v]scalerA. rewrite normrZ ger0_norm // -mulrA gtr_pMr // ltr_pdivrMl // mulr1. by rewrite prod_normE/= !normrZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n. Qed. diff --git a/theories/exp.v b/theories/exp.v index f24e01a2eb..819e5713d9 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -1003,7 +1003,7 @@ rewrite le_eqVlt => /predU1P[<-|a0]. by rewrite powR0 ?invr_eq0 ?pnatr_eq0// sqrtr0. have /eqP : (a `^ (2^-1)) ^+ 2 = (Num.sqrt a) ^+ 2. rewrite sqr_sqrtr; last exact: ltW. - by rewrite /powR gt_eqF// -expRM_natl mulrA divrr ?mul1r ?unitfE// lnK. + by rewrite /powR gt_eqF// -expRM_natl mulrA divff ?mul1r// lnK. rewrite eqf_sqr => /predU1P[//|/eqP h]. have : 0 < a `^ 2^-1 by exact: powR_gt0. by rewrite h oppr_gt0 ltNge sqrtr_ge0. diff --git a/theories/hoelder.v b/theories/hoelder.v index c452c1d042..cd73616655 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -440,9 +440,9 @@ rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first. rewrite -!muleA [X in _ * X](_ : _ = 1) ?mule1// EFinM muleACA. rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e; last first. rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0. - by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// fpos/= ltey. + by rewrite -EFinM mulVf ?gt_eqF// fine_gt0// fpos/= ltey. rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0. - by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// gpos/= ltey. + by rewrite -EFinM mulVf ?gt_eqF// fine_gt0// gpos/= ltey. rewrite -(mul1e ('N_p%:E[f] * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//. rewrite [leRHS](_ : _ = \int[mu]_x (F x `^ p / p + G x `^ q / q)%:E). rewrite Lnorm1 ae_ge0_le_integral //. diff --git a/theories/landau.v b/theories/landau.v index d7ad161ff9..4e0ad17b92 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -1334,8 +1334,8 @@ rewrite eqOmegaE eqOmegaO [in RHS]bigOE //. have [W1 k1 ?] := bigOmega; have [W2 k2 ?] := bigOmega. near=> k; near=> x; rewrite [`|_|]normrM. rewrite (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(W1 * W2) x|)) //. - rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //. - rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (W1 x)). + rewrite invfM -mulrA ler_pdivlMl// ler_pdivlMl//. + rewrite (mulrCA k2%:num) (mulrA k1%:num) (@normrM _ (W1 x)). by rewrite ler_pM ?mulr_ge0 //; near: x. by rewrite ler_wpM2r // ltW //. Unshelve. all: by end_near. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 4ed29faadd..3118e50f9e 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -626,14 +626,13 @@ rewrite itv_bnd_open_bigcup//; transitivity (limn (lebesgue_measure \o - by move=> ?; exact: measurable_itv. - by apply: bigcup_measurable => k _; exact: measurable_itv. - move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=]. - by move/le_trans; apply; rewrite lerB// ler_pV2 ?ler_nat//; - rewrite inE ltr0n andbT unitfE. + by move/le_trans; apply; rewrite lerB// lef_pV2 ?ler_nat ?posrE. rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)); last first. apply/funext => n /=; rewrite lebesgue_measure_itvoc. have [->|n0] := eqVneq n 0%N. by rewrite invr1 subrr set_itvoc0 wlength0. rewrite wlength_itv/= lte_fin ifT; last first. - by rewrite ler_ltB// invr_lt1 ?unitfE// ltr1n ltnS lt0n. + by rewrite ler_ltB// invf_lt1// ltr1n ltnS lt0n. by rewrite !(EFinB,EFinN) fin_num_oppeB// addeAC addeA subee// add0e. apply/cvg_lim => //=; apply/fine_cvgP; split => /=; first exact: nearW. apply/(@cvgrPdist_lt _ R^o) => _/posnumP[e]. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index a7d0381252..186c57c810 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -995,7 +995,7 @@ move=> mf mg; rewrite (_ : (_ \* _) = (fun x => 2%:R^-1 * (f x + g x) ^+ 2) exact: measurableT_comp (exprn_measurable _) _. rewrite funeqE => x /=; rewrite -2!mulrBr sqrrD (addrC (f x ^+ 2)) -addrA. rewrite -(addrA (f x * g x *+ 2)) -opprB opprK (addrC (g x ^+ 2)) addrK. -by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVr ?mul1r// unitfE. +by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVf ?mul1r. Qed. Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g -> diff --git a/theories/measure.v b/theories/measure.v index 2956ce6a65..c3eff8723d 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -3618,7 +3618,7 @@ Proof. rewrite /mnormalize; case: ifPn; first by rewrite probability_setT. rewrite negb_or => /andP[ft0 ftoo]. have ? : mu setT \is a fin_num by rewrite ge0_fin_numE// ltey. -by rewrite -{1}(@fineK _ (mu setT))// -EFinM divrr// ?unitfE fine_eq0. +by rewrite -{1}(@fineK _ (mu setT))// -EFinM divff// fine_eq0. Qed. HB.instance Definition _ := diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 3ec114f2fd..399ca49b3a 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1975,7 +1975,7 @@ have [es|se] := leP s e%:num; last first. by apply: B0y; rewrite -ball_normE /ball_ /= distrC xye. exists (y + (s / 2) *: (`|x - y|^-1 *: (x - y))); split; [apply: Be|apply: B0y]. rewrite /= opprD addrA -[X in `|X - _|](scale1r (x - y)) scalerA -scalerBl. - rewrite -[X in X - _](@divrr _ `|x - y|) ?unitfE ?normr_eq0 ?subr_eq0//. + rewrite -[X in X - _](@divff _ `|x - y|) ?normr_eq0 ?subr_eq0//. rewrite -mulrBl -scalerA normrZ normfZV ?subr_eq0// mulr1. rewrite gtr0_norm; first by rewrite ltrBlDl xye ltrDr mulr_gt0. by rewrite subr_gt0 xye ltr_pdivrMr // mulr_natr mulr2n ltr_pwDl. diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index 0ac8720f61..09773081e8 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -719,8 +719,8 @@ Notation near_in_itv := near_in_itvoo (only parsing). Lemma near_infty_natSinv_lt (R : archiFieldType) (e : {posnum R}) : \forall n \near \oo, n.+1%:R^-1 < e%:num. Proof. -near=> n; rewrite -(@ltr_pM2r _ n.+1%:R) // mulVr ?unitfE //. -rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVr ?unitfE // mul1r. +near=> n; rewrite -(@ltr_pM2r _ n.+1%:R) // mulVf. +rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVf// mul1r. rewrite (lt_trans (archi_boundP _)) // ltr_nat. by near: n; exists (Num.bound e%:num^-1). Unshelve. all: by end_near. Qed. @@ -729,10 +729,10 @@ Lemma near_infty_natSinv_expn_lt (R : archiFieldType) (e : {posnum R}) : \forall n \near \oo, 1 / 2 ^+ n < e%:num. Proof. near=> n. -rewrite -(@ltr_pM2r _ (2 ^+ n)) // -?natrX ?ltr0n ?expn_gt0//. -rewrite mul1r mulVr ?unitfE ?gt_eqF// ?ltr0n ?expn_gt0//. -rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVr ?unitfE // mul1r. -rewrite (lt_trans (archi_boundP _)) // natrX upper_nthrootP //. +rewrite -(@ltr_pM2r _ (2 ^+ n))// -?natrX ?ltr0n ?expn_gt0//. +rewrite mul1r mulVf ?gt_eqF//. +rewrite -(@ltr_pM2l _ e%:num^-1)// mulr1 mulrA mulVf// mul1r. +rewrite (lt_trans (archi_boundP _))// natrX upper_nthrootP//. near: n; eexists; last by move=> m; exact. by []. Unshelve. all: by end_near. Qed. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 2c93a3da7e..48005b39b8 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -412,8 +412,7 @@ apply/negPn/negP => /set0P[c] []; rewrite -ball_normE /ball_ => acr bcr. have r22 : r%:num * 2 = r%:num + r%:num. by rewrite (_ : 2 = 1 + 1) // mulrDr mulr1. move: (ltrD acr bcr); rewrite -r22 (distrC b c). -move/(le_lt_trans (ler_distD c a b)). -by rewrite -mulrA mulVr ?mulr1 ?ltxx // unitfE. +by move/(le_lt_trans (ler_distD c a b)); rewrite -mulrA mulVf// mulr1 ltxx. Qed. Local Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core. diff --git a/theories/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v index 0c6248f4c7..448833277d 100644 --- a/theories/normedtype_theory/vitali_lemma.v +++ b/theories/normedtype_theory/vitali_lemma.v @@ -535,7 +535,7 @@ have Bjrn : (radius (B j))%:num > r / (2 ^ n.+1)%:R. exists j; split => //. - by case: Dj => m /= mn Dm; exists m. - rewrite (le_trans _ (ltW Bjrn))// ler_pdivrMr// expnSr natrM. - by rewrite invrM ?unitfE// mulrAC -mulrA (mulrA 2) divff// div1r. + by rewrite invfM -!mulrA mulVf// mulr1. - move=> x Bix. rewrite is_ball_closure//; last first. by rewrite (ballE (is_ballB j)) scale_ballE; [exact: is_ball_ball|]. diff --git a/theories/numfun.v b/theories/numfun.v index c3083f2448..bde2baaf01 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -575,7 +575,7 @@ move=> x Ax; have := fA1 _ Ax; rewrite 2!ler_norml => /andP[Mfx fxM]. have [xL|xL] := leP (f x) (-(1/3) * M%:num). have: [set g x | x in A `&` f@^-1` `]-oo, -(1/3) * M%:num]] (g x) by exists x. move/gL3=> ->; rewrite !mulNr opprK; apply/andP; split. - by rewrite -lerBlDr -opprD -2!mulrDl natr1 divrr ?unitfE// mul1r. + by rewrite -lerBlDr -opprD -2!mulrDl natr1 divff// mul1r. rewrite -lerBrDr -2!mulrBl -(@natrB _ 2 1)// (le_trans xL)//. by rewrite ler_pM2r// ltW// gtrN// divr_gt0. have [xR|xR] := lerP (1/3 * M%:num) (f x). @@ -584,7 +584,7 @@ have [xR|xR] := lerP (1/3 * M%:num) (f x). move/gR3 => ->; apply/andP; split. rewrite lerBrDl -2!mulrBl (le_trans _ xR)// ler_pM2r//. by rewrite ler_wpM2r ?invr_ge0 ?ler0n// lerBlDl natr1 ler1n. - by rewrite lerBlDl -2!mulrDl nat1r divrr ?mul1r// unitfE. + by rewrite lerBlDl -2!mulrDl nat1r divff ?mul1r. have /andP[ng3 pg3] : -(1/3) * M%:num <= g x <= 1/3 * M%:num. by apply: grng; exists x. rewrite ?(intrD _ 1 1) !mulrDl; apply/andP; split. @@ -606,7 +606,7 @@ by move=> bd pm cf; have [g ?] := tietze_step' pm cf bd; exists g. Qed. Let onem_twothirds : 1 - 2/3 = 1/3 :> R. -Proof. by apply/eqP; rewrite subr_eq/= -mulrDl nat1r divrr// unitfE. Qed. +Proof. by apply/eqP; rewrite subr_eq/= -mulrDl nat1r divff. Qed. (** Tietze's theorem: *) Lemma continuous_bounded_extension (f : X -> R^o) M : @@ -681,7 +681,7 @@ exists (lim (h_ @ \oo)); split. rewrite (le_trans (lim_series_norm _))//; apply: le_trans. exact/(lim_series_le cvg_gt _ (g_bd ^~ t))/is_cvg_geometric_series. rewrite (cvg_lim _ (cvg_geometric_series _))//; last exact: Rhausdorff. - by rewrite onem_twothirds mulrAC divrr ?mul1r// unitfE. + by rewrite onem_twothirds mulrAC divff mul1r. Unshelve. all: by end_near. Qed. End Tietze. diff --git a/theories/probability.v b/theories/probability.v index d7c5b6d228..6d9585dc04 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -745,7 +745,7 @@ rewrite eqr_div; [|apply: lt0r_neq0..]; last 2 first. - by rewrite exprz_gt0 -1?[ltLHS]addr0 ?ltr_leD. - by rewrite ltr_wpDl ?fine_ge0 ?variance_ge0 ?exprz_gt0. apply/eqP; have -> : fine 'V_P[X] = (u0 * lambda)%R. - by rewrite /u0 -mulrA mulVr ?mulr1 ?unitfE ?gt_eqF. + by rewrite /u0 -mulrA mulVf ?mulr1 ?gt_eqF. by rewrite -mulrDl -mulrDr (addrC u0) [in RHS](mulrAC u0) -exprnP expr2 !mulrA. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index efd5c573de..dc394ad03a 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -825,7 +825,7 @@ suff abel : forall n, set h := 'o_\oo (@harmonic R). apply/eqoP => _/posnumP[e] /=. near=> n; rewrite normr1 mulr1 normrM -ler_pdivlMl ?normr_gt0//. - rewrite mulrC -normrV ?unitfE //. + rewrite mulrC -normfV. near: n. by case: (eqoP eventually_filterType (@harmonic R) h) => Hh _; apply Hh. move: (cesaro a_o); rewrite /arithmetic_mean /series /= -/a_. @@ -836,7 +836,7 @@ case => [|n]. rewrite /arithmetic_mean /= seriesEnat /= big_nat_recl //=. under eq_bigr do rewrite [u_ _]eq_sum_telescope. rewrite big_split /= big_const_nat iter_addr addr0 addrA -mulrS mulrDr. -rewrite -(mulr_natl (u_ O)) mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r opprD addrA. +rewrite -(mulr_natl (u_ O)) mulrA mulVf ?pnatr_eq0// mul1r opprD addrA. rewrite eq_sum_telescope (addrC (u_ O)) addrK. rewrite [X in _ - _ * X](_ : _ = \sum_(0 <= i < n.+1) \sum_(0 <= k < n.+1 | (k < i.+1)%N) a_ k); last first. @@ -863,7 +863,7 @@ rewrite [X in _ - _ * X](_ : _ = rewrite big_distrr /= big_mkord (big_morph _ (@opprD _) (@oppr0 _)). rewrite seriesEord -big_split /= big_add1 /= big_mkord; apply: eq_bigr => i _. rewrite mulrCA -[X in X - _]mulr1 -mulrBr [RHS]mulrC; congr (_ * _). -rewrite -[X in X - _](@divrr _ (n.+2)%:R) ?unitfE ?pnatr_eq0 //. +rewrite -[X in X - _](@divff _ (n.+2)%:R) ?pnatr_eq0//. rewrite [in X in _ - X]mulrC -mulrBl; congr (_ / _). rewrite -natrB; last by rewrite (@leq_trans n.+1) // leq_subr. rewrite subnBA; by [rewrite addSnnS addnC addnK | rewrite ltnW]. @@ -966,8 +966,7 @@ rewrite (_ : series _ = series (geometric (r / (2 ^ n.+1)%:R) 2^-1%R)); last fir rewrite funeqE => m; rewrite /series /=; apply: eq_bigr => k _. by rewrite expnD natrM (mulrC (2 ^ k)%:R) invfM exprVn (natrX _ 2 k) mulrA. apply: cvg_trans. - apply: cvg_geometric_series. - by rewrite ger0_norm // invr_lt1 // ?ltr1n // unitfE. + by apply: cvg_geometric_series; rewrite ger0_norm // invf_lt1 // ?ltr1n. rewrite [X in (X - _)%R](splitr 1) div1r addrK. by rewrite -mulrA -invfM expnSr natrM -mulrA divff// mulr1 natrX. Qed. @@ -2634,7 +2633,7 @@ have /le_trans -> // : `| y n - y (n + m)| <= rewrite -[q%:num]/(q'%:num) -!mulrA -mulrDr ler_pM// {}/q'/=. rewrite -!/(`1-_) -mulrDr exprSr onemM -addrA. rewrite -[in leRHS](mulrC _ `1-(_ ^+ m)) -onemMr onemK. - by rewrite [in leRHS]mulrDl mulrAC mulrV ?mul1r// unitf_gt0// onem_gt0. + by rewrite [in leRHS]mulrDl mulrAC mulfV ?mul1r// gt_eqF// onem_gt0. rewrite geometric_seriesE ?lt_eqF//= -[leRHS]mulr1 (ACl (1*4*2*3))/= -/C. by rewrite ler_wpM2l// 1?mulr_ge0// lerBlDr lerDl. Qed.