proposition: Lemma UC_integral_chasles_rat_rat : forall {R : ConstructiveReals} (a b : Q) (c : CRcarrier R) (f : CRcarrier R -> CRcarrier R) (cont_mod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f cont_mod) (leab : (CR_of_Q R a) <= (CR_of_Q R b)) (lebc : (CR_of_Q R b) <= c) (leac : (CR_of_Q R a) <= c), UC_integral f (CR_of_Q R a) c cont_mod fCont leac == UC_integral f (CR_of_Q R a) (CR_of_Q R b) cont_mod fCont leab + UC_integral f (CR_of_Q R b) c cont_mod fCont lebc.
proof: Proof. intros. assert (forall n : nat, c < c + CR_of_Q R (1 # Pos.of_nat (S n))). { intro n. apply (CRle_lt_trans _ (c+0)). rewrite CRplus_0_r. apply CRle_refl. apply CRplus_lt_compat_l, CR_of_Q_pos. reflexivity. } pose (fun n => let (q,_) := CR_Q_dense R c (c + CR_of_Q R (1 # Pos.of_nat (S n))) (H n) in q) as cn. assert (forall n:nat, c <= CR_of_Q R (cn n)) as H0. { intro n. unfold cn. destruct (CR_Q_dense R c (c + CR_of_Q R (1 # Pos.of_nat (S n))) (H n)). apply CRlt_asym, p. } assert (CR_cv R (fun n : nat => CR_of_Q R (cn n)) c) as cvRight. { intro p. exists (Pos.to_nat p). intros. unfold cn. destruct (CR_Q_dense R c (c + CR_of_Q R (1 # Pos.of_nat (S i))) (H i)). rewrite CRabs_right. apply (CRplus_le_reg_r c). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_comm. apply CRlt_asym, (CRlt_le_trans _ _ _ (snd p0)). apply CRplus_le_compat_l. apply CR_of_Q_le. apply Pos2Z.pos_le_pos. unfold Qden. do 2 rewrite Pos.mul_1_l. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply le_S, H1. discriminate. rewrite <- (CRplus_opp_r c). apply CRplus_le_compat_r. apply CRlt_asym, p0. } apply (CR_cv_unique (fun n => UC_integral f (CR_of_Q R a) (CR_of_Q R (cn n)) cont_mod fCont (CRle_trans _ _ _ leac (H0 n)))). - apply (UC_right_bound_cv (CR_of_Q R a) c (fun n => CR_of_Q R (cn n)) f cont_mod fCont leac). exact cvRight. - apply (CR_cv_eq _ (fun n : nat => UC_integral f (CR_of_Q R a) (CR_of_Q R b) cont_mod fCont leab + UC_integral f (CR_of_Q R b) (CR_of_Q R (cn n)) cont_mod fCont (CRle_trans _ _ _ lebc (H0 n)))). intro n. symmetry. apply (UC_integral_chasles_rat a b (cn n) f). apply CR_cv_plus. apply CR_cv_const. exact (UC_right_bound_cv (CR_of_Q R b) c (fun n => CR_of_Q R (cn n)) f _ _ _ _ cvRight). Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont