From 17fd5f81943d2142502996d156f5d542942e9afe Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Mon, 16 Oct 2023 10:54:03 +0200 Subject: [PATCH 1/2] Adds measurable_expR and measurable function composition Measurable function composition only works in the specific case where `f` and `g` are maps to reals --- theories/lebesgue_integral.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 8eaa1ba7c..7f12a3350 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -155,6 +155,15 @@ Lemma mfun_cst x : @cst_mfun x =1 cst x. Proof. by []. Qed. HB.instance Definition _ := @isMeasurableFun.Build _ _ rT (@normr rT rT) (@measurable_normr rT setT). +HB.instance Definition _ := isMeasurableFun.Build _ _ rT + (@expR rT) (@measurable_expR rT). + +Let measurableT_comp_subproof (f : {mfun rT >-> rT}) (g : {mfun aT >-> rT}) : + measurable_fun setT (f \o g). +Proof. by apply: measurableT_comp; last apply: @measurable_funP _ _ _ g. Qed. + +HB.instance Definition _ (f : {mfun rT >-> rT}) (g : {mfun aT >-> rT}) := isMeasurableFun.Build _ _ _ (f \o g) (@measurableT_comp_subproof _ _). + End mfun. Section ring. From 45375483ea36df18d2ecce365f8bee198e90e018 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Mon, 16 Oct 2023 14:36:45 +0200 Subject: [PATCH 2/2] Generalizes measurable_comp to two real types --- theories/lebesgue_integral.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 7f12a3350..e6adb8d98 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -158,11 +158,11 @@ HB.instance Definition _ := @isMeasurableFun.Build _ _ rT HB.instance Definition _ := isMeasurableFun.Build _ _ rT (@expR rT) (@measurable_expR rT). -Let measurableT_comp_subproof (f : {mfun rT >-> rT}) (g : {mfun aT >-> rT}) : +Let measurableT_comp_subproof {rT' : realType} (f : {mfun rT >-> rT'}) (g : {mfun aT >-> rT}) : measurable_fun setT (f \o g). Proof. by apply: measurableT_comp; last apply: @measurable_funP _ _ _ g. Qed. -HB.instance Definition _ (f : {mfun rT >-> rT}) (g : {mfun aT >-> rT}) := isMeasurableFun.Build _ _ _ (f \o g) (@measurableT_comp_subproof _ _). +HB.instance Definition _ {rT' : realType} (f : {mfun rT >-> rT'}) (g : {mfun aT >-> rT}) := isMeasurableFun.Build _ _ _ (f \o g) (@measurableT_comp_subproof _ _ _). End mfun.