proposition: Lemma IntegrableApproxSequenceBound : forall {IS : IntegrationSpace} (gen : IntegrableSetsGen IS) (A : X (ElemFunc IS) -> Prop) (Aint : IntegrableSet A) (n : nat) (Uint : IntegrableSet (let (U,_) := IntegrableApproxSequence gen A Aint n in U)), MeasureSet Aint - MeasureSet Uint < CRpow (CR_of_Q _ (1#2)) n.
proof: Proof. intros. destruct n. - simpl. simpl in Uint. destruct (gen A Aint 1 (CRzero_lt_one (RealT (ElemFunc IS)))). apply (CRle_lt_trans _ (MeasureSet Aint - MeasureSet sa_bint0)). apply CRplus_le_compat_l, CRopp_ge_le_contravar. apply MeasureNonDecreasing. intros. exact H. exact sa_mes0. - simpl. pose proof (IntegrableApproxSequenceInc gen A Aint n) as Uinc. simpl in Uint; destruct (IntegrableApproxSequence gen A Aint n) as [U Vint]. apply (CRle_lt_trans _ (MeasureSet (IntegrableSetDifference A U Aint Vint) - MeasureSet (sa_bint _ _ _ (gen (fun x0 : X (ElemFunc IS) => A x0 /\ ~ U x0) (IntegrableSetDifference A U Aint Vint) (CR_of_Q (RealT (ElemFunc IS)) (1 # 2) * CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) n) (CRpow_gt_zero (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) (S n) (CR_of_Q_pos (1 # 2) eq_refl)))))). 2: apply sa_mes. rewrite <- MeasureDifferenceIncluded, <- MeasureDifferenceIncluded. apply MeasureNonDecreasing. intros. destruct H. split. split. exact H. intro abs. apply H0. left. exact abs. intro abs. apply H0. right. exact abs. intros. exact (sa_inc _ _ _ _ x H). intros. destruct H. 2: exact (proj1 (sa_inc _ _ _ _ x H)). apply Uinc, H. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile