proposition: Lemma RealSequenceCoverMeasure : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (N : nat), { coverInt : @IntegrableSet IntSpaceCSUCFunctions (fun x => exists n:nat, CRltProp R (un n - CRpow (CR_of_Q R (1#2)) (2 + N + n)) x /\ CRltProp R x (un n + CRpow (CR_of_Q R (1#2)) (2 + N + n))) & MeasureSet coverInt <= CRpow (CR_of_Q R (1#2)) N }.
proof: Proof. intros. assert (forall n:nat, un n - CRpow (CR_of_Q R (1#2)) (2 + N + n) < un n + CRpow (CR_of_Q R (1#2)) (2 + N + n)). { intro n. apply CRplus_lt_compat_l. apply (CRle_lt_trans _ 0). rewrite <- CRopp_0. apply CRopp_ge_le_contravar. apply CRpow_ge_zero, CRlt_asym, CR_of_Q_pos. reflexivity. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. } pose (fun n:nat => OpenIntervalIntegrable _ _ (H n)) as openInt. destruct (@IntegrableSetCountableUnionLe IntSpaceCSUCFunctions (fun n x => CRltProp R (un n - CRpow (CR_of_Q _ (1#2)) (2 + N + n)) x /\ CRltProp R x (un n + CRpow (CR_of_Q _ (1#2)) (2 + N + n))) (fun n => let (i,_) := openInt n in i) (CRpow (CR_of_Q R (1#2)) N)). - apply (series_cv_eq (fun n => CRpow (CR_of_Q R (1#2)) n * CRpow (CR_of_Q R (1#2)) (S N))). intro n. destruct (openInt n). rewrite c. unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive. rewrite (CRplus_comm (un n)), CRplus_assoc, <- (CRplus_assoc (un n)). rewrite CRplus_opp_r, CRplus_0_l. rewrite CRpow_plus_distr, Nat.add_comm. simpl. rewrite <- CRmult_plus_distr_r, <- CR_of_Q_plus, Qinv_plus_distr. setoid_replace (1 + 1 # 2)%Q with 1%Q. 2: reflexivity. rewrite CRmult_1_l. reflexivity. apply (CR_cv_proper _ (CR_of_Q R 2 * CRpow (CR_of_Q R (1 # 2)) (S N))). apply series_cv_scale. apply GeoHalfTwo. simpl. rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. 2: reflexivity. rewrite CRmult_1_l. reflexivity. - exists x. exact c. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia