proposition: Lemma integralAbsMaj : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fL : L (ElemFunc IS) f), CRabs _ (I IS f fL) <= Iabs f fL.
proof: Proof. intros. apply CRabs_le. split. + unfold Iabs. rewrite <- (CRmult_1_l (I IS (Xabs f) (LabsStable (ElemFunc IS) f fL))). rewrite (CRopp_mult_distr_l 1). rewrite <- Ihomogeneous. apply INonDecreasing. intros. rewrite applyXscale. rewrite <- (CRopp_mult_distr_l 1). rewrite CRmult_1_l. destruct f; simpl. rewrite <- (CRopp_involutive (partialApply x y)). rewrite (DomainProp x xF y). rewrite <- CRabs_opp. apply CRopp_ge_le_contravar. apply CRle_abs. + apply INonDecreasing. intros. destruct f; simpl. rewrite (DomainProp x xF y). apply CRle_abs. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions