proposition: Lemma UC_integral_cauchy : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (a b : CRcarrier R) (cont_mod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R), UniformCont f cont_mod -> a <= b -> CR_cauchy R (fun last : nat => IntegralFiniteSum f (fun n => a + (b-a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n => a + (b-a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last).
proof: Proof. intros. intros n. assert (0 < CR_of_Q R (Z.pos (2*n) # 1) * (1+b-a)) as invStepPos. { apply CRmult_lt_0_compat. apply CR_of_Q_lt. reflexivity. apply (CRlt_le_trans _ (1+0)). rewrite CRplus_0_r. apply CRzero_lt_one. unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat. exact H0. apply CRle_refl. } assert (0 < CRinv R (CR_of_Q R (Z.pos (2*n) # 1) * (1+b-a)) (inr invStepPos)) as stepPos. { apply CRinv_0_lt_compat. exact invStepPos. } destruct H. destruct (CRup_nat ((b-a) * (CRinv R (cont_mod _ stepPos) (inr (c _ stepPos))))) as [p pmaj]. exists p. intros. apply (CRle_trans _ (((CRinv R (CR_of_Q R (Z.pos (2*n) # 1) * (1+b-a)) (inr invStepPos)) + (CRinv R (CR_of_Q R (Z.pos (2*n) # 1) * (1+b-a)) (inr invStepPos))) * (b-a))). assert (0 < S i * S j)%nat as sisjPos. { apply Nat.mul_pos_pos; apply le_n_S, Nat.le_0_l. } apply (UC_compare_integrals f a b (CRinv R (CR_of_Q R (Z.pos (2*n) # 1) * (1+b-a)) (inr invStepPos)) (CRinv R (CR_of_Q R (Z.pos (2*n) # 1) * (1+b-a)) (inr invStepPos)) cont_mod (IntervalEquiPartition a b i H0) (IntervalEquiPartition a b j H0) (IntervalEquiPartition a b (pred (S i * S j)) H0) stepPos stepPos (fun n => S j * n)%nat (fun n => S i * n)%nat). split; assumption. - 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 H2. 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 H2. 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 H2. unfold IntervalEquiPartition, ipt_last. intros. rewrite Nat.succ_pred. apply Nat.mul_le_mono_nonneg_l. apply Nat.le_0_l. exact H2. intro abs. rewrite abs in sisjPos. inversion sisjPos. - rewrite EquiPartitionMesh. unfold IntervalEquiPartition, ipt_last. apply (CRle_lt_trans _ ((b - a) * CR_of_Q R (1 # Pos.of_nat (S p)))). apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat. exact H0. 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, H. discriminate. discriminate. apply (CRmult_lt_compat_r (cont_mod _ stepPos)) in pmaj. rewrite CRmult_assoc, CRinv_l, CRmult_1_r in pmaj. apply (CRmult_lt_reg_l (INR (S p))). 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 p)) * (Z.of_nat (S p) # 1))%Q with 1%Q. rewrite CRmult_1_r. apply (CRlt_le_trans _ _ _ pmaj). apply CRmult_le_compat_r. apply CRlt_asym, 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. apply c. - rewrite EquiPartitionMesh. unfold IntervalEquiPartition, ipt_last. apply (CRle_lt_trans _ ((b - a) * CR_of_Q R (1 # Pos.of_nat (S p)))). apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat. exact H0. 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, H1. discriminate. discriminate. apply (CRmult_lt_compat_r (cont_mod _ stepPos)) in pmaj. rewrite CRmult_assoc, CRinv_l, CRmult_1_r in pmaj. apply (CRmult_lt_reg_l (INR (S p))). 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 p)) * (Z.of_nat (S p) # 1))%Q with 1%Q. rewrite CRmult_1_r. apply (CRlt_le_trans _ _ _ pmaj). apply CRmult_le_compat_r. apply CRlt_asym, 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. apply c. - rewrite <- (CRmult_1_r (CRinv R (CR_of_Q R (Z.pos (2 * n) # 1) * (1 + b - a)) (inr invStepPos))). rewrite <- CRmult_plus_distr_l. apply (CRmult_le_reg_l (CR_of_Q R (Z.pos (2 * n) # 1) * (1 + b - a))). exact invStepPos. do 2 rewrite <- CRmult_assoc. rewrite CRinv_r, CRmult_1_l. rewrite <- (CRmult_comm (1 + b - a)), CRmult_assoc. rewrite <- CR_of_Q_mult. setoid_replace ((Z.pos (2 * n) # 1) * (1 # n))%Q with 2%Q. rewrite CRmult_comm, <- CR_of_Q_plus. apply CRmult_le_compat_r. apply CR_of_Q_le. discriminate. rewrite <- (CRplus_0_l (b-a)). unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_r. apply CRlt_asym, CRzero_lt_one. unfold Qeq, Qnum, Qden. simpl. do 2 rewrite Pos.mul_1_r. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont