proposition: Lemma UC_integral_nonneg : forall {R : ConstructiveReals} f g a b (modF : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (modG : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f modF) (gCont : UniformCont g modG) (leab leabb : a <= b), (forall x, (a <= x /\ x <= b) -> (f x) <= (g x)) -> UC_integral f a b modF fCont leab <= (UC_integral g a b modG gCont leabb).
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 modF fCont leab)). destruct (CR_complete R (fun last : nat => IntegralFiniteSum g (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 g a b modG gCont leabb)). assert (forall n:nat, ((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) n) <= ((fun last : nat => IntegralFiniteSum g (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) n)). { intros. unfold IntegralFiniteSum, CRminus. apply sum_Rle. intros. apply CRmult_le_compat_r. apply (CRle_minus (a + (b + - a) * CR_of_Q R (Z.of_nat k # Pos.of_nat (S n))) ( a + (b + - a) * CR_of_Q R (Z.of_nat (S k) # Pos.of_nat (S n)))). apply CRplus_le_compat_l. apply CRmult_le_compat_l. apply (CRle_minus a b), leab. apply CR_of_Q_le. unfold Qle, Qnum, Qden. apply Z.mul_le_mono_nonneg_r. discriminate. apply Nat2Z.inj_le, le_S, Nat.le_refl. apply H. 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. apply (CRle_minus a b), leab. 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, H0. discriminate. } apply (CR_cv_le _ _ _ _ H0); assumption. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont