From b66a9ae8233ed88090abdb801feac8569b606f69 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 24 Aug 2024 12:17:13 +0900 Subject: [PATCH] addressing comments --- theories/lebesgue_integral.v | 4 ++-- theories/probability.v | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 9f6f518d75..7c7f88912c 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3391,8 +3391,8 @@ have [r0|r0|->] := ltgtP r 0%R. Qed. Lemma integralZr r : - \int[mu]_(x in D) (f x * r%:E) = r%:E * \int[mu]_(x in D) f x. -Proof. by rewrite -integralZl; under eq_integral do rewrite muleC. Qed. + \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")] diff --git a/theories/probability.v b/theories/probability.v index 37aed52156..3a6c382614 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -159,7 +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. by rewrite unlock -integralZr. 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].