proposition: Lemma StepApproxBoundCv : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (t : CRcarrier (RealT (ElemFunc IS))) (tPos : 0 < t), (forall b : CRcarrier (RealT (ElemFunc IS)), 0 < b -> StepApproxBound f fInt t t b (CRle_refl t)) -> CR_cauchy _ (fun n:nat => Integral (StepApproxIntegrable f _ t (StepApproxBetween t tPos n) fInt)).
proof: Proof. intros. intro p. destruct (H (CR_of_Q _ (1 # p))) as [ext extmaj]. apply CR_of_Q_pos. reflexivity. assert (0 < ext_eta ext). { destruct ext; clear extmaj. simpl. apply (CRplus_lt_reg_l _ t). rewrite CRplus_0_r. exact right_ordered0. } destruct (CR_cv_open_below _ (t-ext_eta ext) t (StepApproxCv t)) as [n nmaj]. apply ext. exists n. intros. destruct (le_lt_dec i j). - rewrite CRabs_right. apply (CRle_trans _ (Integral (StepApproxIntegrable f (t - ext_eta ext) t (left_ordered ext) fInt) - Integral (StepApproxIntegrable f t (t + ext_eta ext) (IntExtRightPos ext (CRle_refl t), right_ordered ext) fInt))). 2: apply CRlt_asym; exact extmaj. apply CRplus_le_compat. apply StepApproxIntegralIncr. apply CRlt_asym, nmaj, H1. apply CRle_refl. apply CRopp_ge_le_contravar. apply StepApproxIntegralIncr. apply CRlt_asym, StepApproxBetween, tPos. apply CRlt_asym, ext. apply (CRplus_le_reg_r (Integral (StepApproxIntegrable f (t * CR_of_Q (RealT (ElemFunc IS)) (1 - (1 # Pos.of_nat (2 * S j)))) t (StepApproxBetween t tPos j) fInt))). unfold CRminus. rewrite CRplus_0_l, CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply StepApproxIntegralIncr. 2: apply CRle_refl. apply CRmult_le_compat_l. apply CRlt_asym, tPos. apply CR_of_Q_le, Qplus_le_r, Qopp_le_compat. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. rewrite Pos2Nat.inj_le, Nat2Pos.id, Nat2Pos.id. apply Nat.mul_le_mono_nonneg_l. auto. apply le_n_S, l. discriminate. discriminate. - rewrite CRabs_minus_sym. rewrite CRabs_right. apply (CRle_trans _ (Integral (StepApproxIntegrable f (t - ext_eta ext) t (left_ordered ext) fInt) - Integral (StepApproxIntegrable f t (t + ext_eta ext) (IntExtRightPos ext (CRle_refl t), right_ordered ext) fInt))). 2: apply CRlt_asym; exact extmaj. apply CRplus_le_compat. apply StepApproxIntegralIncr. apply CRlt_asym, nmaj, H2. apply CRle_refl. apply CRopp_ge_le_contravar. apply StepApproxIntegralIncr. apply CRlt_asym, StepApproxBetween, tPos. apply CRlt_asym, ext. apply (CRplus_le_reg_r (Integral (StepApproxIntegrable f (t * CR_of_Q (RealT (ElemFunc IS)) (1 - (1 # Pos.of_nat (2 * S i)))) t (StepApproxBetween t tPos i) fInt))). unfold CRminus. rewrite CRplus_0_l, CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply StepApproxIntegralIncr. 2: apply CRle_refl. apply CRmult_le_compat_l. apply CRlt_asym, tPos. apply CR_of_Q_le, Qplus_le_r, Qopp_le_compat. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. rewrite Pos2Nat.inj_le, Nat2Pos.id, Nat2Pos.id. apply Nat.mul_le_mono_nonneg_l. auto. apply le_S, l. discriminate. discriminate. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia