Skip to content

Commit

Permalink
fixes #1241
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Jun 16, 2024
1 parent 9c311a9 commit e65a7a2
Show file tree
Hide file tree
Showing 7 changed files with 112 additions and 59 deletions.
19 changes: 19 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
104 changes: 69 additions & 35 deletions theories/constructive_ereal.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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.

Expand Down
8 changes: 4 additions & 4 deletions theories/hoelder.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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).
Expand Down
22 changes: 11 additions & 11 deletions theories/lebesgue_integral.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 => //.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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//.
Expand All @@ -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.
Expand Down Expand Up @@ -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 => //.
Expand Down Expand Up @@ -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//=.
Expand Down Expand Up @@ -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 => //=.
Expand Down Expand Up @@ -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) => //=.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion theories/lebesgue_measure.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 _.
Expand Down
10 changes: 5 additions & 5 deletions theories/normedtype.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down Expand Up @@ -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).
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand Down
Loading

0 comments on commit e65a7a2

Please sign in to comment.