proposition: Lemma IntegralTruncateLimitZero : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), CR_cv _ (fun n : nat => Integral (IntegrableMinConst (Xabs f) (CR_of_Q _ (1 # Pos.of_nat (S n))) (IntegrableAbs fInt) (invSuccRealPositive n))) 0.
proof: Proof. intros. intro p. destruct (IntegralDense f fInt (2*p)%positive) as [n nmaj]. destruct (Ilimit IS (Xsum (IntFn (let (intRepres, _) := fInt in intRepres)) n) (LsumStable (IntFn (let (intRepres, _) := fInt in intRepres)) (IntFnL (let (intRepres, _) := fInt in intRepres)) n)) as [_ cv]. specialize (cv (2*p)%positive) as [k kmaj]. exists (max n k). intros. unfold CRminus. rewrite CRopp_0, CRplus_0_r, CRabs_right. apply (CRle_trans _ (Integral (IntegrableMinConst (Xabs f) (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S (max n k)))) (IntegrableAbs fInt) (invSuccRealPositive (max n k))))). - apply IntegralNonDecreasing. intros y ydf ydg. apply CRmin_glb. rewrite applyXminConst, (DomainProp _ y ydf ydg). apply CRmin_l. apply (CRle_trans _ (CR_of_Q _ (1 # Pos.of_nat (S i)))). apply CRmin_r. 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, Nat2Pos.id. apply le_n_S, H. discriminate. discriminate. - clear H i. specialize (nmaj n (Nat.le_refl n)). specialize (kmaj (max n k) (Nat.le_max_r _ _)). unfold IntegralDistance in nmaj. rewrite <- CRplus_0_r. rewrite <- (CRplus_opp_l (CRabs (RealT (ElemFunc IS)) (I IS _ (LminConstStable (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S (Init.Nat.max n k)))) (Xabs (Xsum (IntFn (let (intRepres, _) := fInt in intRepres)) n)) (invSuccRealPositive (Init.Nat.max n k)) (LabsStable (ElemFunc IS) (Xsum (IntFn (let (intRepres, _) := fInt in intRepres)) n) (LsumStable (IntFn (let (intRepres, _) := fInt in intRepres)) (IntFnL (let (intRepres, _) := fInt in intRepres)) n))) - 0))). rewrite <- CRplus_assoc. setoid_replace (CR_of_Q (RealT (ElemFunc IS)) (1 # p)) with (CR_of_Q (RealT (ElemFunc IS)) (1 # (2*p)) + CR_of_Q _ (1 # (2*p))). apply CRplus_le_compat. 2: exact kmaj. clear kmaj. unfold CRminus. rewrite CRopp_0, CRplus_0_r, CRabs_right. rewrite <- IntegralLstable. pose proof (@IntegralMinus IS). unfold CRminus in H. rewrite <- H. clear H. refine (CRle_trans _ _ _ _ nmaj). clear nmaj. apply IntegralNonDecreasing. intros y ydf ydg. destruct ydf, ydg. rewrite applyXabs. rewrite (applyXminus _ f y d1 d2), CRabs_minus_sym. rewrite (applyXminus _ (XminConst (Xabs (Xsum (IntFn (let (intRepres, _) := fInt in intRepres)) n)) (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S (Init.Nat.max n k))))) y d d0). rewrite applyXminConst, applyXminConst. apply (CRle_trans _ _ _ (CRle_abs _)). apply (CRle_trans _ _ _ (CRmin_contract _ _ _)). rewrite (DomainProp f y d2 d), applyXabs. rewrite (DomainProp _ y d1 d0), applyXabs. apply CRabs_triang_inv2. apply integralPositive. intros y ydf. apply CRmin_glb. apply CRabs_pos. apply CR_of_Q_le. discriminate. rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. reflexivity. - apply IntegralNonNeg. intros y ydf. apply CRmin_glb. apply CRabs_pos. apply CR_of_Q_le. discriminate. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions