proposition: Lemma MeasurableSetEquiv : forall {IS : IntegrationSpace} (A : (X (ElemFunc IS)) -> Prop), prod (MeasurableSet A -> (forall B : (X (ElemFunc IS)) -> Prop, IntegrableSet B -> IntegrableFunction (Xmult (CharacFunc A) (CharacFunc B)))) ((forall B : (X (ElemFunc IS)) -> Prop, IntegrableSet B -> IntegrableFunction (Xmult (CharacFunc A) (CharacFunc B))) -> MeasurableSet A).
proof: Proof. intros IS A. assert (forall B x xD xG k, partialApply (Xmult (CharacFunc A) (CharacFunc B)) x xD == partialApply (XmaxConst (XminConst (Xmult (CharacFunc B) (CharacFunc A)) (CR_of_Q (RealT (ElemFunc IS)) (Z.pos k # 1))) (CR_of_Q (RealT (ElemFunc IS)) (Z.neg k # 1))) x xG). { intros. rewrite applyXmaxConst, CRmax_left. rewrite applyXminConst, CRmin_left. destruct xD, xG. simpl. destruct d. destruct d2. 2: contradiction. destruct d0. destruct d1. 2: contradiction. reflexivity. destruct d1. contradiction. apply CRmult_comm. rewrite CRmult_0_l. destruct d2. contradiction. rewrite CRmult_0_r. reflexivity. apply (CRle_trans _ 1). simpl. destruct xG. destruct d. destruct d0. rewrite CRmult_1_l. apply CRle_refl. rewrite CRmult_1_l. apply CRlt_asym, CRzero_lt_one. rewrite CRmult_0_l. apply CRlt_asym, CRzero_lt_one. apply CR_of_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_r. destruct k; discriminate. apply (CRle_trans _ 0). apply CR_of_Q_le. discriminate. apply CRmin_glb. simpl. destruct xG, d. rewrite CRmult_1_l. destruct d0. apply CRlt_asym, CRzero_lt_one. apply CRle_refl. rewrite CRmult_0_l. apply CRle_refl. apply CR_of_Q_le. discriminate. } split. - intros Ames B Bint. specialize (Ames B 1%positive Bint). refine (IntegrableFunctionExtensional _ _ _ Ames). split. + intros x xdf. destruct xdf. split. exact d0. exact d. + intros x xD xG. symmetry. apply H. - intros H0 B k Bint. specialize (H0 B Bint). refine (IntegrableFunctionExtensional _ _ _ H0). split. + intros x xdf. destruct xdf. split. exact d0. exact d. + intros x xD xG. apply H. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile