proposition: Lemma FindJumpPointsFinite : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (a b alpha epsilon : CRcarrier (RealT (ElemFunc IS))) (aPos : 0 < a) (ltab : a < b) (epsPos : 0 < epsilon) (q : nat), alpha <= CR_of_Q _ (Z.of_nat q # 1) * epsilon -> q <> O -> StepApproxBound f fInt a b alpha (CRlt_asym a b ltab) -> { s : nat -> CRcarrier (RealT (ElemFunc IS)) | (s O == a) /\ (forall k:nat, le q k -> s k == b) /\ (forall k:nat, s k <= s (S k)) /\ (forall k:nat, StepApproxBoundOpen f fInt (s k) (s (S k)) epsilon) }.
proof: Proof. intros IS f fInt a b alpha epsilon aPos ltab epsPos q H qnz H0. destruct H0 as [ext c]. pose (StepApproxDiscretize f fInt a b (ext_eta ext) aPos ltab (left_ordered ext) (pair (CRlt_trans _ _ _ aPos ltab) (right_ordered ext))) as Fni. destruct (CRuncountableDiag3 (fun n i k => (Fni n O - Fni n i) * CR_of_Q _ (Z.of_nat q # Pos.of_nat (S k))) _ alpha c) as [epsilonPrime H0]. destruct H0. assert (0 < epsilonPrime) as epsilonPrimePos. { apply (CRle_lt_trans _ (Integral (StepApproxIntegrable f (a - ext_eta ext) a (left_ordered ext) fInt) - Integral (StepApproxIntegrable f b (b + ext_eta ext) (IntExtRightPos ext (CRlt_asym a b ltab), right_ordered ext) fInt))). 2: apply p. apply (CRplus_le_reg_r ( Integral (StepApproxIntegrable f b (b + ext_eta ext) (IntExtRightPos ext (CRlt_asym a b ltab), right_ordered ext) fInt))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_0_l. apply StepApproxIntegralIncr. apply (CRle_trans _ a). apply CRlt_asym, ext. apply CRlt_asym, ltab. apply (CRle_trans _ b). apply CRlt_asym, ltab. apply CRlt_asym, ext. } assert (forall n k:nat, Fni n O - CR_of_Q _ (Z.of_nat (S k) # Pos.of_nat q) * epsilonPrime < Fni n O) as H0. { intros. apply (CRlt_le_trans _ (Fni n 0%nat - 0)). apply CRplus_lt_compat_l, CRopp_gt_lt_contravar. apply CRmult_lt_0_compat. apply CR_of_Q_pos. reflexivity. exact epsilonPrimePos. unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply CRle_refl. } assert (forall n k i : nat, (Fni n 0%nat - CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat (S k) # Pos.of_nat q) * epsilonPrime) ≶ (Fni n i)). { intros. apply (CRplus_appart_reg_r (CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat (S k) # Pos.of_nat q) * epsilonPrime)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply (CRplus_appart_reg_l (-(Fni n i))). apply (CRapart_morph _ _ (CReq_refl _) _ (CR_of_Q _ (Z.of_nat (S k) # Pos.of_nat q) * epsilonPrime)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. rewrite CRplus_comm. specialize (c0 n i k). apply (CRmult_appart_reg_l (CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat q # Pos.of_nat (S k)))). apply CR_of_Q_pos. destruct q. exfalso; exact (qnz (eq_refl O)). reflexivity. apply (CRapart_morph _ _ (CReq_refl _) _ epsilonPrime). rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((Z.of_nat q # Pos.of_nat (S k)) * (Z.of_nat (S k) # Pos.of_nat q))%Q with 1%Q. rewrite CRmult_1_l. reflexivity. unfold Qmult, Qeq, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_r, Z.mul_comm. rewrite Pos2Z.inj_mul. apply f_equal2. simpl (Z.of_nat (S k)). apply f_equal. rewrite Pos.of_nat_succ. reflexivity. destruct q. exfalso; exact (qnz (eq_refl O)). simpl (Z.of_nat (S q)). apply f_equal. rewrite Pos.of_nat_succ. reflexivity. rewrite CRmult_comm. destruct c0. right. exact c0. left. exact c0. } pose proof (fun (n k:nat) => FindCrossingPoint (Fni n) (2 ^ n) (Fni n O - CR_of_Q _ (Z.of_nat (S k) # Pos.of_nat q) * epsilonPrime) (fun i:nat => StepApproxDiscretizeDecr f fInt a b (ext_eta ext) aPos ltab (left_ordered ext) (pair (CRlt_trans _ _ _ aPos ltab) (right_ordered ext)) n i (S i) (le_S i i (Nat.le_refl i))) (H1 n k) (H0 n k)) as H2. clear H1. clear H0. pose (fun (n k:nat) => let (i,_) := H2 n k in BinarySubdiv a b n i) as snk. assert (forall n k:nat, CRabs _ (snk (S n) k - snk n k) <= (b-a) * CRpow (CR_of_Q _ (1#2)) n). { intros n k. unfold snk. destruct (H2 n k), (H2 (S n) k). apply CRabs_le. split. - pose proof (FindCrossingPointIncr f fInt a b (ext_eta ext) (Fni n O - CR_of_Q _ (Z.of_nat (S k) # Pos.of_nat q) * epsilonPrime) aPos ltab (left_ordered ext) (pair (CRlt_trans _ _ _ aPos ltab) (right_ordered ext)) _ _ _ p0 p1). apply (CRplus_le_reg_r (BinarySubdiv a b n x)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply (CRplus_le_reg_l ((b - a) * CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) n)). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l, CRplus_comm. apply (CRle_trans _ _ _ H0). apply CRplus_le_compat_l. apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltab. rewrite <- (CRmult_1_l (CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) n)). simpl. apply CRmult_le_compat_r. apply CRpow_ge_zero, CRlt_asym, CR_of_Q_pos. reflexivity. apply CR_of_Q_le. discriminate. - pose proof (FindCrossingPointDecr f fInt a b (ext_eta ext) (Fni n O - CR_of_Q _ (Z.of_nat (S k) # Pos.of_nat q) * epsilonPrime) aPos ltab (left_ordered ext) (pair (CRlt_trans _ _ _ aPos ltab) (right_ordered ext)) _ _ _ p0 p1). apply (CRplus_le_reg_r (BinarySubdiv a b n x)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_comm. exact H0. } assert (series_cv (fun n : nat => (b - a) * CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) n) (CR_of_Q _ 2 * (b-a))). { apply (series_cv_eq (fun n : nat => CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) n * (b-a))). intro n. apply CRmult_comm. apply series_cv_scale. apply GeoHalfTwo. } pose proof (fun (k:nat) => diff_series_cv_maj (fun n => snk n k) (fun n => (b - a) * CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) n) (CR_of_Q _ 2 * (b-a)) (fun n => H0 n k) H1). pose (fun k:nat => match k with | O => a | S i => let (l,_) := H3 i in l end) as sk. exists sk. assert (forall k:nat, le q k -> sk k == b) as lastB. { intros. unfold sk. destruct k. exfalso. inversion H4. rewrite H5 in qnz. exact (qnz (eq_refl _)). destruct (H3 k) as [x p0]. destruct p0. clear c2. apply (CR_cv_unique (fun n : nat => snk n k) _ _ c1). clear c1 x. apply (CR_cv_eq _ (fun _ : nat => b)). 2: apply CR_cv_const. intro n. unfold snk. destruct (H2 n k). destruct p0, p0. destruct s. - rewrite e. rewrite BinarySubdivRight. reflexivity. apply CRlt_asym, ltab. - exfalso. clear c1. contradict c2. apply (CRle_trans _ (Fni n (S (2^n)))). 2: apply StepApproxDiscretizeDecr, le_n_S, l. apply (CRle_trans _ ( Fni n 0%nat - 1 * epsilonPrime)). apply CRplus_le_compat_l, CRopp_ge_le_contravar. apply CRmult_le_compat_r. apply CRlt_asym, epsilonPrimePos. apply CR_of_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_l. simpl (Z.of_nat (S k)). apply Pos2Z.pos_le_pos. rewrite Pos.of_nat_succ. apply Pos2Nat.inj_le. rewrite Nat2Pos.id, Nat2Pos.id. exact H4. discriminate. exact qnz. rewrite CRmult_1_l. apply (CRplus_le_reg_r epsilonPrime). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply (CRplus_le_reg_l (-Fni n (S (2^n)))). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l, CRplus_comm. destruct p. unfold Fni, StepApproxDiscretize. destruct (le_lt_dec (S (2 ^ n)) (S (2 ^ n))). rewrite (StepApproxProofIrrel f fInt _ _ (CRlt_trans 0 a b aPos ltab, right_ordered ext) (IntExtRightPos ext (CRlt_asym a b ltab), right_ordered ext) ). apply CRlt_asym, c1. exfalso; exact (proj1 (Nat.lt_nge _ _) l0 (Nat.le_refl _)). } assert (forall k : nat, sk k <= sk (S k)) as skIncr. { unfold sk. intros k. destruct k. - destruct (H3 O). apply (CR_cv_bound_down (fun n : nat => snk n 0%nat) _ _ O). intros. unfold snk. destruct (H2 n O). apply BinarySubdivInside. apply CRlt_asym, ltab. apply (fst p1). exact (fst p0). - destruct (H3 k), (H3 (S k)). apply (CR_cv_le (fun n : nat => snk n k) (fun n : nat => snk n (S k))). 2: exact (fst p0). 2: exact (fst p1). intro n. unfold snk. destruct (H2 n k), (H2 n (S k)). apply CRplus_le_compat_l. rewrite CRmult_assoc, CRmult_assoc. apply CRmult_le_compat_r. apply CRmult_le_0_compat. apply CRlt_asym, CRlt_minus, ltab. apply CRpow_ge_zero. apply CRlt_asym, CR_of_Q_pos. reflexivity. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le. apply (FindCrossingPointThreasholdDecr f fInt a b (ext_eta ext) (Fni n 0%nat - CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat (S (S k)) # Pos.of_nat q) * epsilonPrime) (Fni n 0%nat - CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat (S k) # Pos.of_nat q) * epsilonPrime) aPos ltab (left_ordered ext) (CRlt_trans 0 a b aPos ltab, right_ordered ext) n). 2: exact p3. 2: exact p2. apply CRplus_le_compat_l, CRopp_ge_le_contravar. apply CRmult_le_compat_r. apply CRlt_asym, epsilonPrimePos. apply CR_of_Q_le. unfold Qle, Qnum, Qden. apply Z.mul_le_mono_nonneg_r. discriminate. apply Nat2Z.inj_le. apply le_S, Nat.le_refl. } split. 2: split. 3: split. - reflexivity. - exact lastB. - exact skIncr. - intros k x y u v ltxy ltuv H4 H5 H6. destruct (le_lt_dec q k) as [l | ltkq]. contradict H6. apply (CRle_trans _ b). apply lastB. apply le_S, l. apply (CRle_trans _ u). 2: apply CRlt_asym, (snd ltuv). apply (CRle_trans _ y). 2: exact H5. apply (CRle_trans _ x). 2: apply CRlt_asym, (snd ltxy). rewrite <- (lastB k). apply CRlt_asym, H4. exact l. assert (CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat 1 # Pos.of_nat q) * epsilonPrime < epsilon). { apply (CRmult_lt_reg_l (CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat q # 1))). apply CR_of_Q_pos. destruct q. exfalso; exact (qnz (eq_refl _)). reflexivity. apply (CRlt_le_trans _ alpha). 2: exact H. apply (CRle_lt_trans _ epsilonPrime). 2: exact (snd p). rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((Z.of_nat q # 1) * (Z.of_nat 1 # Pos.of_nat q))%Q with 1%Q. rewrite CRmult_1_l. apply CRle_refl. unfold Qmult, Qeq, Qnum, Qden. simpl. do 2 rewrite Z.mul_1_r. destruct q. exfalso; exact (qnz (eq_refl _)). simpl (Z.of_nat (S q)). apply f_equal. apply (Pos.of_nat_succ). } destruct (CR_cv_open_below (fun n => snk n k + (CRpow (CR_of_Q _ (1#2)) n)*(-(b-a))) v (sk (S k))) as [m mcv]. apply (CR_cv_proper _ (sk (S k) + 0)). 2: apply CRplus_0_r. apply CR_cv_plus. unfold sk. destruct (H3 k). exact (fst p0). apply (CR_cv_proper _ (0 * (-(b-a)))). apply CR_cv_scale. apply GeoCvZero. apply CRmult_0_l. exact H6. destruct k. + apply (CRle_trans _ (Fni m O - Fni m (let (i, _) := H2 m O in i))). unfold sk in H4. apply CRplus_le_compat. apply StepApproxIntegralIncr. apply (CRle_trans _ a). apply CRlt_asym, (snd (left_ordered ext)). apply CRlt_asym, H4. apply (CRle_trans _ x). apply CRlt_asym, H4. apply CRlt_asym, (snd ltxy). apply CRopp_ge_le_contravar. unfold Fni. specialize (mcv m (Nat.le_refl m)). unfold snk in mcv. destruct (H2 m O), p0, p0. unfold StepApproxDiscretize. destruct x0. exfalso. contradict mcv. apply (CRle_trans _ (a+0)). unfold BinarySubdiv. rewrite CRmult_0_l, CRmult_0_l, CRplus_assoc. apply CRplus_le_compat_l. rewrite CRplus_0_l, <- CRopp_mult_distr_r, <- CRopp_0. apply CRopp_ge_le_contravar, CRmult_le_0_compat. apply CRpow_ge_zero. apply CRlt_asym, CR_of_Q_pos. reflexivity. apply CRlt_asym, CRlt_minus, ltab. rewrite CRplus_0_r. apply CRlt_asym. apply (CRlt_trans _ _ _ H4), (CRlt_trans _ _ _ (snd ltxy)). apply (CRle_lt_trans _ _ _ H5), (snd ltuv). destruct (le_lt_dec (S (2 ^ m)) (S x0)). exfalso. apply le_S_n in l0. exact (proj1 (Nat.lt_nge _ _) l l0). assert (v <= BinarySubdiv a b m x0). { apply (CRle_trans _ (BinarySubdiv a b m (S x0) + CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) m * - (b - a))). apply CRlt_asym, mcv. rewrite <- BinarySubdivNext. rewrite <- CRopp_mult_distr_r, CRplus_assoc, CRplus_opp_r. rewrite CRplus_0_r. apply CRle_refl. } apply StepApproxIntegralIncr. clear l0 c1 s. apply (CRle_trans _ v). apply CRlt_asym, (snd ltuv). exact H8. apply (CRle_trans _ _ _ H8). apply CRplus_le_compat_l. rewrite CRmult_assoc, CRmult_assoc. apply CRmult_le_compat_r. apply CRmult_le_0_compat. apply CRlt_asym, CRlt_minus, ltab. apply CRpow_ge_zero. apply CRlt_asym, CR_of_Q_pos. reflexivity. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, le_S, Nat.le_refl. destruct (H2 m O), p0, p0. apply (CRplus_le_reg_r (Fni m x0)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply (CRplus_le_reg_r (- (CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat 1 # Pos.of_nat q) * epsilonPrime))). apply (CRle_trans _ (Fni m x0) _ (CRlt_asym _ _ c1)). rewrite (CRplus_comm epsilon), <- (CRplus_0_r (Fni m x0)). rewrite CRplus_assoc, CRplus_assoc. apply CRplus_le_compat_l. rewrite CRplus_0_l. apply CRlt_asym, CRlt_minus, H7. + destruct (CR_cv_open_above (fun n => snk n k + (CRpow (CR_of_Q _ (1#2)) n)*(b-a)) x (sk (S k))) as [n ncv]. 2: exact H4. apply (CR_cv_proper _ (sk (S k) + 0)). 2: apply CRplus_0_r. apply CR_cv_plus. unfold sk. destruct (H3 k), p0. exact c1. apply (CR_cv_proper _ (0 * (b-a))). apply CR_cv_scale. apply GeoCvZero. apply CRmult_0_l. specialize (ncv (max n m) (Nat.le_max_l _ _)). specialize (mcv (max n m) (Nat.le_max_r _ _)). rewrite <- CRopp_mult_distr_r in mcv. apply (CRle_trans _ (Fni (max n m) (let (i,_) := H2 (max n m) k in S i) - Fni (max n m) (let (i, _) := H2 (max n m) (S k) in i))). * assert (forall i j:nat, le i j -> sk i <= sk j). { induction j. intros. inversion H8. apply CRle_refl. intros. apply Nat.le_succ_r in H8. destruct H8. apply (CRle_trans _ (sk j)). exact (IHj H8). apply skIncr. subst i. apply CRle_refl. } apply CRplus_le_compat. clear mcv. unfold Fni, StepApproxDiscretize. unfold snk in ncv. destruct (H2 (max n m) k) as [x0 p0]. destruct (le_lt_dec (S (2 ^ max n m)) (S x0)). destruct p0, p0. apply le_S_n in l. apply (Nat.le_antisymm _ _ l0) in l. subst x0. clear l0 s c1. contradict ncv. apply (CRle_trans _ (b+0)). rewrite CRplus_0_r. apply (CRle_trans _ y _ (CRlt_asym _ _ (snd ltxy))). apply (CRle_trans _ u _ H5). apply (CRle_trans _ v _ (CRlt_asym _ _ (snd ltuv))). apply (CRle_trans _ _ _ (CRlt_asym _ _ H6)). apply (CRle_trans _ (sk q)). apply H8. exact ltkq. apply lastB. apply Nat.le_refl. rewrite BinarySubdivRight. apply CRplus_le_compat_l. apply CRlt_asym, CRmult_lt_0_compat. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. apply CRlt_minus, ltab. apply CRlt_asym, ltab. rewrite BinarySubdivNext in ncv. apply StepApproxIntegralIncr. apply le_S_n in l. destruct p0, p0. clear l0. apply (CRle_trans _ (BinarySubdiv a b (max n m) (S x0))). apply CRlt_asym, BinarySubdivIncr. exact (pair aPos ltab). apply CRlt_asym, ncv. apply (CRle_trans _ x). apply CRlt_asym, ncv. apply CRlt_asym, (snd ltxy). clear ncv. apply CRopp_ge_le_contravar. unfold Fni, StepApproxDiscretize. unfold snk in mcv. destruct (H2 (max n m) (S k)), p0, p0. destruct x0. clear l c1. contradict mcv. apply (CRle_trans _ (a-0)). unfold BinarySubdiv, CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. rewrite CRmult_0_l, CRmult_0_l, CRplus_0_l. apply CRopp_ge_le_contravar. apply CRlt_asym, CRmult_lt_0_compat. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. apply CRlt_minus, ltab. unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply (CRle_trans _ (sk (S k))). apply (H8 O (S k)), Nat.le_0_l. apply (CRle_trans _ x _ (CRlt_asym _ _ H4)). apply (CRle_trans _ y _ (CRlt_asym _ _ (snd ltxy))). apply (CRle_trans _ u _ H5). apply CRlt_asym, (snd ltuv). destruct (le_lt_dec (S (2 ^ max n m)) (S x0)). apply le_S_n in l0. exfalso. exact (proj1 (Nat.lt_nge _ _) l l0). apply CRlt_asym in mcv. rewrite <- BinarySubdivNext, CRplus_assoc, CRplus_opp_r, CRplus_0_r in mcv. apply StepApproxIntegralIncr. apply (CRle_trans _ v _ (CRlt_asym _ _ (snd ltuv)) mcv). apply (CRle_trans _ _ _ mcv). apply CRlt_asym, BinarySubdivIncr. exact (pair aPos ltab). * destruct (H2 (max n m) k) as [x0 p0], (H2 (max n m) (S k)) as [x1 p1]. destruct p0, p1, p0, p1. destruct s. subst x0. apply (CRplus_le_reg_r (Fni (max n m) x1)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply (CRle_trans _ (0 + Fni (max n m) x1)). rewrite CRplus_0_l. apply StepApproxDiscretizeDecr. apply le_S, l0. apply CRplus_le_compat_r. apply CRlt_asym, epsPos. apply (CRle_trans _ (Fni (Init.Nat.max n m) 0%nat - CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat (S k) # Pos.of_nat q) * epsilonPrime - (Fni (Init.Nat.max n m) 0%nat - CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat (S (S k)) # Pos.of_nat q) * epsilonPrime))). apply CRplus_le_compat. apply CRlt_asym, c3. apply CRopp_ge_le_contravar. apply CRlt_asym, c2. unfold CRminus. rewrite (CRplus_comm (Fni (max n m) O)), CRplus_assoc, CRopp_plus_distr. rewrite <- (CRplus_assoc (Fni (max n m) O)), CRplus_opp_r, CRplus_0_l. rewrite CRopp_involutive, CRopp_mult_distr_l. rewrite <- CRmult_plus_distr_r. apply (CRle_trans _ ((CR_of_Q _ (1 # Pos.of_nat q)) * epsilonPrime)). apply CRmult_le_compat_r. apply CRlt_asym, epsilonPrimePos. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus. apply CR_of_Q_le. rewrite Qplus_comm, Qinv_minus_distr. unfold Qle, Qnum, Qden. apply Z.mul_le_mono_nonneg_r. discriminate. destruct k. discriminate. 2: apply CRlt_asym, H7. rewrite (Z.add_le_mono_r _ _ (Z.of_nat (S (S k)))). ring_simplify. replace 1%Z with (Z.of_nat 1). rewrite <- Nat2Z.inj_add, Nat.add_comm. apply Z.le_refl. reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia