proposition: Lemma IntegrableApproxSequenceLimit : forall {IS : IntegrationSpace} (gen : IntegrableSetsGen IS) (A : X (ElemFunc IS) -> Prop) (Aint : IntegrableSet A), { intUnion : IntegrableSet (fun x => exists n:nat, let (U,_) := IntegrableApproxSequence gen A Aint n in U x) | MeasureSet intUnion == MeasureSet Aint }.
proof: Proof. intros. assert (forall n:nat, IntegrableSet (fun x => let (U, _) := IntegrableApproxSequence gen A Aint n in U x)) as seqInt. { intro n. destruct (IntegrableApproxSequence gen A Aint n). exact i. } apply (IntegrableSetCountableUnion (fun n x => let (U,_) := IntegrableApproxSequence gen A Aint n in U x) seqInt (MeasureSet Aint)). intro p. pose proof (@GeoCvZero (RealT (ElemFunc IS)) p) as [n ncv]. exists n. intros i H. rewrite CRabs_minus_sym, CRabs_right. - apply (CRle_trans _ (MeasureSet Aint - MeasureSet (seqInt i))). apply CRplus_le_compat_l, CRopp_ge_le_contravar. apply MeasureNonDecreasing. intros. apply applyUnionIterate. exists i. exact (conj (Nat.le_refl i) H0). specialize (ncv i H). apply (CRle_trans _ (CRpow (CR_of_Q _ (1#2)) i)). generalize (seqInt i). intro iint. pose proof (IntegrableApproxSequenceBound gen A Aint i). destruct (IntegrableApproxSequence gen A Aint i). apply CRlt_asym, X. unfold CRminus in ncv. rewrite CRopp_0, CRplus_0_r, CRabs_right in ncv. exact ncv. apply CRpow_ge_zero. apply CR_of_Q_le. discriminate. - rewrite <- (CRplus_opp_r (MeasureSet Aint)). apply CRplus_le_compat_l, CRopp_ge_le_contravar. apply MeasureNonDecreasing. intros. apply applyUnionIterate in H0. destruct H0, H0. pose proof (IntegrableApproxSequenceInc gen A Aint x0 x). destruct (IntegrableApproxSequence gen A Aint x0). exact (H2 H1). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile