proposition: Lemma IntegralDense : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), Un_integral_cv _ f (IntegrableSum _ (fun n => IntegrableL _ (IntFnL (let (intRepres,_) := fInt in intRepres) n))) fInt.
proof: Proof. intros. destruct fInt as [intRepres lim]. intro p. pose proof (IntAbsSumCv intRepres p) as [n nmaj]. exists n. intros i H. apply (CRle_trans _ (Integral (IntegrableSelf (IntegralRepresentationShift (IntegralRepresentationAbs intRepres) i)))). - apply IntegralNonDecreasing. intros x xdf [xnlim cau]. destruct xdf. rewrite applyXabs, (applyXminus (Xsum (IntFn intRepres) i) f). simpl. assert (forall n0:nat, Domain (IntFn intRepres n0) x) as xdn. { intro j. destruct (le_lt_dec j i). exact (domainXsumIncReverse (IntFn intRepres) j i _ d l). unfold lt in l. simpl in xnlim. pose proof (xnlim (j - S i)%nat) as H0. replace (S (i + (j - S i)))%nat with j in H0. exact H0. symmetry. rewrite Nat.add_comm. rewrite <- Nat.add_succ_r. exact (Nat.sub_add (S i) j l). } destruct (series_cv_abs (fun n0 : nat => CRabs _ (partialApply (IntFn intRepres (S (i + n0))) x (xnlim n0))) cau) as [x0 s]. apply (series_cv_eq _ (fun n0 => CRabs _ (partialApply (IntFn intRepres (S (i + n0))) x (xdn (S i + n0)%nat)))) in s. apply (series_cv_shift (fun n0 : nat => CRabs _ (partialApply (IntFn intRepres n0) x (xdn n0))) i x0) in s. rewrite (applyXsum _ _ x _ xdn). rewrite <- (CRplus_0_r x0), <- (CRplus_opp_r (CRsum (fun n0 : nat => CRabs _ (partialApply (IntFn intRepres n0) x (xdn n0))) i)), <- CRplus_assoc. apply (series_cv_abs_remainder (fun n0 : nat => (partialApply (IntFn intRepres n0) x (xdn n0))) (partialApply f x d0) (x0 + CRsum (fun n0 : nat => CRabs _ (partialApply (IntFn intRepres n0) x (xdn n0))) i) i). 2: exact s. destruct lim. assert (Domain (XinfiniteSumAbs (IntFn intRepres)) x) as H0. { exists xdn. apply Rcv_cauchy_mod in s. exact s. } rewrite <- (c x H0). apply (series_cv_eq (fun n : nat => partialApply (IntFn intRepres n) x (domainInfiniteSumAbsIncReverse (IntFn intRepres) x H0 n))). 2: apply applyInfiniteSumAbs; reflexivity. intros. apply DomainProp. intros. apply CRabs_morph, DomainProp. - unfold Integral, IntegrableSelf. rewrite IntegralRepresentationShiftVal. rewrite IntegralRepresentationAbsVal. simpl. specialize (nmaj i H). rewrite CRabs_minus_sym in nmaj. apply (CRle_trans _ _ _ (CRle_abs _) nmaj). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions