proposition: Lemma IntegralAbsLimit : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), CR_cv _ (fun n : nat => (Iabs _ (LsumStable (IntFn (let (i,_) := fInt in i)) (IntFnL (let (i,_) := fInt in i)) n))) (Integral (IntegrableAbs fInt)).
proof: Proof. intros IS. assert (CRabs (RealT (ElemFunc IS)) 0 == 0) as CReal_abs_R0. { rewrite CRabs_right. reflexivity. apply CRle_refl. } intros. unfold Integral, IntegrableAbs, IntegrableOpContract, IntegralRepresentationOpContract. destruct fInt as [x p], (IabsOpContract (IntFn x) (IntFnL x) (CRabs _) (CRabs_morph_prop _) (LabsStable (ElemFunc IS)) CRabs_triang_inv2 (CRabs_right 0 (CRle_refl 0)) (IntAbsSum x) (IntAbsSumCv x)). do 2 rewrite IntegralRepresentationWeaveSum. rewrite IntegralHomogeneousHalf, <- CRopp_mult_distr_r, CRmult_1_r, CRplus_opp_r, CRplus_0_r. destruct x as [fn fnL sumIAbsFn H]; unfold IntFn, IntFnL. apply (CR_cv_eq _ (CRsum (fun n : nat => I IS (telescopicOp (X (ElemFunc IS)) fn (CRabs _) (CRabs_morph_prop _) n) (telescopicOpL fn fnL (CRabs _) (CRabs_morph_prop _) (fun (g : PartialFunction (X (ElemFunc IS))) (gL : L (ElemFunc IS) g) => LabsStable (ElemFunc IS) g gL) n)))). 2: apply (IntegralCv {| IntFn := telescopicOp (X (ElemFunc IS)) fn (CRabs _) (CRabs_morph_prop _); IntFnL := telescopicOpL fn fnL (CRabs _) (CRabs_morph_prop _) (fun (g : PartialFunction (X (ElemFunc IS))) (gL : L (ElemFunc IS) g) => LabsStable (ElemFunc IS) g gL); IntAbsSum := x0; IntAbsSumCv := s |}). intro n. rewrite intTelescopicAbs. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase