proposition: Lemma ClosedIntervalIntegrable : forall {R : ConstructiveReals} (a b : CRcarrier R), a <= b -> { limInt : @IntegrableSet IntSpaceCSUCFunctions (fun x => a <= x <= b) | MeasureSet limInt == b-a }.
proof: Proof. intros. assert (forall n:nat, a - CR_of_Q R (1 # Pos.of_nat n) < b + CR_of_Q R (1 # Pos.of_nat n)) as ltabn. { intro n. apply (CRle_lt_trans _ (a + 0)). rewrite <- CRopp_0. apply CRplus_le_compat_l, CRopp_ge_le_contravar. apply CR_of_Q_le. discriminate. apply (CRle_lt_trans _ (b+0)). apply CRplus_le_compat_r, H. apply CRplus_lt_compat_l, CR_of_Q_pos. reflexivity. } assert (CR_cv R (fun i : nat => CR_of_Q R (1 # Pos.of_nat i)) 0) as invCv. { intro p. exists (Pos.to_nat p). intros. unfold CRminus. rewrite CRopp_0, CRplus_0_r, CRabs_right. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. exact H0. destruct i. exfalso. inversion H0. pose proof (Pos2Nat.is_pos p). rewrite H2 in H1. inversion H1. discriminate. apply CR_of_Q_le. discriminate. } destruct (@IntegrableSetCountableIntersect IntSpaceCSUCFunctions (fun n x => CRltProp R (a - CR_of_Q _ (1 # Pos.of_nat n)) x /\ CRltProp R x (b + CR_of_Q _ (1 # Pos.of_nat n))) (fun n => let (i,_) := OpenIntervalIntegrable _ _ (ltabn n) in i) (b-a)). - apply (CR_cv_eq _ (fun n => b + CR_of_Q R (1 # Pos.of_nat n) - (a - CR_of_Q R (1 # Pos.of_nat n)))). intro n. rewrite MeasureIntersectSeqDecr. destruct (OpenIntervalIntegrable (a - CR_of_Q R (1 # Pos.of_nat n)) (b + CR_of_Q R (1 # Pos.of_nat n)) (ltabn n)). symmetry; exact c. intros. destruct H0. split. apply CRltForget. apply CRltEpsilon in H0. apply (CRle_lt_trans _ (a - CR_of_Q R (1 # Pos.of_nat (S n0)))). 2: exact H0. apply CRplus_le_compat_l. apply CRopp_ge_le_contravar. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. destruct n0. discriminate. apply Pos2Nat.inj_le. rewrite Nat2Pos.id, Nat2Pos.id. apply le_S, Nat.le_refl. discriminate. discriminate. apply CRltEpsilon in H1. apply CRltForget. apply (CRlt_le_trans _ _ _ H1). apply CRplus_le_compat_l. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. destruct n0. discriminate. apply Pos2Nat.inj_le. rewrite Nat2Pos.id, Nat2Pos.id. apply le_S, Nat.le_refl. discriminate. discriminate. apply CR_cv_minus. apply (CR_cv_proper _ (b+0)). apply CR_cv_plus. apply CR_cv_const. exact invCv. rewrite CRplus_0_r. reflexivity. apply (CR_cv_proper _ (a-0)). apply CR_cv_minus. apply CR_cv_const. exact invCv. unfold CRminus. rewrite CRopp_0, CRplus_0_r. reflexivity. - assert (forall x, (forall n : nat, CRltProp R (a - CR_of_Q R (1 # Pos.of_nat n)) x /\ CRltProp R x (b + CR_of_Q R (1 # Pos.of_nat n))) <-> a <= x <= b) as H0. { split. intros. split. apply (CR_cv_bound_up (fun n => (a - CR_of_Q R (1 # Pos.of_nat n))) _ _ O). intros. specialize (H0 n) as [H0 _]. apply CRlt_asym, CRltEpsilon, H0. apply (CR_cv_proper _ (a-0)). apply CR_cv_minus. apply CR_cv_const. exact invCv. unfold CRminus. rewrite CRopp_0, CRplus_0_r. reflexivity. apply (CR_cv_bound_down (fun n => (b + CR_of_Q R (1 # Pos.of_nat n))) _ _ O). intros. specialize (H0 n) as [_ H0]. apply CRlt_asym, CRltEpsilon, H0. apply (CR_cv_proper _ (b+0)). apply CR_cv_plus. apply CR_cv_const. exact invCv. rewrite CRplus_0_r. reflexivity. intros. split. apply CRltForget. apply (CRlt_le_trans _ (a+-0)). 2: rewrite CRopp_0, CRplus_0_r; exact (proj1 H0). apply CRplus_lt_compat_l, CRopp_gt_lt_contravar, CR_of_Q_pos. reflexivity. apply CRltForget. apply (CRle_lt_trans _ (b+0)). rewrite CRplus_0_r. exact (proj2 H0). apply CRplus_lt_compat_l, CR_of_Q_pos. reflexivity. } exists (IntegrableSetExtensional (fun x : X (ElemFunc IntSpaceCSUCFunctions) => forall n : nat, CRltProp R (a - CR_of_Q R (1 # Pos.of_nat n)) x /\ CRltProp R x (b + CR_of_Q R (1 # Pos.of_nat n))) _ (fun x _ => H0 x) x0). rewrite <- (MeasureExtensional _ _ x0 _ (fun x _ _ => H0 x)). exact c. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets