variants of existing lemmas

CHANGELOG_UNRELEASED.md

@@ -33,6 +33,11 @@
   + notation `^-1` in `relation_scope` (use to be a local notation)
   + lemma `set_prod_invK` (was a local lemma in `normedtype.v`)
   + definition `diagonal`, lemma `diagonalP`
+- in `mathcomp_extra.v`:
+  + lemmas `invf_ple`, `invf_lep`
+
+- in `lebesgue_integral.v`:
+  + lemma `integralZr`
 
 ### Changed
 

classical/mathcomp_extra.v

@@ -65,7 +65,19 @@ Qed.
 Lemma invf_ltp (F : numFieldType) :
   {in Num.pos &, forall x y : F, (x < y^-1)%R = (y < x^-1)%R}.
 Proof.
-by move=> x y ? ?; rewrite -[in RHS](@invrK _ y) ltf_pV2// posrE invr_gt0.
+by move=> x y ? ?; rewrite -(invrK x) invf_plt ?posrE ?invr_gt0// !invrK.
+Qed.
+
+Lemma invf_ple (F : numFieldType) :
+  {in Num.pos &, forall x y : F, (x^-1 <= y)%R = (y^-1 <= x)%R}.
+Proof.
+by move=> x y ? ?; rewrite -[in LHS](@invrK _ y) lef_pV2// posrE invr_gt0.
+Qed.
+
+Lemma invf_lep (F : numFieldType) :
+  {in Num.pos &, forall x y : F, (x <= y^-1)%R = (y <= x^-1)%R}.
+Proof.
+by move=> x y ? ?; rewrite -(invrK x) invf_ple ?posrE ?invr_gt0// !invrK.
 Qed.
 
 Definition proj {I} {T : I -> Type} i (f : forall i, T i) := f i.

theories/lebesgue_integral.v

@@ -3377,27 +3377,23 @@ Let mesf : measurable_fun D f. Proof. exact: measurable_int intf. Qed.
 Lemma integralZl r :
   \int[mu]_(x in D) (r%:E * f x) = r%:E * \int[mu]_(x in D) f x.
 Proof.
-have [r0|r0|->] := ltgtP r 0%R; last first.
-  by under eq_fun do rewrite mul0e; rewrite mul0e integral0.
-- rewrite [in LHS]integralE// gt0_funeposM// gt0_funenegM//.
-  rewrite (ge0_integralZl_EFin _ _ _ _ (ltW r0)) //; last first.
-    exact: measurable_funepos.
-  rewrite (ge0_integralZl_EFin _ _ _ _ (ltW r0)) //; last first.
-    exact: measurable_funeneg.
-  rewrite -muleBr 1?[in RHS]integralE//.
-  exact: integrable_add_def.
+have [r0|r0|->] := ltgtP r 0%R.
 - rewrite [in LHS]integralE// lt0_funeposM// lt0_funenegM//.
-  rewrite ge0_integralZl_EFin //; last 2 first.
-    + exact: measurable_funeneg.
-    + by rewrite -lerNr oppr0 ltW.
-  rewrite ge0_integralZl_EFin //; last 2 first.
-    + exact: measurable_funepos.
-    + by rewrite -lerNr oppr0 ltW.
-  rewrite -mulNe -EFinN opprK addeC EFinN mulNe -muleBr //; last first.
-    exact: integrable_add_def.
+  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funeneg _)) ?oppr_ge0 ?ltW//.
+  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funepos _)) ?oppr_ge0 ?ltW//.
+  rewrite !EFinN addeC !mulNe oppeK -muleBr ?integrable_add_def//.
   by rewrite [in RHS]integralE.
+- rewrite [in LHS]integralE// gt0_funeposM// gt0_funenegM//.
+  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funepos _) (ltW r0))//.
+  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funeneg _) (ltW r0))//.
+  by rewrite -muleBr 1?[in RHS]integralE// integrable_add_def.
+- by under eq_fun do rewrite mul0e; rewrite mul0e integral0.
 Qed.
 
+Lemma integralZr r :
+  \int[mu]_(x in D) (f x * r%:E) = (\int[mu]_(x in D) f x) * r%:E.
+Proof. by rewrite muleC -integralZl; under eq_integral do rewrite muleC. Qed.
+
 End linearityZ.
 #[deprecated(since="mathcomp-analysis 0.6.4", note="use `integralZl` instead")]
 Notation integralM := integralZl (only parsing).

theories/probability.v

@@ -159,10 +159,7 @@ Qed.
 
 Lemma expectationM (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X))
   (k : R) : 'E_P[k \o* X] = k%:E * 'E_P [X].
-Proof.
-rewrite unlock; under eq_integral do rewrite EFinM.
-by rewrite -integralZl//; under eq_integral do rewrite muleC.
-Qed.
+Proof. by rewrite unlock muleC -integralZr. Qed.
 
 Lemma expectation_ge0 (X : {RV P >-> R}) :
   (forall x, 0 <= X x)%R -> 0 <= 'E_P[X].