proposition: Lemma PositiveMeasureSubsetExists : forall (IS : IntegrationSpace), @PositiveMeasureSubset IS.
proof: Proof. intro IS. destruct (@IoneValSplit IS) as [[n k] H]. unfold fst, snd in H. assert (1 # Pos.of_nat (S k) < Z.of_nat (2 + n) # 1)%Q. { unfold Qlt, Qnum, Qden. rewrite Z.mul_1_l. apply (Z.lt_le_trans _ (Z.of_nat (2+n)*1)). rewrite Z.mul_1_r. replace 1%Z with (Z.of_nat 1). apply Nat2Z.inj_lt. apply le_n_S, le_n_S, Nat.le_0_l. reflexivity. apply Z.mul_le_mono_nonneg_l. discriminate. apply Pos2Z.pos_le_pos. apply Pos.le_1_l. } pose proof (InverseImageIntegrableAE (Xabs (Ione IS)) (IntegrableL _ (LabsStable _ _ (IoneL IS)))) as [s sint]. assert (0 < CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S k)) < INR (2 + n)). { split. apply CR_of_Q_pos. reflexivity. apply CR_of_Q_lt. exact H0. } destruct (CRuncountable s 0 (CR_of_Q _ (1 # Pos.of_nat (S k))) (fst H1)) as [t tap]. destruct tap. specialize (sint t (fst p) c). destruct sint. assert (0 < MeasureSet x). { apply (CRlt_le_trans _ (Integral (StepApproxIntegrable (Xabs (Ione IS)) (CR_of_Q _ (1 # Pos.of_nat (S k))) (INR (2 + n)) H1 (IntegrableL _ (LabsStable _ _ (IoneL IS)))))). unfold StepApproxIntegrable. rewrite (IntegralScale (Xminus (XminConst (Xabs (Ione IS)) (INR (2 + n))) (XminConst (Xabs (Ione IS)) (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S k))))) _ (CRinv (RealT (ElemFunc IS)) (INR (2 + n) - CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S k))) (inr (CRlt_minus (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S k))) (INR (2 + n)) (snd H1)))) ). apply CRmult_lt_0_compat. rewrite IntegralMinus. apply CRlt_minus. apply (CRle_lt_trans _ (Integral (IntegrableL _ (LminConstStable (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S k))) (Xabs (Ione IS)) (invSuccRealPositive k) (LabsStable (ElemFunc IS) (Ione IS) (IoneL IS)))))). apply IntegralNonDecreasing. intros y ydf ydg. rewrite (DomainProp _ y ydf ydg). apply CRle_refl. rewrite IntegralLstable. apply (CRlt_le_trans _ _ _ H). apply (CRle_trans _ (Integral (IntegrableL _ (LminIntStable (2 + n) (Xabs (Ione IS)) (LabsStable (ElemFunc IS) (Ione IS) (IoneL IS)))))). rewrite IntegralLstable. apply CRle_refl. apply IntegralNonDecreasing. intros y ydf ydg. rewrite (DomainProp _ y ydf ydg). apply CRle_refl. apply CRinv_0_lt_compat, CRlt_minus, CR_of_Q_lt. exact H0. apply IntegralNonDecreasing. intros y ydf ydg. simpl ( partialApply (CharacFunc (fun x0 : X (ElemFunc IS) => exists xD : Domain (Xabs (Ione IS)) x0, t <= partialApply (Xabs (Ione IS)) x0 xD)) y ydg). destruct ydg. - unfold StepApprox. rewrite applyXscale. destruct ydf. rewrite (applyXminus _ (XminConst (Xabs (Ione IS)) (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S k))))). do 2 rewrite applyXminConst. rewrite (DomainProp (Xabs (Ione IS)) y d0 d). apply StepApproxMax. apply CRlt_asym, CR_of_Q_lt. exact H0. - destruct (CRltLinear (RealT (ElemFunc IS))). destruct ydf. destruct (s0 t (partialApply (Xabs (Ione IS)) y d0) (CR_of_Q _ (1 # Pos.of_nat (S k))) (snd p)). exfalso. apply n0. exists d0. apply CRlt_asym, c1. unfold StepApprox. rewrite applyXscale. apply (CRmult_le_reg_l (INR (2 + n) - CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S k)))). apply CRlt_minus, CR_of_Q_lt. exact H0. rewrite <- CRmult_assoc, CRinv_r, CRmult_0_r, CRmult_1_l. rewrite (applyXminus _ (XminConst (Xabs (Ione IS)) (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S k))))). do 2 rewrite applyXminConst. rewrite (DomainProp (Xabs (Ione IS)) y d d0). unfold CRminus. rewrite CRmin_left, CRmin_left, CRplus_opp_r. apply CRle_refl. apply CRlt_asym, c1. apply CRlt_asym. apply (CRlt_trans _ _ _ c1). apply CR_of_Q_lt. exact H0. } exact (Build_PositiveMeasureSubset IS _ x H2). Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia