proposition: Lemma UC_integral_constant : forall {R : ConstructiveReals} f a b c (cont_mod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f cont_mod) (leab : a <= b), (forall x, (a <= x /\ x <= b) -> f x == c) -> UC_integral f a b cont_mod fCont leab == (b-a) * c.
proof: Proof. intros. unfold UC_integral. destruct (CR_complete R (fun last : nat => IntegralFiniteSum f (fun n : nat => a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n : nat => a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last) (UC_integral_cauchy f a b cont_mod fCont leab)). apply (CR_cv_unique (fun last : nat => IntegralFiniteSum f (fun n : nat => (a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last)))) (fun n : nat => (a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last)))) last) ). exact c0. intros n. exists O. intros. unfold IntegralFiniteSum, CRminus. rewrite (CRsum_eq _ (fun k => c * (b-a) * CR_of_Q R (1# Pos.of_nat (S i)))). rewrite sum_const. setoid_replace (c * (b - a) * CR_of_Q R (1 # Pos.of_nat (S i)) * INR (S i) + - ((b + - a) * c)) with (CR_of_Q R 0). rewrite CRabs_right. apply CR_of_Q_le; discriminate. apply CRle_refl. unfold INR. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # Pos.of_nat (S i)) * (Z.of_nat (S i) # 1))%Q with 1%Q. rewrite CRmult_1_r, CRmult_comm. unfold CRminus. rewrite CRplus_opp_r. reflexivity. unfold Qmult, Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_l. rewrite Z.mul_1_r, Pos.mul_1_r. rewrite <- positive_nat_Z. rewrite Nat2Pos.id. reflexivity. discriminate. intros. rewrite H. rewrite CRmult_assoc. apply CRmult_morph. reflexivity. transitivity ((b + - a) * (CR_of_Q R (Z.of_nat (S i0) # Pos.of_nat (S i)) - CR_of_Q R (Z.of_nat i0 # Pos.of_nat (S i)))). unfold CRminus. do 3 rewrite CRmult_plus_distr_r. do 2 rewrite CRopp_plus_distr. do 2 rewrite CRmult_plus_distr_l. do 2 rewrite CRopp_mult_distr_l. do 4 rewrite <- CRplus_assoc. apply CRplus_morph. 2: rewrite CRopp_involutive, <- CRopp_mult_distr_l, <- CRopp_mult_distr_r, CRopp_involutive; reflexivity. rewrite (CRplus_comm a). do 4 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. do 2 rewrite <- CRplus_assoc. rewrite (CRplus_comm (b * - CR_of_Q R (Z.of_nat i0 # Pos.of_nat (S i)))). apply CRplus_morph. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_l. reflexivity. rewrite <- CRopp_mult_distr_l, <- CRopp_mult_distr_r. reflexivity. apply CRmult_morph. reflexivity. unfold CRminus. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_minus_distr. replace (Z.of_nat (S i0) - Z.of_nat i0)%Z with 1%Z. reflexivity. rewrite Nat2Z.inj_succ. ring. split. apply (CRle_trans _ (a + 0)). rewrite CRplus_0_r. apply CRle_refl. apply CRplus_le_compat_l. rewrite <- (CRmult_0_r (b-a)). 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. rewrite Z.mul_0_l, Z.mul_1_r. apply Nat2Z.is_nonneg. apply (CRplus_le_reg_l (-a)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite <- (CRmult_1_r (-a+b)), (CRplus_comm (-a)). 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. rewrite Z.mul_1_r, Z.mul_1_l. rewrite <- positive_nat_Z. rewrite Nat2Pos.id. apply Nat2Z.inj_le, le_S, H1. discriminate. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont