proposition: Lemma UC_compare_integrals_limit : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (a b : CRcarrier R) (leab : a <= b) (n : nat) (eps : CRcarrier R) (epsPos : 0 < eps) (cont_mod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f cont_mod), PartitionMesh (ipt_seq (IntervalEquiPartition a b n leab)) (S (ipt_last (IntervalEquiPartition a b n leab))) < cont_mod eps epsPos -> CRabs _ (IntegralFiniteSum f (ipt_seq (IntervalEquiPartition a b n leab)) (ipt_seq (IntervalEquiPartition a b n leab)) (ipt_last (IntervalEquiPartition a b n leab)) - UC_integral f a b cont_mod fCont leab) <= eps * (b-a).
proof: Proof. intros. assert (forall k:nat, 0 < CR_of_Q R (1 # Pos.of_nat (S k))) as kPos. { intros. apply CR_of_Q_lt. reflexivity. } assert (forall k:nat, let (q,_) := CRup_nat ((b-a) * (CRinv R (cont_mod _ (kPos k)) (inr ((fst fCont) _ (kPos k))))) in CRabs _ (IntegralFiniteSum f (ipt_seq (IntervalEquiPartition a b n leab)) (ipt_seq (IntervalEquiPartition a b n leab)) (ipt_last (IntervalEquiPartition a b n leab)) - IntegralFiniteSum f (ipt_seq (IntervalEquiPartition a b (max k q) leab)) (ipt_seq (IntervalEquiPartition a b (max k q) leab)) (ipt_last (IntervalEquiPartition a b (max k q) leab))) <= (eps + (CR_of_Q R (1# Pos.of_nat (S k)))) * (b-a)). { intro k. destruct (CRup_nat ((b-a) * (CRinv R (cont_mod _ (kPos k)) (inr ((fst fCont) _ (kPos k)))))) as [q qmaj]. assert (0 < S n * S (max k q))%nat as sisjPos. apply Nat.mul_pos_pos; apply le_n_S, Nat.le_0_l. apply (UC_compare_integrals f a b _ _ cont_mod _ _ (IntervalEquiPartition a b (pred (S n * S (max k q))) leab) epsPos (kPos k) (fun i => S (max k q) * i)%nat (fun i => S n * i)%nat fCont). - split. intros. unfold IntervalEquiPartition, ipt_seq. rewrite Nat.succ_pred. apply CRplus_morph. reflexivity. apply CRmult_morph. reflexivity. apply CR_of_Q_morph. rewrite Nat2Z.inj_mul, Nat2Pos.inj_mul. unfold Qeq, Qnum, Qden. do 2 rewrite <- positive_nat_Z. rewrite Pos2Nat.inj_mul. rewrite Nat2Pos.id. rewrite Nat2Pos.id. rewrite Nat2Z.inj_mul. ring. discriminate. discriminate. discriminate. discriminate. discriminate. split. intros. apply Nat.mul_lt_mono_pos_l. apply le_n_S, Nat.le_0_l. exact H0. unfold IntervalEquiPartition, ipt_last. intros. rewrite Nat.succ_pred. rewrite Nat.mul_comm. apply Nat.mul_le_mono_nonneg_r. apply Nat.le_0_l. exact H0. intro abs. rewrite abs in sisjPos. inversion sisjPos. - split. intros. unfold IntervalEquiPartition, ipt_seq. rewrite Nat.succ_pred. apply CRplus_morph. reflexivity. apply CRmult_morph. reflexivity. apply CR_of_Q_morph. rewrite Nat2Z.inj_mul, Nat2Pos.inj_mul. unfold Qeq, Qnum, Qden. do 2 rewrite <- positive_nat_Z. rewrite Pos2Nat.inj_mul. rewrite Nat2Pos.id. rewrite Nat2Pos.id. rewrite Nat2Z.inj_mul. ring. discriminate. discriminate. discriminate. discriminate. discriminate. split. intros. apply Nat.mul_lt_mono_pos_l. apply le_n_S, Nat.le_0_l. exact H0. unfold IntervalEquiPartition, ipt_last. intros. rewrite Nat.succ_pred. apply Nat.mul_le_mono_nonneg_l. apply Nat.le_0_l. exact H0. intro abs. rewrite abs in sisjPos. inversion sisjPos. - exact H. - rewrite EquiPartitionMesh. apply (CRle_lt_trans _ ((b - a) * CR_of_Q R (1# Pos.of_nat (S q)))). apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat. exact leab. apply CRle_refl. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. rewrite Nat2Pos.id. apply le_n_S, Nat.le_max_r. discriminate. discriminate. apply (CRmult_lt_compat_r (cont_mod _ (kPos k))) in qmaj. rewrite CRmult_assoc, CRinv_l, CRmult_1_r in qmaj. apply (CRmult_lt_reg_l (INR (S q))). apply CR_of_Q_lt; reflexivity. rewrite CRmult_comm, CRmult_assoc. unfold INR. rewrite <- CR_of_Q_mult. setoid_replace ((1 # Pos.of_nat (S q)) * (Z.of_nat (S q) # 1))%Q with 1%Q. rewrite CRmult_1_r. apply (CRlt_le_trans _ _ _ qmaj). apply CRmult_le_compat_r. apply CRlt_asym. destruct fCont. apply c. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, le_S, Nat.le_refl. unfold Qmult, Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_l. rewrite Z.mul_1_r, <- positive_nat_Z. apply f_equal. rewrite Pos.mul_1_r. rewrite Nat2Pos.id. reflexivity. discriminate. destruct fCont. apply c. } apply (CR_cv_le (fun k => let (q, _) := CRup_nat ((b - a) * (CRinv R (cont_mod (CR_of_Q R (1 # Pos.of_nat (S k))) (kPos k)) (inr (fst fCont (CR_of_Q R (1 # Pos.of_nat (S k))) (kPos k))))) in CRabs _ (IntegralFiniteSum f (ipt_seq (IntervalEquiPartition a b n leab)) (ipt_seq (IntervalEquiPartition a b n leab)) (ipt_last (IntervalEquiPartition a b n leab)) - IntegralFiniteSum f (ipt_seq (IntervalEquiPartition a b (Init.Nat.max k q) leab)) (ipt_seq (IntervalEquiPartition a b (Init.Nat.max k q) leab)) (ipt_last (IntervalEquiPartition a b (Init.Nat.max k q) leab)))) (fun k => (eps + CR_of_Q R (1 # Pos.of_nat (S k))) * (b - a))). - intros. specialize (H0 n0). destruct (CRup_nat ((b - a) * (CRinv R (cont_mod (CR_of_Q R (1 # Pos.of_nat (S n0))) (kPos n0)) (inr (fst fCont (CR_of_Q R (1 # Pos.of_nat (S n0))) (kPos n0)))))). exact H0. - intros eta. unfold UC_integral. destruct (CR_complete R (fun last : nat => IntegralFiniteSum f (fun n1 : nat => a + (b - a) * CR_of_Q R (Z.of_nat n1 # Pos.of_nat (S last))) (fun n1 : nat => a + (b - a) * CR_of_Q R (Z.of_nat n1 # Pos.of_nat (S last))) last) (UC_integral_cauchy f a b cont_mod fCont leab)). specialize (c eta) as [N u]. exists N. intros n0 H1. destruct (CRup_nat ((b - a) * (CRinv R (cont_mod (CR_of_Q R (1 # Pos.of_nat (S n0))) (kPos n0)) (inr (fst fCont (CR_of_Q R (1 # Pos.of_nat (S n0))) (kPos n0)))))). apply (CRle_trans _ _ _ (CRabs_triang_inv2 _ _)). setoid_replace (IntegralFiniteSum f (ipt_seq (IntervalEquiPartition a b n leab)) (ipt_seq (IntervalEquiPartition a b n leab)) (ipt_last (IntervalEquiPartition a b n leab)) - IntegralFiniteSum f (ipt_seq (IntervalEquiPartition a b (Init.Nat.max n0 x0) leab)) (ipt_seq (IntervalEquiPartition a b (Init.Nat.max n0 x0) leab)) (ipt_last (IntervalEquiPartition a b (Init.Nat.max n0 x0) leab)) - (IntegralFiniteSum f (ipt_seq (IntervalEquiPartition a b n leab)) (ipt_seq (IntervalEquiPartition a b n leab)) (ipt_last (IntervalEquiPartition a b n leab)) - x)) with (-(IntegralFiniteSum f (ipt_seq (IntervalEquiPartition a b (Init.Nat.max n0 x0) leab)) (ipt_seq (IntervalEquiPartition a b (Init.Nat.max n0 x0) leab)) (ipt_last (IntervalEquiPartition a b (Init.Nat.max n0 x0) leab)) - x)). rewrite CRabs_opp. apply u. unfold IntervalEquiPartition, ipt_last. apply (Nat.le_trans _ _ _ H1), Nat.le_max_l. unfold CRminus. do 2 rewrite CRopp_plus_distr. rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_l. reflexivity. - apply CR_cv_scale. intros i. exists (Pos.to_nat i). intros. setoid_replace (eps + CR_of_Q R (1 # Pos.of_nat (S i0)) - eps) with (CR_of_Q R (1 # Pos.of_nat (S i0))). rewrite CRabs_right. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply (Nat.le_trans _ _ _ H1), le_S, Nat.le_refl. discriminate. apply CR_of_Q_le. discriminate. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont