proposition: Lemma UC_integral_chasles_rat_rat_rat : forall {R : ConstructiveReals} (a : Q) (b 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) <= b) (lebc : 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) b cont_mod fCont leab + UC_integral f b c cont_mod fCont lebc.
proof: Proof. intros. assert (forall n : nat, b < b + CR_of_Q R (1 # Pos.of_nat (S n))). { intro n. apply (CRle_lt_trans _ (b+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 b (b + CR_of_Q R (1 # Pos.of_nat (S n))) (H n) in q) as bn. assert (CR_cv R (fun n : nat => CR_of_Q R (bn n)) b) as cvb. { intro p. exists (Pos.to_nat p). intros. unfold bn. destruct (CR_Q_dense R b (b + CR_of_Q R (1 # Pos.of_nat (S i))) (H i)). rewrite CRabs_right. apply (CRplus_le_reg_r b). 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, H0. discriminate. rewrite <- (CRplus_opp_r b). apply CRplus_le_compat_r. apply CRlt_asym, p0. } assert (forall n:nat, b <= CR_of_Q R (bn n)) as H0. { intro n. unfold bn. destruct (CR_Q_dense R b (b + CR_of_Q R (1 # Pos.of_nat (S n))) (H n)). apply CRlt_asym, p. } pose (fun n => c + (CR_of_Q R (bn n) - b)) as cn. assert (forall n:nat, CR_of_Q R (bn n) <= cn n). { intro n. unfold cn. rewrite CRplus_comm. apply (CRplus_le_reg_r (-c)). rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. apply CRplus_le_compat_l, CRopp_ge_le_contravar. exact lebc. } apply (CR_cv_unique (fun n => UC_integral f (CR_of_Q R a) (CR_of_Q R (bn n)) cont_mod fCont (CRle_trans _ _ _ leab (H0 n)) + UC_integral f (CR_of_Q R (bn n)) (cn n) cont_mod fCont (H1 n))). - assert (forall n:nat, c <= cn n) as H2. { intro n. unfold cn. apply (CRle_trans _ (c+0)). rewrite CRplus_0_r. apply CRle_refl. apply CRplus_le_compat_l. rewrite <- (CRplus_opp_r b). apply CRplus_le_compat_r. apply H0. } apply (CR_cv_eq _ (fun n : nat => UC_integral f (CR_of_Q R a) (cn n) cont_mod fCont (CRle_trans _ _ _ leac (H2 n)))). intro n. apply UC_integral_chasles_rat_rat. apply UC_right_bound_cv. unfold cn. apply (CR_cv_proper _ (b+(c-b))). apply (CR_cv_eq _ (fun n : nat => CR_of_Q R (bn n) + (c - b))). intro n. rewrite (CRplus_comm c). unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. apply CRplus_comm. apply CR_cv_plus. exact cvb. apply CR_cv_const. unfold CRminus. rewrite CRplus_comm, CRplus_assoc, CRplus_opp_l. apply CRplus_0_r. - apply CR_cv_plus. + apply UC_right_bound_cv. exact cvb. + unfold cn. apply (UC_integral_slide_cv b c f cont_mod fCont lebc (fun n => CR_of_Q R (bn n))). exact cvb. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont