From 8e83e633e24d3f7e695a88075137d6ddd1f3a1ce Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 9 Aug 2024 11:25:40 +0900 Subject: [PATCH 1/2] variants of existing lemmas --- CHANGELOG_UNRELEASED.md | 5 +++++ classical/mathcomp_extra.v | 14 +++++++++++++- theories/lebesgue_integral.v | 30 +++++++++++++----------------- theories/probability.v | 5 +---- 4 files changed, 32 insertions(+), 22 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8f3b16bda..e461b086a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 45c0e6906..249bf6fa4 100644 --- a/classical/mathcomp_extra.v +++ b/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. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 85b334b50..74eec1c41 100644 --- a/theories/lebesgue_integral.v +++ b/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) = r%:E * \int[mu]_(x in D) f x. +Proof. by rewrite -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). diff --git a/theories/probability.v b/theories/probability.v index 8101fb0ac..37aed5215 100644 --- a/theories/probability.v +++ b/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 -integralZr. Qed. Lemma expectation_ge0 (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> 0 <= 'E_P[X]. From d10b87013063007b3c974a0fdef669bf12b7d74b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 24 Aug 2024 12:17:13 +0900 Subject: [PATCH 2/2] 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 74eec1c41..c406e7ad4 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 37aed5215..3a6c38261 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].