proposition: Lemma IntegrableZeroMaj : forall {IS : IntegrationSpace}, PartialRestriction (XinfiniteSumAbs (IntFn (IntegralRepresentationZero))) (Xconst (X (ElemFunc IS)) 0).
proof: Proof. split. - intros x [xn cv]. simpl. trivial. - intros. destruct xD as [xn cv]. transitivity (CR_of_Q (RealT (ElemFunc IS)) 0). apply applyInfiniteSumAbs. apply (series_cv_eq (fun _ => 0)). intro n. unfold IntegralRepresentationZero, IntFn. rewrite applyIzero. reflexivity. intros p. exists O. intros. rewrite sum_const. rewrite CRmult_0_l. unfold CRminus. rewrite CRplus_opp_r, CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase