proposition: Lemma IAbsSumMaj : forall {IS : IntegrationSpace} (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnL : forall n:nat, L (ElemFunc IS) (fn n)) (n : nat), Iabs (Xsum fn n) (LsumStable fn fnL n) <= CRsum (fun n0 : nat => Iabs (fn n0) (fnL n0)) n.
proof: Proof. induction n. - simpl. apply CRle_refl. - simpl. apply (CRle_trans _ (I IS (Xplus (Xabs (Xsum fn n)) (Xabs (fn (S n)))) (LplusStable (ElemFunc IS) (Xabs (Xsum fn n)) (Xabs (fn (S n))) (LabsStable (ElemFunc IS) (Xsum fn n) (LsumStable fn fnL n)) (LabsStable (ElemFunc IS) (fn (S n)) (fnL (S n)))))). + clear IHn. apply INonDecreasing. intros. destruct (fn (S n)), (Xsum fn n), xF, y ; simpl. apply (CRle_trans _ _ _ (CRabs_triang _ _)). apply CRplus_le_compat. rewrite (DomainProp0 x d d1). apply CRle_refl. rewrite (DomainProp x d0 d2). apply CRle_refl. + rewrite Iadditive. apply CRplus_le_compat. apply IHn. apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions