proposition: Lemma IntegralTriangle : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), CRabs _ (Integral fInt) <= Integral (IntegrableAbs fInt).
proof: Proof. intros. apply CRabs_le. split. - rewrite <- IntegralOpp. apply IntegralNonDecreasing. intros x xdf xdg. rewrite applyXscale, applyXabs. rewrite (DomainProp f x xdf xdg). rewrite <- CRopp_mult_distr_l, CRmult_1_l. rewrite <- (CRopp_involutive (partialApply f x xdg)). apply CRopp_ge_le_contravar. rewrite CRopp_involutive. rewrite <- CRabs_opp. apply CRle_abs. - apply IntegralNonDecreasing. intros x xdf xdg. rewrite applyXabs. rewrite (DomainProp f x xdg xdf). apply CRle_abs. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase