proposition: Lemma UC_integral_bound_proper : forall {R : ConstructiveReals} f (a b c d : CRcarrier R) (modF : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f modF) (leab : a <= b) (lecd : c <= d), a == c -> b == d -> UC_integral f a b modF fCont leab == UC_integral f c d modF fCont lecd.
proof: Proof. intros. unfold UC_integral. destruct (CR_complete R (fun last : nat => IntegralFiniteSum f (fun n : nat => c + (d - c) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n : nat => c + (d - c) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last) (UC_integral_cauchy f c d modF fCont lecd) ). apply (CR_cv_unique (fun last : nat => IntegralFiniteSum f (fun n : nat => c + (d - c) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n : nat => c + (d - c) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last)). 2: exact c0. 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)). 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 c1. intro n. apply CRsum_eq. intros. clear c1 x0 c0 x. apply CRmult_morph. apply (UniformContProper f modF fCont). rewrite H, H0. reflexivity. rewrite H, H0. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont