proposition: Lemma CSUCIntegralLimit : forall {R : ConstructiveReals} (f : PartialFunction (CRcarrier R)) (fL : Is_CSUC_func f), prod (CR_cv _ (fun n => IntegralCSUC (XminConst f (INR n)) (@LminIntStable ElemCSUC n f fL)) (IntegralCSUC f fL)) (CR_cv _ (fun n => IntegralCSUC (XminConst (Xabs f) (CR_of_Q R (1# Pos.of_nat (S n)))) (@LminConstStable ElemCSUC (CR_of_Q R (1# Pos.of_nat (S n))) (Xabs f) (invSuccRealPositive n) (LabsStable ElemCSUC f fL))) 0).
proof: Proof. split. - destruct (CSUC_bounded (TotalizeFunc (CRcarrier R) f (CSUC_fullDomain _ fL)) (CSUC_low _ fL) (CSUC_high _ fL) (CSUC_cont_mod _ fL) (CSUC_adapt _ fL) (CSUC_lowHigh _ fL)) as [B Bmaj]. destruct (CRup_nat B) as [k kmaj]. apply (CR_cv_shift _ k). apply (CR_cv_eq _ (fun n : nat => IntegralCSUC f fL)). intro n. apply IntegralCSUC_ext. intro x0. assert (PartialFunExtEq f (XminConst f (INR (n + k)))) as feq. { split. split. intros x H. destruct f; simpl. exact H. intros x H. destruct f; simpl. exact H. intros. unfold XminConst, Xop, partialApply. rewrite CRmin_left. rewrite (DomainProp f x1 xD xG). reflexivity. apply (CRle_trans _ B). specialize (Bmaj x1). unfold TotalizeFunc in Bmaj. rewrite (DomainProp _ _ _ (CSUC_fullDomain f fL x1)). apply (CRle_trans _ _ _ (CRle_abs _)). apply CRlt_asym, Bmaj. apply (CRle_trans _ (INR k)). apply CRlt_asym, kmaj. apply CR_of_Q_le. unfold Qle, Qden, Qnum. do 2 rewrite Z.mul_1_r. rewrite <- (Z.add_0_r (Z.of_nat k)). rewrite Nat2Z.inj_add. rewrite (Z.add_comm (Z.of_nat n)). apply Z.add_le_mono_l. apply Nat2Z.is_nonneg. } rewrite (CSUC_transport_apply f (XminConst f (INR (n + k))) fL feq). unfold TotalizeFunc. apply DomainProp. exists O. intros. unfold CRminus. rewrite CRplus_opp_r. rewrite CRabs_right. apply CR_of_Q_le; discriminate. apply CRle_refl. - intros p. destruct (CRup_nat ((CSUC_high f fL - CSUC_low f fL ) * (CR_of_Q R (Z.pos p # 1)))) as [k kmaj]. exists k. intros n H. unfold CRminus. rewrite CRopp_0. rewrite CRplus_0_r. rewrite CRabs_right. apply (CRle_trans _ (CR_of_Q R (1# Pos.of_nat (S n)) * (CSUC_high _ (@LminConstStable ElemCSUC (CR_of_Q R (1# Pos.of_nat (S n))) (Xabs f) (invSuccRealPositive n) (LabsStable ElemCSUC f fL)) - CSUC_low _ (@LminConstStable ElemCSUC (CR_of_Q R (1# Pos.of_nat (S n))) (Xabs f) (invSuccRealPositive n) (LabsStable ElemCSUC f fL))))). + apply IntegralCSUC_bounded. intro x0. apply CRmin_r. + apply CRlt_asym in kmaj. apply (CRmult_le_compat_r (CR_of_Q R (1 # p))) in kmaj. rewrite CRmult_assoc, <- CR_of_Q_mult in kmaj. setoid_replace ((Z.pos p # 1) * (1 # p))%Q with 1%Q in kmaj. rewrite CRmult_1_r in kmaj. apply (CRmult_le_reg_l (CR_of_Q R (Z.of_nat (S n) #1))). apply CR_of_Q_pos; reflexivity. rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((Z.of_nat (S n) # 1) * (1 # Pos.of_nat (S n)))%Q with 1%Q. rewrite CRmult_1_l. apply (CRle_trans _ (INR k * CR_of_Q R (1#p))). apply (CRle_trans _ (CSUC_high f fL - CSUC_low f fL)). 2: apply kmaj. unfold LminConstStable. rewrite <- CSUC_transport_low. rewrite <- CSUC_transport_high. destruct f, fL; apply CRle_refl. apply CRmult_le_compat_r. apply CR_of_Q_le; discriminate. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, le_S, H. unfold Qmult, Qeq, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r, Z.mul_1_l, Pos.mul_1_l. rewrite <- positive_nat_Z, Nat2Pos.id. reflexivity. discriminate. unfold Qmult, Qeq, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r, Z.mul_1_l, Pos.mul_1_l. reflexivity. apply CR_of_Q_le. discriminate. + unfold IntegralCSUC. apply (UC_integral_pos (TotalizeFunc (CRcarrier R) (XminConst (Xabs f) (CR_of_Q R (1 # Pos.of_nat (S n)))) (CSUC_fullDomain (XminConst (Xabs f) (CR_of_Q R (1 # Pos.of_nat (S n)))) (@LminConstStable ElemCSUC (CR_of_Q R (1 # Pos.of_nat (S n))) (Xabs f) (invSuccRealPositive n) (LabsStable ElemCSUC f fL))))). intros. unfold TotalizeFunc. assert (Domain (Xabs f) x0). { destruct fL,f; apply CSUC_fullDomain0. } rewrite applyXminConst. apply CRmin_glb. 2: apply CR_of_Q_le; discriminate. destruct f; apply CRabs_pos. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets