proposition: Lemma UC_integral_scale : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (a b l : CRcarrier R) (modF : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f modF) (leab : a <= b), UC_integral (fun x => l * (f x)) a b _ (UC_scale f modF l fCont) leab == l * (UC_integral f a b modF fCont leab).
proof: Proof. intros. unfold UC_integral. 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 Rcauchy_complete_eq. 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) * l)). 2: rewrite CRmult_comm; apply CR_cv_scale, c. intro n. unfold IntegralFiniteSum. rewrite <- sum_scale. apply CRsum_eq. intros. rewrite (CRmult_comm l). do 2 rewrite CRmult_assoc. apply CRmult_morph. reflexivity. apply CRmult_comm. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont