proposition: Lemma x_RiemannInt : forall {R : ConstructiveReals} (a b : CRcarrier R) (leab : a <= b), UC_integral (fun x=> x) a b _ UC_x leab == (b*b - a*a) * CR_of_Q R (1#2).
proof: Proof. intros. unfold UC_integral. apply Rcauchy_complete_eq. apply (CR_cv_eq _ (fun n => a*(b-a) + (CR_of_Q R (Z.of_nat n # Pos.of_nat (S n))) * ((b-a) * (b-a) * CR_of_Q R (1#2)))). - intros. unfold IntegralFiniteSum. rewrite (CRsum_eq _ (fun k => a*(b-a) * CR_of_Q R (1# Pos.of_nat (S n)) + INR k * ((b-a)*(b-a) * CR_of_Q R (1# Pos.of_nat (S n * S n))))). + symmetry. rewrite sum_plus, sum_const. rewrite sum_scale, (CRmult_comm (CRsum (fun n0 => INR n0) n)). rewrite sum_INR. rewrite CRmult_assoc. setoid_replace (CR_of_Q R (1 # Pos.of_nat (S n)) * INR (S n)) with (CR_of_Q R 1). rewrite CRmult_1_r. apply CRplus_morph. reflexivity. rewrite <- (CRmult_comm ((b - a) * (b - a) * CR_of_Q R (1 # 2))). rewrite CRmult_assoc. rewrite (CRmult_assoc ((b-a)*(b-a))). apply CRmult_morph. reflexivity. rewrite CRmult_comm, (CRmult_comm ((INR n)*(INR (S n)))). rewrite (CRmult_assoc (CR_of_Q R (1#2))). apply CRmult_morph. reflexivity. unfold INR, CRealConstructive, CR_of_Q. do 2 rewrite <- CR_of_Q_mult. apply CR_of_Q_morph. rewrite Nat2Pos.inj_mul. unfold Qmult, Qeq, Qnum, Qden. rewrite Z.mul_1_r, Pos.mul_1_l. rewrite <- Z.mul_assoc. apply f_equal2. reflexivity. rewrite Pos2Z.inj_mul. apply f_equal2. 2: reflexivity. rewrite <- positive_nat_Z. rewrite Nat2Pos.id. reflexivity. discriminate. discriminate. discriminate. unfold INR. rewrite <- CR_of_Q_mult. apply CR_of_Q_morph. unfold Qmult, Qeq, Qnum, Qden. rewrite Pos.mul_1_r. rewrite Z.mul_1_l, Z.mul_1_l, Z.mul_1_r. rewrite <- positive_nat_Z. rewrite Nat2Pos.id. reflexivity. discriminate. + intros. setoid_replace (a + (b - a) * CR_of_Q R (Z.of_nat (S i) # Pos.of_nat (S n)) - (a + (b - a) * CR_of_Q R (Z.of_nat i # Pos.of_nat (S n)))) with ((b - a) * CR_of_Q R (1 # Pos.of_nat (S n))). rewrite CRmult_plus_distr_r. apply CRplus_morph. rewrite CRmult_assoc. reflexivity. unfold INR. rewrite Nat2Pos.inj_mul. setoid_replace (1 # Pos.of_nat (S n) * Pos.of_nat (S n))%Q with ((1 # Pos.of_nat (S n)) * (1 # Pos.of_nat (S n)))%Q. 2: reflexivity. rewrite CR_of_Q_mult. setoid_replace (Z.of_nat i # Pos.of_nat (S n))%Q with ((Z.of_nat i # 1) * (1# Pos.of_nat (S n)))%Q. rewrite CR_of_Q_mult. do 4 rewrite <- CRmult_assoc. apply CRmult_morph. 2: reflexivity. rewrite (CRmult_comm (b-a)). rewrite <- CRmult_assoc. do 2 rewrite (CRmult_assoc (CR_of_Q R (Z.of_nat i # 1) * (b - a))). apply CRmult_morph. reflexivity. apply CRmult_comm. unfold Qmult, Qeq, Qnum, Qden. rewrite Z.mul_1_r. reflexivity. discriminate. discriminate. setoid_replace (Z.of_nat (S i) # Pos.of_nat (S n))%Q with ((1#Pos.of_nat (S n)) + (Z.of_nat i # Pos.of_nat (S n)))%Q. rewrite CR_of_Q_plus. unfold CRminus. rewrite CRopp_plus_distr. rewrite <- CRplus_assoc, (CRplus_comm a). do 2 rewrite CRplus_assoc. rewrite <- (CRplus_assoc a). rewrite CRplus_opp_r, CRplus_0_l, CRopp_mult_distr_r. rewrite <- CRmult_plus_distr_l. apply CRmult_morph. reflexivity. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. reflexivity. rewrite Qinv_plus_distr. fold (1 + i)%nat. rewrite Nat2Z.inj_add. reflexivity. - apply (CR_cv_proper _ (a*(b-a) + 1 * ((b-a) * (b-a) * CR_of_Q R (1#2)))). apply (CR_cv_plus _ _ (a*(b-a))). apply CR_cv_const. apply CR_cv_scale. intros n. exists (Pos.to_nat n). intros. rewrite CRabs_minus_sym. setoid_replace (1 - CR_of_Q R (Z.of_nat i # Pos.of_nat (S i))) with (CR_of_Q R (1# Pos.of_nat (S i))). 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 le_S,H. discriminate. apply CR_of_Q_le; discriminate. unfold CRminus. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus. apply CR_of_Q_morph. unfold Qopp,Qplus,Qeq,Qnum,Qden. apply f_equal2. 2: reflexivity. rewrite Z.mul_1_l, Z.mul_1_r. rewrite <- positive_nat_Z, Nat2Pos.id. 2: discriminate. fold (1+i)%nat. rewrite Nat2Z.inj_add. ring. rewrite CRmult_1_l. rewrite (CRmult_comm a), CRmult_assoc, <- CRmult_plus_distr_l. setoid_replace (a + (b - a) * CR_of_Q R (1 # 2)) with ((a+b) * CR_of_Q R (1#2)). rewrite <- CRmult_assoc. apply CRmult_morph. 2: reflexivity. unfold CRminus. rewrite CRmult_plus_distr_r, CRmult_plus_distr_l. rewrite CRmult_plus_distr_l, (CRplus_comm (b*a)), CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRplus_comm. rewrite <- (CRopp_mult_distr_l a b), (CRmult_comm a b). rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite <- CRopp_mult_distr_l. reflexivity. apply (CRmult_eq_reg_r (CR_of_Q R 2)). left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_plus_distr_r. rewrite CRmult_assoc, CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1#2)*2)%Q with 1%Q. 2: reflexivity. rewrite (CR_of_Q_plus R 1 1), CRmult_1_r, CRmult_1_r. rewrite CRmult_plus_distr_l. rewrite CRmult_1_r. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. unfold CRminus. rewrite CRplus_comm, CRplus_assoc, CRplus_opp_l. apply CRplus_0_r. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont