proposition: Lemma IntegralSupportExists : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (eps : CRcarrier (RealT (ElemFunc IS))), 0 < eps -> { t : CRcarrier _ & prod (t < eps) (IntegralSupport f fInt (fun x => exists xD:Domain (Xabs f) x, t <= partialApply (Xabs f) x xD) eps) }.
proof: Proof. intros. pose proof (InverseImageIntegrableAE (Xabs f) (IntegrableAbs fInt)) as [jumps invIm]. pose proof (Un_cv_nat_real _ _ (IntegralTruncateLimitZero f fInt) eps H) as [n nmaj]. pose proof (CRuncountable jumps 0 _ (CRmin_lt _ _ _ (invSuccRealPositive n) H)) as [t [[tpos tmin] tcont]]. specialize (invIm t tpos tcont) as [invIm _]. exists t. split. apply (CRlt_le_trans _ _ _ tmin). apply CRmin_r. exists invIm. specialize (nmaj n (Nat.le_refl n)). refine (CRle_lt_trans _ _ _ _ nmaj). unfold CRminus. rewrite CRopp_0, CRplus_0_r, CRabs_right. apply IntegralNonDecreasing. intros x xdf xdg. destruct xdf, d0, d0. - apply (CRle_trans _ 0). simpl. rewrite CRmult_1_l. rewrite <- CRopp_mult_distr_l, CRmult_1_l, (DomainProp f x d1 d). rewrite CRplus_opp_r, CRabs_right. apply CRle_refl. apply CRle_refl. simpl. apply CRmin_glb. apply CRabs_pos. apply CR_of_Q_le. discriminate. - apply (CRle_trans _ (CRabs _ (partialApply f x d))). simpl. rewrite CRmult_0_l, CRmult_0_r, CRplus_0_r. apply CRle_refl. assert (CRabs _ (partialApply f x d) <= t). { intro abs. contradict n0. exists d. apply CRlt_asym, abs. } clear n0. apply CRmin_glb. rewrite applyXabs, (DomainProp f x xdg d). apply CRle_refl. apply (CRle_trans _ _ _ H0). apply CRlt_asym. apply (CRlt_le_trans _ _ _ tmin). apply CRmin_l. - apply IntegralNonNeg. intros x xdf. apply CRmin_glb. apply CRabs_pos. apply CR_of_Q_le. discriminate. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile