proposition: Lemma IntegralTruncateLimit : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), CR_cv _ (fun n : nat => Integral (IntegrableMinInt f n fInt)) (Integral fInt).
proof: Proof. intros IS f fInt. apply CR_cv_growing. - intro n. apply IntegralNonDecreasing. intros x xdf xdg. assert (Domain f x). { destruct f; exact xdf. } apply CRmin_glb. unfold XminConst, Xop, partialApply. rewrite (DomainProp f x xdf xdg). apply CRmin_l. apply (CRle_trans _ _ _ (CRmin_r _ _)). 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. - intro n. apply IntegralNonDecreasing. intros x xdf xdg. unfold XminConst, Xop, partialApply. rewrite (DomainProp f x xdf xdg). apply CRmin_l. - intro p. assert ({ g : PartialFunction (X (ElemFunc IS)) & { gL : L (ElemFunc IS) g | IntegralDistance fInt (IntegrableL g gL) <= CR_of_Q _ (1#3*p) } }). { pose proof (IntegralDense f fInt (3*p)%positive) as [n nmaj]. specialize (nmaj n (Nat.le_refl n)). exists (Xsum (IntFn (let (intRepres, _) := fInt in intRepres)) n). exists (LsumStable _ (IntFnL (let (intRepres, _) := fInt in intRepres)) n). rewrite IntegralDistance_sym. apply (CRle_trans _ (IntegralDistance (IntegrableSum (IntFn (let (intRepres, _) := fInt in intRepres)) (fun n : nat => IntegrableL (IntFn (let (intRepres, _) := fInt in intRepres) n) (IntFnL (let (intRepres, _) := fInt in intRepres) n)) n) fInt)). 2: exact nmaj. clear nmaj. apply IntegralNonDecreasing. intros x xdf xdg. rewrite (DomainProp _ _ xdf xdg). apply CRle_refl. } destruct X as [g [gL gdist]]. pose proof (Ilimit IS g gL) as [glim _]. specialize (glim (3*p)%positive) as [n nmaj]. exists n. apply (CRle_trans _ (I IS g gL + CR_of_Q _ (1#3*p) - Integral (IntegrableMinInt f n fInt))). apply CRplus_le_compat. 2: apply CRle_refl. apply (CRplus_le_reg_l (-I IS g gL)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite CRplus_comm. apply (CRle_trans _ _ _ (CRle_abs _)). fold (Integral fInt - I IS g gL). rewrite <- IntegralLstable. rewrite <- IntegralMinus. exact (CRle_trans _ _ _ (IntegralTriangle _ _) gdist). apply (CRle_trans _ (I IS g gL + CR_of_Q _ (1 # 3 * p) - I IS _ (LminIntStable n g gL) + CR_of_Q _ (1#3*p))). unfold CRminus. rewrite (CRplus_assoc (I IS g gL + CR_of_Q _ (1 # 3 * p))). apply CRplus_le_compat. apply CRle_refl. apply (CRplus_le_reg_l (I IS _ (LminIntStable n g gL))). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. fold (I IS _ (LminIntStable n g gL) - Integral (IntegrableMinInt f n fInt)). rewrite <- IntegralLstable, <- IntegralMinus. apply (CRle_trans _ _ _ (CRle_abs _)). apply (CRle_trans _ _ _ (IntegralTriangle _ _)). apply (CRle_trans _ (IntegralDistance fInt (IntegrableL g gL))). 2: exact gdist. rewrite IntegralDistance_sym. apply IntegralNonDecreasing. intros x xdf xdg. destruct xdf, xdg. rewrite applyXabs, applyXabs, (applyXminus (XminConst g (INR n)) (XminConst f (INR n))), (applyXminus g f), applyXminConst, applyXminConst. assert (0 <= @INR (RealT (ElemFunc IS)) n) as nPos. { apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.is_nonneg. } apply (CRle_trans _ _ _ (CRmin_contract _ _ _)). rewrite (DomainProp g x d d1). rewrite (DomainProp f x d0 d2). apply CRle_refl. apply (CRle_trans _ (CR_of_Q _ (1 # 3 * p) + CR_of_Q _ (1 # 3 * p) + CR_of_Q _ (1 # 3 * p))). apply CRplus_le_compat. 2: apply CRle_refl. unfold CRminus. rewrite (CRplus_comm (I IS g gL)), CRplus_assoc. apply CRplus_le_compat_l. specialize (nmaj n (Nat.le_refl n)). rewrite CRabs_minus_sym in nmaj. exact (CRle_trans _ _ _ (CRle_abs _) nmaj). rewrite <- CR_of_Q_plus, <- CR_of_Q_plus. apply CR_of_Q_le. rewrite Qinv_plus_distr, Qinv_plus_distr. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l. rewrite Pos2Z.inj_mul. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions