proposition: Lemma MeasureZeroAE : forall {IS : IntegrationSpace} (Z : X (ElemFunc IS) -> Prop) (zInt : IntegrableSet Z), MeasureSet zInt == 0 -> almost_everywhere (fun x => ~Z x).
proof: Proof. intros. destruct (IntegrableFunctionsComplete IS (fun _:nat => CharacFunc Z) (fun _ => zInt) 0) as [rep [p s]]. - apply (CR_cv_eq _ (fun _:nat => 0)). 2: apply CR_cv_const. intro n. rewrite sum_const. unfold MeasureSet in H. rewrite <- (CRmult_0_l (INR (S n))). apply CRmult_morph. 2: reflexivity. rewrite <- H. apply IntegralExtensional. intros. rewrite applyXabs. rewrite (DomainProp _ x xdf xdg). rewrite CRabs_right. reflexivity. simpl. destruct xdg. apply CRlt_asym, CRzero_lt_one. apply CRle_refl. - exists (XinfiniteSumAbs (IntFn rep)). split. + exists rep. apply PartialRestriction_refl. + intros x H0 abs. destruct p. specialize (d x H0) as [xn xncv]. apply CR_complete in xncv. destruct xncv as [l lcv]. apply (CR_cv_eq (fun n:nat => CR_of_Q _ (Z.of_nat (S n) # 1))) in lcv. specialize (lcv 1%positive) as [n ncv]. destruct (CRup_nat (1+l)) as [k kup]. specialize (ncv (max n k) (Nat.le_max_l _ _)). apply (CRle_trans _ _ _ (CRle_abs _)) in ncv. apply (CRplus_le_compat_r l) in ncv. unfold CRminus in ncv. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r in ncv. apply ncv. apply (CRlt_le_trans _ _ _ kup). apply CR_of_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. apply Nat2Z.inj_le, le_S, Nat.le_max_r. intro n. rewrite <- (CRsum_eq (fun _ => 1)). rewrite sum_const, CRmult_1_l. reflexivity. intros. simpl. destruct (xn i). rewrite CRabs_right. reflexivity. apply CRlt_asym, CRzero_lt_one. contradiction. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity