diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 67bb43c3b..fb0dceb25 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -8,6 +8,25 @@ ### Renamed +- in `constructive_ereal.v`: + + `lte_pdivr_mull` -> `lte_pdivrMl` + + `lte_pdivr_mulr` -> `lte_pdivrMr` + + `lte_pdivl_mull` -> `lte_pdivlMl` + + `lte_pdivl_mulr` -> `lte_pdivlMr` + + `lte_ndivl_mulr` -> `lte_ndivlMr` + + `lte_ndivl_mull` -> `lte_ndivlMl` + + `lte_ndivr_mull` -> `lte_ndivrMl` + + `lte_ndivr_mulr` -> `lte_ndivrMr` + + `lee_pdivr_mull` -> `lee_pdivrMl` + + `lee_pdivr_mulr` -> `lee_pdivrMr` + + `lee_pdivl_mull` -> `lee_pdivlMl` + + `lee_pdivl_mulr` -> `lee_pdivlMr` + + `lee_ndivl_mulr` -> `lee_ndivlMr` + + `lee_ndivl_mull` -> `lee_ndivlMl` + + `lee_ndivr_mull` -> `lee_ndivrMl` + + `lee_ndivr_mulr` -> `lee_ndivrMr` + + `eqe_pdivr_mull` -> `eqe_pdivrMl` + ### Generalized ### Deprecated diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 63adf6ecf..831e91b69 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -3143,7 +3143,7 @@ move: x y => [x||] [y||] // in x0 h *. - by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e. Qed. -Lemma lte_pdivr_mull r x y : (0 < r)%R -> (r^-1%:E * y < x) = (y < r%:E * x). +Lemma lte_pdivrMl r x y : (0 < r)%R -> (r^-1%:E * y < x) = (y < r%:E * x). Proof. move=> r0; move: x y => [x| |] [y| |] //=. - by rewrite 2!lte_fin ltr_pdivrMl. @@ -3157,10 +3157,10 @@ move=> r0; move: x y => [x| |] [y| |] //=. - by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e. Qed. -Lemma lte_pdivr_mulr r x y : (0 < r)%R -> (y * r^-1%:E < x) = (y < x * r%:E). -Proof. by move=> r0; rewrite muleC lte_pdivr_mull// muleC. Qed. +Lemma lte_pdivrMr r x y : (0 < r)%R -> (y * r^-1%:E < x) = (y < x * r%:E). +Proof. by move=> r0; rewrite muleC lte_pdivrMl// muleC. Qed. -Lemma lte_pdivl_mull r y x : (0 < r)%R -> (x < r^-1%:E * y) = (r%:E * x < y). +Lemma lte_pdivlMl r y x : (0 < r)%R -> (x < r^-1%:E * y) = (r%:E * x < y). Proof. move=> r0; move: x y => [x| |] [y| |] //=. - by rewrite 2!lte_fin ltr_pdivlMl. @@ -3174,78 +3174,112 @@ move=> r0; move: x y => [x| |] [y| |] //=. - by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e. Qed. -Lemma lte_pdivl_mulr r x y : (0 < r)%R -> (x < y * r^-1%:E) = (x * r%:E < y). -Proof. by move=> r0; rewrite muleC lte_pdivl_mull// muleC. Qed. +Lemma lte_pdivlMr r x y : (0 < r)%R -> (x < y * r^-1%:E) = (x * r%:E < y). +Proof. by move=> r0; rewrite muleC lte_pdivlMl// muleC. Qed. -Lemma lte_ndivl_mulr r x y : (r < 0)%R -> (x < y * r^-1%:E) = (y < x * r%:E). +Lemma lte_ndivlMr r x y : (r < 0)%R -> (x < y * r^-1%:E) = (y < x * r%:E). Proof. rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN. -by rewrite EFinN muleN lteNr lte_pdivr_mulr// EFinN muleNN. +by rewrite EFinN muleN lteNr lte_pdivrMr// EFinN muleNN. Qed. -Lemma lte_ndivl_mull r x y : (r < 0)%R -> (x < r^-1%:E * y) = (y < r%:E * x). -Proof. by move=> r0; rewrite muleC lte_ndivl_mulr// muleC. Qed. +Lemma lte_ndivlMl r x y : (r < 0)%R -> (x < r^-1%:E * y) = (y < r%:E * x). +Proof. by move=> r0; rewrite muleC lte_ndivlMr// muleC. Qed. -Lemma lte_ndivr_mull r x y : (r < 0)%R -> (r^-1%:E * y < x) = (r%:E * x < y). +Lemma lte_ndivrMl r x y : (r < 0)%R -> (r^-1%:E * y < x) = (r%:E * x < y). Proof. rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN. -by rewrite EFinN mulNe lteNl lte_pdivl_mull// EFinN muleNN. +by rewrite EFinN mulNe lteNl lte_pdivlMl// EFinN muleNN. Qed. -Lemma lte_ndivr_mulr r x y : (r < 0)%R -> (y * r^-1%:E < x) = (x * r%:E < y). -Proof. by move=> r0; rewrite muleC lte_ndivr_mull// muleC. Qed. +Lemma lte_ndivrMr r x y : (r < 0)%R -> (y * r^-1%:E < x) = (x * r%:E < y). +Proof. by move=> r0; rewrite muleC lte_ndivrMl// muleC. Qed. -Lemma lee_pdivr_mull r x y : (0 < r)%R -> (r^-1%:E * y <= x) = (y <= r%:E * x). +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_pdivr_mull// => /ltW. +- rewrite le_eqVlt => /predU1P[<-|]; last by rewrite lte_pdivrMl// => /ltW. by rewrite muleA -EFinM divrr ?mul1e// unitfE gt_eqF. -- rewrite le_eqVlt => /predU1P[->|]; last by rewrite -lte_pdivr_mull// => /ltW. +- rewrite le_eqVlt => /predU1P[->|]; last by rewrite -lte_pdivrMl// => /ltW. by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF. Qed. -Lemma lee_pdivr_mulr r x y : (0 < r)%R -> (y * r^-1%:E <= x) = (y <= x * r%:E). -Proof. by move=> r0; rewrite muleC lee_pdivr_mull// muleC. Qed. +Lemma lee_pdivrMr r x y : (0 < r)%R -> (y * r^-1%:E <= x) = (y <= x * r%:E). +Proof. by move=> r0; rewrite muleC lee_pdivrMl// muleC. Qed. -Lemma lee_pdivl_mull r y x : (0 < r)%R -> (x <= r^-1%:E * y) = (r%:E * x <= y). +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_pdivl_mull// => /ltW. +- rewrite le_eqVlt => /predU1P[->|]; last by rewrite lte_pdivlMl// => /ltW. by rewrite muleA -EFinM divrr ?mul1e// unitfE gt_eqF. -- rewrite le_eqVlt => /predU1P[<-|]; last by rewrite -lte_pdivl_mull// => /ltW. +- rewrite le_eqVlt => /predU1P[<-|]; last by rewrite -lte_pdivlMl// => /ltW. by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF. Qed. -Lemma lee_pdivl_mulr r x y : (0 < r)%R -> (x <= y * r^-1%:E) = (x * r%:E <= y). -Proof. by move=> r0; rewrite muleC lee_pdivl_mull// muleC. Qed. +Lemma lee_pdivlMr r x y : (0 < r)%R -> (x <= y * r^-1%:E) = (x * r%:E <= y). +Proof. by move=> r0; rewrite muleC lee_pdivlMl// muleC. Qed. -Lemma lee_ndivl_mulr r x y : (r < 0)%R -> (x <= y * r^-1%:E) = (y <= x * r%:E). +Lemma lee_ndivlMr r x y : (r < 0)%R -> (x <= y * r^-1%:E) = (y <= x * r%:E). Proof. rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN. -by rewrite EFinN muleN leeNr lee_pdivr_mulr// EFinN muleNN. +by rewrite EFinN muleN leeNr lee_pdivrMr// EFinN muleNN. Qed. -Lemma lee_ndivl_mull r x y : (r < 0)%R -> (x <= r^-1%:E * y) = (y <= r%:E * x). -Proof. by move=> r0; rewrite muleC lee_ndivl_mulr// muleC. Qed. +Lemma lee_ndivlMl r x y : (r < 0)%R -> (x <= r^-1%:E * y) = (y <= r%:E * x). +Proof. by move=> r0; rewrite muleC lee_ndivlMr// muleC. Qed. -Lemma lee_ndivr_mull r x y : (r < 0)%R -> (r^-1%:E * y <= x) = (r%:E * x <= y). +Lemma lee_ndivrMl r x y : (r < 0)%R -> (r^-1%:E * y <= x) = (r%:E * x <= y). Proof. rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN. -by rewrite EFinN mulNe leeNl lee_pdivl_mull// EFinN muleNN. +by rewrite EFinN mulNe leeNl lee_pdivlMl// EFinN muleNN. Qed. -Lemma lee_ndivr_mulr r x y : (r < 0)%R -> (y * r^-1%:E <= x) = (x * r%:E <= y). -Proof. by move=> r0; rewrite muleC lee_ndivr_mull// muleC. Qed. +Lemma lee_ndivrMr r x y : (r < 0)%R -> (y * r^-1%:E <= x) = (x * r%:E <= y). +Proof. by move=> r0; rewrite muleC lee_ndivrMl// muleC. Qed. -Lemma eqe_pdivr_mull r x y : (r != 0)%R -> +Lemma eqe_pdivrMl r x y : (r != 0)%R -> ((r^-1)%:E * y == x) = (y == r%:E * x). Proof. rewrite neq_lt => /orP[|] r0. -- by rewrite eq_le lee_ndivr_mull// lee_ndivl_mull// -eq_le. -- by rewrite eq_le lee_pdivr_mull// lee_pdivl_mull// -eq_le. +- by rewrite eq_le lee_ndivrMl// lee_ndivlMl// -eq_le. +- by rewrite eq_le lee_pdivrMl// lee_pdivlMl// -eq_le. Qed. End realFieldType_lemmas. +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivrMl`")] +Notation lte_pdivr_mull := lte_pdivrMl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivrMr`")] +Notation lte_pdivr_mulr := lte_pdivrMr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivlMl`")] +Notation lte_pdivl_mull := lte_pdivlMl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivlMr`")] +Notation lte_pdivl_mulr := lte_pdivlMr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivrMl`")] +Notation lee_pdivr_mull := lee_pdivrMl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivrMr`")] +Notation lee_pdivr_mulr := lee_pdivrMr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivlMl`")] +Notation lee_pdivl_mull := lee_pdivlMl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivlMr`")] +Notation lee_pdivl_mulr := lee_pdivlMr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivrMl`")] +Notation lte_ndivr_mull := lte_ndivrMl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivrMr`")] +Notation lte_ndivr_mulr := lte_ndivrMr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivlMl`")] +Notation lte_ndivl_mull := lte_ndivlMl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivlMr`")] +Notation lte_ndivl_mulr := lte_ndivlMr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivrMl`")] +Notation lee_ndivr_mull := lee_ndivrMl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivrMr`")] +Notation lee_ndivr_mulr := lee_ndivrMr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivlMl`")] +Notation lee_ndivl_mull := lee_ndivlMl (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivlMr`")] +Notation lee_ndivl_mulr := lee_ndivlMr (only parsing). +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `eqe_pdivrMl`")] +Notation eqe_pdivr_mull := eqe_pdivrMl (only parsing). Module DualAddTheoryRealField. diff --git a/theories/hoelder.v b/theories/hoelder.v index faf1b064a..38ff6ee92 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -179,7 +179,7 @@ under eq_integral do rewrite EFinM muleC. have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo. move/integrableP: ifp => -[_]. by under eq_integral do rewrite gee0_abs// ?lee_fin ?powR_ge0//. -rewrite integralZl//; apply/eqP; rewrite eqe_pdivr_mull ?mule1. +rewrite integralZl//; apply/eqP; rewrite eqe_pdivrMl ?mule1. - by rewrite fineK// gt0_fin_numE. - by rewrite gt_eqF// fine_gt0// foo andbT. Qed. @@ -423,14 +423,14 @@ suff : 'N_p%:E[(f \+ g)%R] `^ p <= ('N_p%:E[f] + 'N_p%:E[g]) * 'N_p%:E[(f \+ g)%R] `^ p * (fine 'N_p%:E[(f \+ g)%R])^-1%:E. have [-> _|Nfg0] := eqVneq 'N_p%:E[(f \+ g)%R] 0. by rewrite adde_ge0 ?Lnorm_ge0. - rewrite lee_pdivl_mulr ?fine_gt0// ?lt0e ?Nfg0 ?Lnorm_ge0//. + rewrite lee_pdivlMr ?fine_gt0// ?lt0e ?Nfg0 ?Lnorm_ge0//. rewrite -{1}(@fineK _ ('N_p%:E[(f \+ g)%R] `^ p)); last first. by rewrite fin_num_poweR// ge0_fin_numE// Lnorm_ge0. - rewrite -(invrK (fine _)) lee_pdivr_mull; last first. + rewrite -(invrK (fine _)) lee_pdivrMl; last first. rewrite invr_gt0 fine_gt0// (poweR_lty _ Nfgoo) andbT poweR_gt0//. by rewrite lt0e Nfg0 Lnorm_ge0. rewrite fineK ?ge0_fin_numE ?Lnorm_ge0// => /le_trans; apply. - rewrite lee_pdivr_mull; last first. + rewrite lee_pdivrMl; last first. by rewrite fine_gt0// poweR_lty// andbT poweR_gt0// lt0e Nfg0 Lnorm_ge0. by rewrite fineK// 1?muleC// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. have p0 : (0 < p)%R by exact: (lt_trans _ p1). diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 0670dfa84..16910f726 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -2374,7 +2374,7 @@ near=> n; have [ifoo|] := ltP (\int[mu]_(x in D) f x) +oo; last first. by near: n; exists 1%N => // n /= n0; rewrite gtr0_sg// ?lte_fin// ltr0n. rewrite -(@fineK _ (\int[mu]_(x in D) f x)); last first. by rewrite fin_numElt ifoo (le_lt_trans _ if_gt0). -rewrite -lee_pdivr_mulr//; last first. +rewrite -lee_pdivrMr//; last first. by move: if_gt0 ifoo; case: (\int[mu]_(x in D) f x). near: n. exists `|reals.ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //. @@ -2619,7 +2619,7 @@ rewrite monotone_convergence //. by rewrite mulry gtr0_sg ?mul1e ?leey// ltr0n. exists `|reals.ceil (M / fine (mu D))|%N => // m /=. rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//. - rewrite -lee_pdivr_mulr; last by rewrite fine_gt0// lt0e muD0 measure_ge0. + rewrite -lee_pdivrMr; last by rewrite fine_gt0// lt0e muD0 measure_ge0. rewrite lee_fin (le_trans _ MDm)//. by rewrite natr_absz (le_trans (ceil_ge _))// ler_int ler_norm. - by move=> n; exact: measurable_cst. @@ -5175,7 +5175,7 @@ apply: (le_lt_trans (integral_le_bound (M *+ 2)%:E _ _ _ _)) => //. - by rewrite lee_fin mulrn_wge0// ltW. - apply: aeW => z [Ez _]; rewrite /= lee_fin mulr2n. by rewrite (le_trans (ler_normB _ _))// lerD. -by rewrite -lte_pdivl_mull ?mulrn_wgt0// muleC -EFinM. +by rewrite -lte_pdivlMl ?mulrn_wgt0// muleC -EFinM. Qed. End continuous_density_L1. @@ -6029,7 +6029,7 @@ have ka_pos : fine k / a \is Num.pos. have k_fin_num : k \is a fin_num. by rewrite ge0_fin_numE ?locally_integrable_ltbally// integral_ge0. have kar : (0 < 2^-1 * (fine k / a) - r)%R. - move: afxr; rewrite -{1}(fineK k_fin_num) -lte_pdivr_mulr; last first. + move: afxr; rewrite -{1}(fineK k_fin_num) -lte_pdivrMr; last first. by rewrite fine_gt0// k_gt0/= ltey_eq k_fin_num. rewrite (lebesgue_measure_ball _ (ltW r0))//. rewrite -!EFinM !lte_fin -invf_div ltf_pV2 ?posrE ?pmulrn_lgt0//. @@ -6038,7 +6038,7 @@ have kar : (0 < 2^-1 * (fine k / a) - r)%R. near (0%R : R)^'+ => d. have axrdk : a%:E < (fine (mu (ball x (r + d))))^-1%:E * k. rewrite lebesgue_measure_ball//; last by rewrite addr_ge0// ltW. - rewrite -(fineK k_fin_num) -lte_pdivr_mulr; last first. + rewrite -(fineK k_fin_num) -lte_pdivrMr; last first. by rewrite fine_gt0// k_gt0/= locally_integrable_ltbally. rewrite -!EFinM !lte_fin -invf_div ltf_pV2//; last first. by rewrite posrE fine_gt0// ltry andbT lte_fin pmulrn_lgt0// addr_gt0. @@ -6086,7 +6086,7 @@ have r_proof x : HL f x > c%:E -> {r | (0 < r)%R & rewrite in_itv/= andbT => rg0 <-{y} Hc; exists r => //. rewrite -(@fineK _ (mu (ball x r))) ?ge0_fin_numE//; last first. by rewrite lebesgue_measure_ball ?ltry// ltW. - rewrite -lte_pdivl_mulr// 1?muleC// fine_gt0//. + rewrite -lte_pdivlMr// 1?muleC// fine_gt0//. by rewrite lebesgue_measure_ball 1?ltW// ltry lte_fin mulrn_wgt0. rewrite lebesgue_regularity_inner_sup//; last first. rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. @@ -6127,7 +6127,7 @@ rewrite !EFinM -muleA lee_wpmul2l//=. apply: (@le_trans _ _ (\sum_(i <- E) c^-1%:E * \int[mu]_(y in B i) `|(f y)|%:E)). rewrite [in leLHS]big_seq [in leRHS]big_seq; apply: lee_sum => r /ED /Dsub /[!inE] rD. - by rewrite -lee_pdivr_mull ?invr_gt0// invrK /B/=; exact/ltW/cMfx_int. + by rewrite -lee_pdivrMl ?invr_gt0// invrK /B/=; exact/ltW/cMfx_int. rewrite -ge0_sume_distrr//; last by move=> x _; rewrite integral_ge0. rewrite lee_wpmul2l//; first by rewrite lee_fin invr_ge0 ltW. rewrite -ge0_integral_bigsetU//=. @@ -6220,7 +6220,7 @@ near=> t. have [t0|t0] := leP t 0%R; first by rewrite /= davg0//= subrr normr0 ltW. rewrite sub0r normrN /= ger0_norm; last by rewrite fine_ge0// davg_ge0. rewrite -lee_fin fineK//; last by rewrite dfx//= sub0r normrN gtr0_norm. -rewrite /davg/= /iavg/= lee_pdivr_mull//; last first. +rewrite /davg/= /iavg/= lee_pdivrMl//; last first. by rewrite fine_gt0// lebesgue_measure_ball// ?ltry ?lte_fin ?mulrn_wgt0 ?ltW. rewrite (@le_trans _ _ (\int[mu]_(y in ball x t) e%:E))//. apply: ge0_le_integral => //=. @@ -6577,7 +6577,7 @@ have HL_null n : mu (HLf_g_Be n) <= (3%:R / (e / 2))%:E * n.+1%:R^-1%:E. by rewrite indicE; case: (_ \in _) => /=; rewrite !(mulr1, mulr0). have fgn_null n : mu [set x | `|(f_ k \- g_B n) x|%:E >= (e / 2)%:E] <= (e / 2)^-1%:E * n.+1%:R^-1%:E. - rewrite lee_pdivl_mull ?invr_gt0 ?divr_gt0// -[X in mu X]setTI. + rewrite lee_pdivlMl ?invr_gt0 ?divr_gt0// -[X in mu X]setTI. apply: le_trans. apply: (@le_integral_comp_abse _ _ _ mu _ measurableT (EFin \o (f_ k \- g_B n)%R) (e / 2) id) => //=. @@ -6606,7 +6606,7 @@ rewrite (@le_trans _ _ ((4 / (e / 2))%:E * n.+1%:R^-1%:E))//. apply: le_trans; first by apply: leeD; [exact: HL_null|exact: fgn_null]. rewrite -muleDl// lee_pmul2r// -EFinD lee_fin -{2}(mul1r (_^-1)) -div1r. by rewrite -mulrDl natr1. -rewrite -lee_pdivl_mull ?divr_gt0// -EFinM lee_fin -(@invrK _ r). +rewrite -lee_pdivlMl ?divr_gt0// -EFinM lee_fin -(@invrK _ r). rewrite -invrM ?unitfE ?gt_eqF ?invr_gt0 ?divr_gt0//. rewrite lef_pV2 ?posrE ?mulr_gt0 ?invr_gt0 ?divr_gt0//. by rewrite -(@natr1 _ n) -lerBlDr; near: n; exact: nbhs_infty_ger. @@ -6773,7 +6773,7 @@ Lemma nicely_shrinking_gt0 x E : nicely_shrinking x E -> forall n, (0 < mu (E n))%E. Proof. move=> [mE [[C r_]]] [/= C_gt0 _ _ + ] n => /(_ n). -rewrite lebesgue_measure_ball// -lee_pdivr_mull//. +rewrite lebesgue_measure_ball// -lee_pdivrMl//. apply: lt_le_trans. by rewrite mule_gt0// lte_fin invr_gt0. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 8f8c3d2d2..204e2dcb7 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2392,7 +2392,7 @@ have {}ZNF5 : mu (Z r%:num) <= + apply: bigcup_measurable => k _; case: ifPn => // _. by apply: measurable_closure; exact: is_scale_ball. apply/(le_trans ZNF5). -move/ltW: F5e; rewrite [in X in X -> _](@lee_pdivl_mull R 5%:R) ?ltr0n//. +move/ltW: F5e; rewrite [in X in X -> _](@lee_pdivlMl R 5%:R) ?ltr0n//. rewrite -nneseriesZl//; last by move=> *; exact: esum_ge0. apply: le_trans; apply: lee_nneseries => //; first by move=> *; exact: esum_ge0. move=> n _. diff --git a/theories/normedtype.v b/theories/normedtype.v index 365b3c9fa..6b5b67271 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2941,10 +2941,10 @@ move=> [s||]/=. by apply: near_fun => //=; apply: continuousM => //=; apply: cvg_cst. - rewrite gt0_muley ?lte_fin// => A [u [realu uA]]. exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW. - by move=> x rux; apply: uA; move: rux; rewrite EFinM lte_pdivr_mull. + by move=> x rux; apply: uA; move: rux; rewrite EFinM lte_pdivrMl. - rewrite gt0_muleNy ?lte_fin// => A [u [realu uA]]. exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW. - by move=> x xru; apply: uA; move: xru; rewrite EFinM lte_pdivl_mull. + by move=> x xru; apply: uA; move: xru; rewrite EFinM lte_pdivlMl. Unshelve. all: by end_near. Qed. Lemma cvgeMl f x y : y \is a fin_num -> @@ -2981,7 +2981,7 @@ Proof. move=> b_gt0 /cvgeyPge foo /fine_cvgP[gfin gb]; apply/cvgeyPgey. near (0%R : R)^'+ => e; near=> A; near=> n. rewrite (@le_trans _ _ (f n * e%:E))// ?lee_pmul// ?lee_fin//. -- by rewrite -lee_pdivr_mulr ?divr_gt0//; near: n; apply: foo. +- by rewrite -lee_pdivrMr ?divr_gt0//; near: n; apply: foo. - by rewrite (@le_trans _ _ 1) ?lee_fin//; near: n; apply: foo. rewrite -(@fineK _ (g n)) ?lee_fin; last by near: n; exact: gfin. by near: n; apply: (cvgr_ge b). @@ -2993,7 +2993,7 @@ Proof. move=> b0 /cvgeyPge foo /fine_cvgP -[gfin gb]; apply/cvgeNyPleNy. near (0%R : R)^'+ => e; near=> A; near=> n. rewrite -leeN2 -muleN (@le_trans _ _ (f n * e%:E))//. - by rewrite -lee_pdivr_mulr ?mulr_gt0 ?oppr_gt0//; near: n; apply: foo. + by rewrite -lee_pdivrMr ?mulr_gt0 ?oppr_gt0//; near: n; apply: foo. rewrite lee_pmul ?lee_fin//. by rewrite (@le_trans _ _ 1) ?lee_fin//; near: n; apply: foo. rewrite -(@fineK _ (g n)) ?lee_fin; last by near: n; exact: gfin. @@ -3270,7 +3270,7 @@ have : (edist (x, y) <= (eps%:num / 2)%:E)%E. apply: ereal_inf_lb; exists (eps%:num / 2) => //; split => //. exact: (bxy (eps%:num / 2)%:pos). apply: contra_leP => _. -by rewrite /= EFinM fineK// lte_pdivr_mulr// lte_pmulr// lte1n. +by rewrite /= EFinM fineK// lte_pdivrMr// lte_pmulr// lte1n. Qed. Lemma edist_refl x : edist (x, x) = 0%E. Proof. exact/edist_closeP. Qed. diff --git a/theories/probability.v b/theories/probability.v index 576b95ccb..0ba7a79ab 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -558,7 +558,7 @@ move=> t0. rewrite /mmt_gen_fun; have -> : expR \o r \o* X = (normr \o normr) \o [the {mfun T >-> R} of expR \o r \o* X]. by apply: funext => t /=; rewrite normr_id ger0_norm ?expR_ge0. -rewrite expRN lee_pdivl_mulr ?expR_gt0//. +rewrite expRN lee_pdivlMr ?expR_gt0//. rewrite (le_trans _ (markov _ (expR_gt0 (r * a)) _ _ _))//; last first. exact: (monoW_in (@ger0_le_norm _)). rewrite ger0_norm ?expR_ge0// muleC lee_pmul2l// ?lte_fin ?expR_gt0//. @@ -573,7 +573,7 @@ move => heps; have [->|hv] := eqVneq 'V_P[X] +oo. by rewrite mulr_infty gtr0_sg ?mul1e// ?leey// invr_gt0// exprn_gt0. have h (Y : {RV P >-> R}) : P [set x | (eps <= `|Y x|)%R] <= (eps ^- 2)%:E * 'E_P[Y ^+ 2]. - rewrite -lee_pdivr_mull; last by rewrite invr_gt0// exprn_gt0. + rewrite -lee_pdivrMl; last by rewrite invr_gt0// exprn_gt0. rewrite exprnN expfV exprz_inv opprK -exprnP. apply: (@le_trans _ _ ('E_P[(@GRing.exp R ^~ 2%N \o normr) \o Y])). apply: (@markov Y (@GRing.exp R ^~ 2%N)) => //. @@ -658,7 +658,7 @@ have le (u : R) : (0 <= u)%R -> by apply/measurableT_comp => //; apply/measurable_funD. set eps := ((lambda + u) ^ 2)%R. have peps : (0 < eps)%R by rewrite exprz_gt0 ?ltr_wpDr. - rewrite (lee_pdivl_mulr _ _ peps) muleC. + rewrite (lee_pdivlMr _ _ peps) muleC. under eq_set => x. rewrite -[leRHS]gee0_abs ?lee_fin ?sqr_ge0 -?lee_fin => [|//]. rewrite -[(_ ^+ 2)%R]/(((Y \+ cst u) ^+ 2) x)%R; over.