proposition: Lemma IntegrableContinuous : forall {IS : IntegrationSpace} (h : PartialFunction (X (ElemFunc IS))) (hn : nat -> PartialFunction (X (ElemFunc IS))) (hL : IntegrableFunction h) (hnL : forall n:nat, IntegrableFunction (hn n)), (forall n:nat, nonNegFunc (hn n)) -> series_cv_lim_lt (fun n => Integral (hnL n)) (Integral hL) -> { x : CommonPointFunSeq _ h hn & series_cv_lim_lt (fun n => partialApply (hn n) _ (cpxFn _ _ _ x n)) (partialApply h _ (cpxF _ _ _ x)) }.
proof: Proof. intros. destruct H0, p. destruct (Break_lt_3_eps _ _ c) as [eps [epsPos epsMaj]]. assert (forall n:nat, 0 < eps * CR_of_Q _ (1#2) * CRpow (CR_of_Q _ (1#2)) n). { intro n. rewrite <- (CRmult_0_r eps). rewrite CRmult_assoc. apply CRmult_lt_compat_l. exact epsPos. rewrite <- (CRmult_0_r (CR_of_Q _ (1#2))). apply CRmult_lt_compat_l. apply CR_of_Q_lt. reflexivity. apply CRpow_gt_zero. apply CR_of_Q_lt. reflexivity. } pose (fun n => IntFn (let (r,_) := AbsRepresentation IS (hn n) (eps*CR_of_Q _ (1#2)*CRpow (CR_of_Q _ (1#2)) n) (hnL n) (H0 n) in r)) as phink. pose ( fun n k : nat => let s1 := AbsRepresentation IS (hn n) (eps * CR_of_Q _ (1#2) * CRpow (CR_of_Q _ (1 # 2)) n) (hnL n) (H0 n) in let (x0, _) as s2 return (L (ElemFunc IS) (IntFn (let (r, _) := s2 in r) k)) := s1 in let X := IntFnL x0 in X k) as phinkL. assert (forall n:nat, { l : CRcarrier _ & (series_cv (fun k => I IS (Xabs (phink n k)) (LabsStable _ _ (phinkL n k))) l) * (l <= Integral (hnL n) + eps * CR_of_Q _ (1#2)* CRpow (CR_of_Q _ (1#2)) n)%ConstructiveReals }%type) as phinkAbsCv. { intro n. unfold phink, phinkL. destruct (AbsRepresentation IS (hn n) (eps * CR_of_Q _ (1#2) * CRpow (CR_of_Q _ (1 # 2)) n) (hnL n) (H0 n)). exists (IntAbsSum x0). split. exact (IntAbsSumCv x0). destruct p. setoid_replace (Integral (hnL n)) with (Integral (IntegrableAbs (hnL n))). exact c0. apply IntegralExtensional. intros. simpl. rewrite CRabs_right. apply DomainProp. apply H. } assert (forall n:nat, PartialRestriction (XinfiniteSumAbs (phink n)) (hn n)) as phinkRes. { intros n. unfold phink. destruct (AbsRepresentation IS (hn n) (eps * CR_of_Q _ (1#2)*CRpow (CR_of_Q _ (1 # 2)) n) (hnL n) (H0 n)). apply p. } destruct hL as [x0 psiRes], x0 as [psik psikL IntAbsSum IntAbsSumCv]. unfold Integral in epsMaj, c. unfold IntFn in psiRes. assert (CR_cv _ (fun K => I IS (Xsum psik K) (LsumStable psik psikL K)) (IntegralSeries {| IntFn := psik; IntFnL := psikL; IntAbsSum := IntAbsSum; IntAbsSumCv := IntAbsSumCv |})) as psiInt. { apply (CR_cv_eq _ (CRsum (fun K => I IS (psik K) (psikL K)))). intro n. rewrite IadditiveIterate. reflexivity. unfold IntegralSeries. destruct ( series_cv_maj (fun n : nat => I IS (psik n) (psikL n)) (fun k : nat => Iabs (psik k) (psikL k)) IntAbsSum (fun n : nat => integralAbsMaj (psik n) (psikL n)) IntAbsSumCv). destruct p. exact s0. } assert ({K : nat & prod (IntegralSeries {| IntFn := psik; IntFnL := psikL; IntAbsSum := IntAbsSum; IntAbsSumCv := IntAbsSumCv |} < I IS (Xsum psik K) (LsumStable psik psikL K) + eps) (series_cv_lim_lt (fun k => I IS (Xabs (psik (k+S K)%nat)) (LabsStable _ _ (psikL _))) eps) }). { pose proof (Un_cv_nat_real _ _ psiInt eps epsPos) as [i imaj]. destruct (series_cv_remainder_cv _ _ eps IntAbsSumCv epsPos) as [j jmaj]. exists (max i j). split. specialize (imaj (max i j) (Nat.le_max_l _ _)). rewrite CRabs_minus_sym in imaj. apply (CRplus_lt_reg_l _ (- I IS (Xsum psik (Init.Nat.max i j)) (LsumStable psik psikL (Init.Nat.max i j)))). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l, CRplus_comm. apply (CRle_lt_trans _ _ _ (CRle_abs _)). exact imaj. apply jmaj. apply le_S, Nat.le_max_r. } destruct H1 as [K kmaj]. assert (forall n:nat, L (ElemFunc IS) (diagSeq (fun n k => Xabs (phink n k)) n)) as L1. { apply diagSeqL. intros n k. apply LabsStable. apply phinkL. } assert (forall k:nat, L (ElemFunc IS) (Xabs (psik (k+S K)%nat))) as L2. { intro k. apply LabsStable. apply psikL. } destruct (IcontinuousWeave (Xsum psik K) (diagSeq (fun n k => Xabs (phink n k))) (fun k => Xabs (psik (k+S K)%nat)) (LsumStable psik psikL K) L1 L2) as [x0 xcv]. - intro n. unfold diagSeq. destruct (diagPlaneInv n). intros y ydf. apply CRabs_pos. - intros n y ydf. apply CRabs_pos. - destruct kmaj, s0, p. destruct (series_cv_maj (fun n => let (l,_):=phinkAbsCv n in l) (fun n => Integral (hnL n) + eps * CR_of_Q _ (1#2) * CRpow (CR_of_Q _ (1 # 2)) n) (x + eps)). intro n. destruct (phinkAbsCv n). simpl. destruct p. rewrite CRabs_right. exact c2. apply (series_cv_nonneg (fun k : nat => I IS (Xabs (phink n k)) (LabsStable _ _ (phinkL n k)))). intros. apply integralPositive. intros y ydf. apply CRabs_pos. exact s1. apply series_cv_plus. exact s. apply (series_cv_eq (fun n : nat => CRpow (CR_of_Q _ (1 # 2)) n * (eps*CR_of_Q _ (1#2)))). intro n. apply CRmult_comm. apply (CR_cv_proper _ (CR_of_Q _ 2*(eps*CR_of_Q _ (1#2)))). apply series_cv_scale. apply GeoHalfTwo. rewrite CRmult_comm, CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1#2) * 2)%Q with 1%Q. rewrite CRmult_1_r. reflexivity. reflexivity. destruct p. exists (x1, x0). unfold fst, snd. split. split. apply (series_cv_eq (diagSeq (fun n k : nat => I IS (Xabs (phink n k)) (LabsStable _ _ (phinkL n k))))). intro n. unfold diagSeq. generalize (L1 n). intros. unfold diagSeq in l. destruct (diagPlaneInv n). apply IExtensional. intros. apply DomainProp. apply (DiagSeqInfiniteSumColPos _ (fun n : nat => let (l, _) := phinkAbsCv n in l)). intros n k. apply integralPositive. intros y ydf. apply CRabs_pos. intro n. destruct (phinkAbsCv n). apply p. exact s1. apply (series_cv_eq (fun k : nat => I IS (Xabs (psik (k + S K)%nat)) (LabsStable (ElemFunc IS) (psik (k + S K)%nat) (psikL (k + S K)%nat)))). intro n. apply IExtensional. intros. apply DomainProp. exact s0. apply (CRplus_le_compat_l (eps+eps)) in c2. do 2 rewrite (CRplus_comm (eps+eps)) in c2. rewrite CRplus_assoc in c2. setoid_replace (eps + (eps+eps)) with (CR_of_Q _ 3 * eps) in c2. pose proof (CRle_lt_trans _ _ _ c2 epsMaj). clear c2. pose proof (CRlt_trans _ _ _ H1 c0). clear H1. rewrite <- CRplus_assoc in H2. apply CRplus_lt_reg_r in H2. apply (CRlt_trans _ (x1 + eps)). apply CRplus_lt_compat_l. exact c1. exact H2. setoid_replace (CR_of_Q (RealT (ElemFunc IS)) 3) with (1+1+CR_of_Q (RealT (ElemFunc IS)) 1). do 2 rewrite CRmult_plus_distr_r. rewrite CRmult_1_l, CRplus_assoc. reflexivity. do 2 rewrite <- CR_of_Q_plus. reflexivity. - destruct x0 as [cpx cpxF cpxFn cpxGn]. simpl in xcv. destruct xcv, p, x0. simpl in p. destruct p. simpl in c0. assert (forall k:nat, Domain (psik k) cpx) as cpxDpsik. { intro k. destruct (le_lt_dec k K). apply (domainXsumIncReverse _ _ K). exact cpxF. exact l. rewrite <- (Nat.sub_add (S K) k). apply cpxGn. exact l. } assert (forall k:nat, Domain (diagSeq phink k) cpx) as cpxDdiagBis. { intro k. unfold diagSeq. destruct (diagPlaneInv k). apply (diagSeqDomain _ (fun n k => Xabs (phink n k)) _ cpxFn). } assert (Domain (XinfiniteSumAbs psik) cpx). { exists cpxDpsik. apply (Rcv_cauchy_mod _ (c2 + CRsum (fun k => partialApply (Xabs (psik k)) cpx (cpxDpsik k)) K)). apply series_cv_shift. apply (series_cv_eq (fun n : nat => CRabs _ (partialApply (psik (n + S K)%nat) cpx (cpxGn n)))). intros. apply CRabs_morph. rewrite (Nat.add_comm (S K)). apply DomainProp. exact s1. } assert (forall n:nat, Domain (XinfiniteSumAbs (phink n)) cpx). { intro n. apply (domainInfiniteSumAbsDiag _ (fun n0 k : nat => phink n0 k) n). exists cpxDdiagBis. apply (Rcv_cauchy_mod _ c1). apply (series_cv_eq (fun n : nat => partialApply (diagSeq (fun n0 k : nat => Xabs (phink n0 k)) n) cpx (cpxFn n))). 2: exact s0. apply applyDiagAbs. } assert (forall n:nat, Domain (hn n) cpx) as cpxDhn. { intro n. apply phinkRes. apply H2. } destruct psiRes. exists (Build_CommonPointFunSeq _ _ _ _ cpx (d _ H1) cpxDhn). simpl. assert ({ l : CRcarrier _ & prod (series_cv (fun n => partialApply _ cpx (cpxDhn n)) l) (l <= c1) }). { destruct (DiagSeqInfiniteSum (fun n k => partialApply (phink n k) cpx (diagSeqDomain _ phink cpx cpxDdiagBis n k)) (fun n => partialApply (hn n) cpx (cpxDhn n)) c1). apply (series_cv_eq (fun n : nat => partialApply (diagSeq (fun n0 k : nat => Xabs (phink n0 k)) n) cpx (cpxFn n))). intro n. rewrite (applyDiagAbs phink cpx cpxFn cpxDdiagBis). unfold diagSeq. generalize (cpxDdiagBis n). intros. unfold diagSeq in d0. destruct (diagPlaneInv n). apply CRabs_morph. apply DomainProp. exact s0. intro n. apply (series_cv_eq (fun k => partialApply (phink n k) cpx (domainInfiniteSumAbsIncReverse (phink n) cpx (H2 n) k))). intro i. apply DomainProp. apply applyInfiniteSumAbs. apply phinkRes. exists x0. split; apply p. } destruct H3, p. assert ({ l : CRcarrier _ & prod (series_cv (fun n => partialApply _ cpx (cpxDpsik (n+S K)%nat)) l) (CRabs _ l <= c2) }). { destruct (series_cv_abs (fun n => partialApply _ cpx (cpxDpsik (n+S K)%nat))). apply (Rcv_cauchy_mod _ c2). apply (series_cv_eq (fun n : nat => CRabs _ (partialApply (psik (n + S K)%nat) cpx (cpxGn n)))). intro n. apply CRabs_morph. apply DomainProp. exact s1. exists x1. split. exact s3. apply (series_cv_triangle (fun n => partialApply _ cpx (cpxDpsik (n+S K)%nat))). exact s3. apply (series_cv_eq (fun n : nat => CRabs _ (partialApply (psik (n + S K)%nat) cpx (cpxGn n)))). intro n. apply CRabs_morph. apply DomainProp. exact s1. } destruct H3. assert (x0 - x1 < partialApply (Xsum psik K) cpx cpxF). { apply (CRle_lt_trans _ (c1 + c2)). 2: exact c0. apply CRplus_le_compat. exact c4. apply (CRle_trans _ (CRabs _ x1)). rewrite <- CRabs_opp. apply CRle_abs. apply p. } destruct p. clear c1 s0 c0 c4. clear c2 s1 c5. apply (CRplus_lt_compat_r x1) in H3. unfold CRminus in H3. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r in H3. exists x0. split. exact s2. rewrite (applyXsum _ K cpx _ cpxDpsik), CRplus_comm in H3. rewrite <- (c3 cpx H1). setoid_replace (partialApply (XinfiniteSumAbs psik) cpx H1) with (x1 + CRsum (fun k : nat => partialApply (psik k) cpx (cpxDpsik k)) K). exact H3. apply applyInfiniteSumAbs. apply (series_cv_eq (fun n : nat => partialApply (psik n) cpx (cpxDpsik n))). intro n. apply DomainProp. apply series_cv_shift. apply (series_cv_eq (fun n : nat => partialApply (psik (n + S K)%nat) cpx (cpxDpsik (n + S K)%nat))). intro n. rewrite Nat.add_comm. reflexivity. exact s3. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions