proposition: Lemma UC_integral_chasles : forall {R : ConstructiveReals} (a 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 : a <= b) (lebc : b <= c) (leac : a <= c), UC_integral f a c cont_mod fCont leac == UC_integral f a b cont_mod fCont leab + UC_integral f b c cont_mod fCont lebc.
proof: Proof. intros. assert (a-a <= c-a). { apply CRplus_le_compat_r, leac. } assert (CR_of_Q R 0 <= c-a). { rewrite <- (CRplus_opp_r a). exact H. } rewrite (UC_integral_translate f a c (-a) _ H). rewrite (UC_integral_bound_proper _ (a+-a) (c+-a) (CR_of_Q R 0) (c+-a) cont_mod _ _ H0). assert (CR_of_Q R 0 <= b-a). { rewrite <- (CRplus_opp_r a). apply CRplus_le_compat_r. exact leab. } assert (b-a <= c-a). { apply CRplus_le_compat_r. exact lebc. } rewrite (UC_integral_chasles_rat_rat_rat 0 (b-a) (c+-a) _ _ _ H1 H2). apply CRplus_morph. - assert (a-a <= b-a). { apply CRplus_le_compat_r. exact leab. } rewrite (UC_integral_translate f a b (-a) _ H3). apply UC_integral_bound_proper. rewrite CRplus_opp_r. reflexivity. reflexivity. - rewrite (UC_integral_translate f b c (-a) _ H2). apply UC_integral_bound_proper. reflexivity. reflexivity. - rewrite CRplus_opp_r. reflexivity. - reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont