From 1af3ad14fb572e3f89e1791a79a43184ba51a3ed Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 7 Jul 2022 22:02:34 +0200 Subject: [PATCH] Circumvented the `measurableTypeR rT` problem but stack overflowed --- theories/lebesgue_integral.v | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 107ed925de..b0a9fb00bc 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -325,14 +325,14 @@ HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). -Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D. +Definition mindic (D : set aT) of measurable D : aT -> measurableTypeR rT := \1_D. Lemma mindicE (D : set aT) (mD : measurable D) : mindic mD = (fun x => (x \in D)%:R). Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. HB.instance Definition _ (D : set aT) (mD : measurable D) : - @FImFun aT rT (mindic mD) := FImFun.on (mindic mD). + @FImFun aT (measurableTypeR rT) (mindic mD) := FImFun.on (mindic mD). Lemma indic_mfun_subproof (D : set aT) (mD : measurable D) : - @isMeasurableFun d _ aT rT (mindic mD). + @isMeasurableFun d _ aT (measurableTypeR rT) (mindic mD). Proof. split=> mA /= B mB; rewrite preimage_indic. case: ifPn => B1; case: ifPn => B0 //. @@ -341,10 +341,10 @@ case: ifPn => B1; case: ifPn => B0 //. - by apply: measurableI => //; apply: measurableC. - by rewrite setI0. Qed. -HB.instance Definition _ D mD := @indic_mfun_subproof D mD. +HB.instance Definition _ D mD := @indic_mfun_subproof D mD. (* FIXME: remove measurableTypeR here? *) Definition indic_mfun (D : set aT) (mD : measurable D) := - [the {mfun aT >-> rT} of mindic mD]. + [the {mfun aT >-> (measurableTypeR rT)} of mindic mD]. HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_mfun k). Definition scale_mfun k f := [the {mfun aT >-> rT} of k \o* f]. @@ -352,14 +352,14 @@ Definition scale_mfun k f := [the {mfun aT >-> rT} of k \o* f]. Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g). Proof. by split; apply: measurable_maxr. Qed. HB.instance Definition _ f g := max_mfun_subproof f g. -Definition max_mfun f g := [the {mfun aT >-> _} of f \max g]. +Definition max_mfun f g := [the {mfun aT >-> rT} of f \max g]. End ring. Arguments indic_mfun {d aT rT} _. Lemma measurable_indic d (T : measurableType d) (R : realType) (D A : set T) : measurable A -> - measurable_fun D (\1_A : T -> R). + measurable_fun D (\1_A : T -> (measurableTypeR R)). Proof. by move=> mA; apply/measurable_funTS; rewrite (_ : \1__ = mindic R mA). Qed. @@ -398,12 +398,12 @@ End sfun_pred. Section sfun. Context {d} {aT : measurableType d} {rT : realType}. -Notation T := {sfun aT >-> rT}. -Notation sfun := (@sfun _ aT rT). +Notation T := {sfun aT >-> (measurableTypeR rT)}. +Notation sfun := (@sfun _ aT (measurableTypeR rT)). Section Sub. -Context (f : aT -> rT) (fP : f \in sfun). +Context (f : aT -> measurableTypeR rT) (fP : f \in sfun). Definition sfun_Sub1_subproof := - @isMeasurableFun.Build d _ aT rT f (set_mem (sub_sfun_mfun fP)). + @isMeasurableFun.Build d _ aT (measurableTypeR rT) f (set_mem (sub_sfun_mfun fP)). #[local] HB.instance Definition _ := sfun_Sub1_subproof. Definition sfun_Sub2_subproof := @FiniteImage.Build aT rT f (set_mem (sub_sfun_fimfun fP)).