proposition: Lemma AbsRepresentation : forall (IS : IntegrationSpace) (f : PartialFunction (X (ElemFunc IS))) (eps : CRcarrier (RealT (ElemFunc IS))) (fInt : IntegrableFunction f), 0 < eps -> { intRepres : IntegralRepresentation & prod (PartialRestriction (XinfiniteSumAbs (IntFn intRepres)) f) (IntAbsSum intRepres <= Integral (IntegrableAbs fInt) + eps) }.
proof: Proof. intros. pose proof (IntegralAbsLimit f fInt) as IabsLimit. destruct fInt as [[fn fnL sumIAbsFn lim] [inj restr]] eqn:desFint. unfold IntFn, IntFnL in IabsLimit. unfold IntFn in inj, restr. assert (forall N:nat, series_cv (fun k : nat => Iabs (PackFirstFunctions (X (ElemFunc IS)) fn N k) (PackFirstFunctionsL IS fn fnL N k)) (sumIAbsFn - CRsum (fun n : nat => Iabs (fn n) (fnL n)) N + Iabs (Xsum fn N) (LsumStable fn fnL N))) as limPack. { intro N. apply (series_cv_eq (fun n => match n with | O => Iabs (Xsum fn N) (LsumStable fn fnL N) | _ => Iabs (fn (N+n)%nat) (fnL (N+n)%nat) end)). intro n. destruct n; reflexivity. apply (PackSeriesCV (fun n : nat => Iabs (fn n) (fnL n))). assumption. } pose (fun N:nat => Build_IntegralRepresentation IS (PackFirstFunctions (X (ElemFunc IS)) fn N) (PackFirstFunctionsL IS fn fnL N) (sumIAbsFn - CRsum (fun n => Iabs (fn n) (fnL n)) N + Iabs (Xsum fn N) (LsumStable fn fnL N)) (limPack N)) as represPack. assert (forall N:nat, PartialRestriction (XinfiniteSumAbs (IntFn (represPack N))) f) as IsRepresPack. { intro N. unfold represPack, IntFn. destruct (domainInfiniteSumPackInc (X (ElemFunc IS)) fn N) as [inc app]. split. intros x xdf. apply inj, inc. exact xdf. intros. specialize (app x xD (inc x xD)). rewrite app. apply restr. } destruct (CRup_nat (CR_of_Q _ 2 * CRinv _ eps (inr H))) as [epsN majEpsN]. pose proof (lim (Pos.of_nat epsN)) as [N limN]. exists (represPack N). split. apply IsRepresPack. apply (CRle_trans _ (Iabs (Xsum fn N) (LsumStable fn fnL N) + eps * CR_of_Q _ (1#2))). - simpl. specialize (limN N (Nat.le_refl N)). rewrite <- (CRplus_comm (eps * CR_of_Q _ (1#2))). apply CRplus_le_compat. 2: apply CRle_refl. rewrite CRabs_minus_sym in limN. apply (CRle_trans _ (CRabs _ (sumIAbsFn - CRsum (fun k : nat => Iabs (fn k) (fnL k)) N))). apply CRle_abs. apply (CRle_trans _ (CR_of_Q _ (1# Pos.of_nat epsN))). assumption. apply (CRmult_lt_compat_r eps) in majEpsN. rewrite CRmult_assoc, CRinv_l, CRmult_1_r in majEpsN. 2: exact H. apply CRlt_asym. apply (CRmult_lt_reg_r (CR_of_Q _ 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- (CR_of_Q_mult _ (1#2)). setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. rewrite CRmult_1_r. apply (CRmult_lt_reg_l (CR_of_Q _ (Z.pos (Pos.of_nat epsN) #1))). apply CR_of_Q_lt; reflexivity. rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((Z.pos (Pos.of_nat epsN) # 1) * (1 # Pos.of_nat epsN))%Q with 1%Q. rewrite CRmult_1_l. apply (CRlt_le_trans _ _ _ majEpsN). apply CRmult_le_compat_r. apply CRlt_asym, H. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. destruct epsN. discriminate. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite SuccNat2Pos.id_succ, Nat2Pos.id. apply Nat.le_refl. discriminate. unfold Qmult, Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. reflexivity. - apply (CR_cv_bound_down (fun m => Iabs (Xsum fn m) (LsumStable fn fnL m) + eps) _ _ (S N)). intros m maj. apply (CRplus_le_reg_l (- Iabs (Xsum fn m) (LsumStable fn fnL m))). rewrite <- CRplus_assoc. rewrite <- CRplus_assoc. rewrite CRplus_opp_l. rewrite CRplus_0_l. apply (CRplus_le_reg_r (- (eps * CR_of_Q _ (1#2)))). rewrite CRplus_assoc. rewrite CRplus_opp_r. rewrite CRplus_0_r. apply (CRle_trans _ (Iabs (Xminus (Xsum fn m) (Xsum fn N)) (LminusStable _ _ (LsumStable fn fnL m) (LsumStable fn fnL N)))). apply IabsMinusMaj. destruct (Nat.le_exists_sub N m) as [k [add _]]. apply le_S in maj. apply le_S_n in maj. assumption. subst m. destruct k. exfalso. exact (Nat.lt_irrefl N maj). apply (CRle_trans _ (Iabs (Xsum (fun a => fn (S N + a)%nat) k) (LsumStable (fun a => fn (S N + a)%nat) (fun a => fnL (S N + a)%nat) k))). apply INonDecreasing. intros. rewrite applyXabs. rewrite applyXabs. remember (S k + N)%nat. rewrite Nat.add_comm in Heqn. replace (N + S k)%nat with (S N + k)%nat in Heqn. subst n. rewrite (Xsum_assocMinus fn N k x _ y). apply CRle_refl. rewrite Nat.add_succ_r. reflexivity. apply (CRle_trans _ (I IS (Xsum (fun a : nat => Xabs (fn (S N + a)%nat)) k) (LsumStable _ (fun a => LabsStable (ElemFunc IS) (fn (S N + a)%nat) (fnL (S N + a)%nat)) k))). apply INonDecreasing. intros. apply XmultiTriangleIneg. rewrite IadditiveIterate. rewrite <- (CRsum_eq (fun n0 : nat => I IS (Xabs (fn (N + S n0)%nat)) (LabsStable (ElemFunc IS) (fn (N + S n0)%nat) (fnL (N + S n0)%nat)))). apply (series_cv_remainder_maj (fun n0 : nat => I IS (Xabs (fn n0)) (LabsStable (ElemFunc IS) (fn n0) (fnL n0))) sumIAbsFn). apply lim. rewrite <- (CRplus_opp_r (eps * CR_of_Q _ (1 # 2))). apply CRplus_lt_compat_r. rewrite <- (CRmult_1_r eps). rewrite CRmult_assoc. apply CRmult_lt_compat_l. assumption. rewrite CRmult_1_l. apply (CRmult_lt_reg_l (CR_of_Q _ 2)). apply CR_of_Q_lt; reflexivity. rewrite <- CR_of_Q_mult. rewrite CRmult_1_r. apply CR_of_Q_lt. reflexivity. intro n. apply integralPositive. intros x xdf. rewrite applyXabs. apply CRabs_pos. apply CRlt_asym. setoid_replace (eps + - (eps * CR_of_Q _ (1 # 2))) with (eps * CR_of_Q _ (1 # 2)). apply (CRmult_lt_compat_r eps) in majEpsN. rewrite CRmult_assoc, CRinv_l, CRmult_1_r in majEpsN. 2: exact H. apply (CRle_lt_trans _ (CR_of_Q _ (1 # Pos.of_nat epsN))). apply limN. apply Nat.le_refl. apply (CRmult_lt_reg_r (CR_of_Q _ 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- (CR_of_Q_mult _ (1#2)). setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. rewrite CRmult_1_r. apply (CRmult_lt_reg_l (CR_of_Q _ (Z.pos (Pos.of_nat epsN) #1))). apply CR_of_Q_lt; reflexivity. rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((Z.pos (Pos.of_nat epsN) # 1) * (1 # Pos.of_nat epsN))%Q with 1%Q. rewrite CRmult_1_l. apply (CRlt_le_trans _ _ _ majEpsN). apply CRmult_le_compat_r. apply CRlt_asym, H. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. destruct epsN. discriminate. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite SuccNat2Pos.id_succ, Nat2Pos.id. apply Nat.le_refl. discriminate. unfold Qmult, Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. reflexivity. rewrite <- (CRmult_1_r eps), CRopp_mult_distr_r. rewrite CRmult_assoc, <- CRmult_plus_distr_l. apply CRmult_morph. rewrite CRmult_1_r. reflexivity. rewrite CRmult_1_l. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus. apply CR_of_Q_morph. reflexivity. intros. rewrite Nat.add_succ_r. reflexivity. apply CR_cv_plus. assumption. apply CR_cv_const. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions