proposition: Lemma UC_integral_translate : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (a b t : CRcarrier R) (leab : a <= b) (leabt : a+t <= b+t) (cont_mod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f cont_mod), UC_integral f a b cont_mod fCont leab == UC_integral (fun x => f (x-t)) (a+t) (b+t) cont_mod (UC_translate_horizontal f (-t) cont_mod fCont) leabt.
proof: Proof. intros. unfold UC_integral. assert (forall i j k : CRcarrier R, i + j - (i + k) == j - k) as addSub. { intros. unfold CRminus. rewrite CRopp_plus_distr. rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. } destruct (CR_complete R (fun last : nat => IntegralFiniteSum (fun x : CRcarrier R => f (x - t)) (fun n : nat => a + t + (b + t - (a + t)) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n : nat => a + t + (b + t - (a + t)) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last) (UC_integral_cauchy (fun x : CRcarrier R => f (x - t)) (a + t) (b + t) cont_mod (UC_translate_horizontal f (- t) cont_mod fCont) leabt)). apply (CR_cv_unique (fun last : nat => IntegralFiniteSum (fun x : CRcarrier R => f (x - t)) (fun n : nat => a + t + (b + t - (a + t)) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n : nat => a + t + (b + t - (a + t)) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last)). 2: exact c. 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_eq _ (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)). 2: exact c0. intro n. apply CRsum_eq. intros. apply CRmult_morph. - apply (UniformContProper f cont_mod fCont). setoid_replace (b + t - (a + t)) with (b-a). unfold CRminus. do 2 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite (CRplus_comm t), CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity. rewrite (CRplus_comm b), (CRplus_comm a). rewrite addSub. reflexivity. - setoid_replace (b + t - (a + t)) with (b-a). rewrite addSub, addSub. reflexivity. rewrite (CRplus_comm b), (CRplus_comm a). rewrite addSub. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont