proposition: Lemma PositiveMeasureInhabited : forall {IS : IntegrationSpace} (A : X (ElemFunc IS) -> Prop) (aInt : IntegrableSet A), 0 < MeasureSet aInt -> { x : X (ElemFunc IS) | A x }.
proof: Proof. intros. destruct aInt. destruct (splitIntegralSumPosNeg (IntFn x) (IntFnL x) (IntAbsSum x) (IntAbsSumCv x)), s, p0, p0. assert (series_cv (fun k : nat => Iabs (XposPart (IntFn x k)) (LposPartStable (IntFn x k) (IntFnL x k))) x0). { apply (series_cv_eq (fun n0 : nat => I IS (XposPart (IntFn x n0)) (LposPartStable (IntFn x n0) (IntFnL x n0)))). 2: exact s0. intro n. apply IExtensional. intros. rewrite applyXabs, CRabs_right, (DomainProp _ x2 xF y). reflexivity. apply applyXposPartNonNeg. } destruct (IntegrableContinuous (XinfiniteSumAbs (fun n : nat => XposPart (IntFn x n))) (fun n => XnegPart (IntFn x n)) (existT _ (Build_IntegralRepresentation IS (fun n => XposPart (IntFn x n)) (fun n => LposPartStable _ (IntFnL x n)) x0 H0) (pair (fun y yD => yD) (fun x2 xD xG => DomainProp _ x2 xD xG))) (fun n => IntegrableL _ (LnegPartStable (IntFn x n) (IntFnL x n)))). - intro n. apply applyXnegPartNonNeg. - exists x1. split. apply (series_cv_eq (fun n0 : nat => I IS (XnegPart (IntFn x n0)) (LnegPartStable (IntFn x n0) (IntFnL x n0)))). 2: exact s1. intro n. rewrite IntegralLstable. reflexivity. unfold Integral. apply (CRlt_le_trans _ x0). apply (CRplus_lt_reg_r (-x1)). rewrite CRplus_opp_r. pose proof (IntegralCv x). setoid_replace (x0 + - x1) with (IntegralSeries x). exact H. apply (series_cv_unique (fun n : nat => I IS (IntFn x n) (IntFnL x n))). 2: exact H1. unfold CRminus in s. exact s. unfold IntegralSeries. destruct (series_cv_maj _ _ x0 (fun n : nat => integralAbsMaj (XposPart (IntFn x n)) (LposPartStable (IntFn x n) (IntFnL x n))) H0), p0. setoid_replace x0 with x2. apply CRle_refl. apply (series_cv_unique (fun k : nat => Iabs (XposPart (IntFn x k)) (LposPartStable (IntFn x k) (IntFnL x k))) _ _ H0). apply (series_cv_eq (fun n : nat => I IS (XposPart (IntFn x n)) (LposPartStable (IntFn x n) (IntFnL x n)))). 2: exact s2. intro n. apply IExtensional. intros. rewrite applyXabs, CRabs_right. apply DomainProp. apply applyXposPartNonNeg. - clear H. destruct x2; unfold ConstructivePartialFunctions.cpx, ConstructivePartialFunctions.cpxF, ConstructivePartialFunctions.cpxFn in s2. exists cpx. destruct s2, p0, p. assert (Domain (XinfiniteSumAbs (IntFn x)) cpx). { apply (domainXinfinitePosNeg _ _ cpxF). exists cpxFn. apply (Rcv_cauchy_mod _ x2). apply (series_cv_eq (fun n : nat => partialApply (XnegPart (IntFn x n)) cpx (cpxFn n))). 2: exact s2. intro n. rewrite CRabs_right. reflexivity. apply applyXnegPartNonNeg. } pose proof (c0 cpx H (d _ H)). simpl (partialApply (CharacFunc A) cpx (d cpx H)) in H1. destruct (d cpx H). exact a. exfalso. clear n. apply applyInfiniteSumAbs in H1. pose proof (series_cv_unique _ 0 (partialApply (XinfiniteSumAbs (fun n : nat => XposPart (IntFn x n))) cpx cpxF-x2) H1). clear H1. apply CRlt_minus in c. destruct H2. 2: contradiction. destruct cpxF. apply (series_cv_eq (fun n : nat => partialApply (XposPart (IntFn x n)) cpx (x3 n) - partialApply (XnegPart (IntFn x n)) cpx (cpxFn n))). intro n. apply SplitPosNegParts. apply series_cv_minus. 2: exact s2. apply (series_cv_eq (fun n => partialApply (XposPart (IntFn x n)) cpx (domainInfiniteSumAbsIncReverse _ cpx (existT _ x3 c1) n))). intro n. apply DomainProp. apply applyInfiniteSumAbs. reflexivity. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity