proposition: Lemma UC_integral_slide_cv : forall {R : ConstructiveReals} (a b : 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) (an : nat -> CRcarrier R) (lebbn : forall n:nat, an n <= b + (an n - a)), CR_cv R an a -> CR_cv R (fun n : nat => UC_integral f (an n) (b + (an n - a)) cont_mod fCont (lebbn n)) (UC_integral f a b cont_mod fCont leab).
proof: Proof. intros. intro p. 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. } assert (0 < b-a+1). { rewrite <- (CRplus_opp_l a). unfold CRminus. rewrite (CRplus_comm b), CRplus_assoc. apply CRplus_lt_compat_l. apply (CRle_lt_trans _ (b+0)). rewrite CRplus_0_r. exact leab. apply CRplus_lt_compat_l, CRzero_lt_one. } assert (0 < CR_of_Q R (1#p) * CRinv R (b-a+1) (inr H0)) as H1. { destruct fCont. apply CRmult_lt_0_compat. apply CR_of_Q_pos. reflexivity. apply CRinv_0_lt_compat, H0. } pose proof (Un_cv_nat_real _ _ H _ (fst fCont _ H1)) as [n nmaj]. exists n. intros. apply (CR_cv_bound_up (fun last : nat => CRabs R (IntegralFiniteSum f (fun n => an i + (b-a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n => an i + (b-a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last - IntegralFiniteSum f (fun n => a + (b-a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n => a + (b-a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last)) (CR_of_Q R (1#p)) _ O). - intros n0 _. unfold IntegralFiniteSum. unfold CRminus. rewrite <- sum_opp, <- sum_plus. rewrite (CRsum_eq _ (fun n1 => (f (an i + (b + - a) * CR_of_Q R (Z.of_nat n1 # Pos.of_nat (S n0))) - f (a + (b + - a) * CR_of_Q R (Z.of_nat n1 # Pos.of_nat (S n0)))) * (b + - a) * CR_of_Q R (1 # Pos.of_nat (S n0)))). + rewrite sum_scale, sum_scale. specialize (nmaj i H2). rewrite CRmult_assoc, CRabs_mult. apply (CRle_trans _ ((CRsum (fun _ : nat => CR_of_Q R (1 # p) * CRinv R (b - a + 1) (inr H0)) n0) * CRabs R (CR_of_Q R (1 # Pos.of_nat (S n0)) * (b + - a)))). rewrite <- (CRmult_comm (b+-a)). apply CRmult_le_compat_r. apply CRabs_pos. apply (CRle_trans _ _ _ (multiTriangleIneg _ _)). apply sum_Rle. intros. apply CRlt_asym, (snd fCont _ _ _ H1). rewrite (CRplus_comm (an i)), (CRplus_comm a), addSub. exact nmaj. rewrite sum_const, CRabs_right, CRmult_assoc, <- (CRmult_1_r (CR_of_Q R (1 # p))). do 2 rewrite CRmult_assoc. apply CRmult_le_compat_l. apply CRlt_asym, CR_of_Q_pos. reflexivity. rewrite CRmult_1_l. unfold INR. rewrite CRmult_comm, <- CRmult_assoc. rewrite <- CR_of_Q_mult. setoid_replace ((Z.of_nat (S n0) # 1) * (1 # Pos.of_nat (S n0)))%Q with 1%Q. rewrite CRmult_1_l. apply (CRmult_le_reg_r (b-a+1) _ _ H0). rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_1_l. apply (CRle_trans _ (b-a + 0)). rewrite CRplus_0_r. apply CRle_refl. apply CRplus_le_compat_l. apply CRlt_asym, CRzero_lt_one. unfold Z.of_nat. rewrite Pos.of_nat_succ. unfold Qeq. simpl. do 2 rewrite Pos.mul_1_r. reflexivity. apply CRmult_le_0_compat. apply CR_of_Q_le. discriminate. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat_r. exact leab. + intros. rewrite (addSub (an i) ((b + - a) * CR_of_Q R (Z.of_nat (S i0) # Pos.of_nat (S n0))) ((b + - a) * CR_of_Q R (Z.of_nat i0 # Pos.of_nat (S n0)))). rewrite (addSub a ((b + - a) * CR_of_Q R (Z.of_nat (S i0) # Pos.of_nat (S n0))) ((b + - a) * CR_of_Q R (Z.of_nat i0 # Pos.of_nat (S n0)))). rewrite CRopp_mult_distr_l, <- CRmult_plus_distr_r. unfold CRminus. rewrite CRopp_mult_distr_r, <- CRmult_plus_distr_l. rewrite CRmult_assoc. apply CRmult_morph. reflexivity. apply CRmult_morph. reflexivity. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_minus_distr. replace (Z.of_nat (S i0) - Z.of_nat i0)%Z with 1%Z. reflexivity. rewrite Nat2Z.inj_succ. unfold Z.succ. ring. - apply CR_cv_abs_cont. apply CR_cv_minus. unfold UC_integral. destruct (CR_complete R (fun last : nat => IntegralFiniteSum f (fun n0 : nat => an i + (b + (an i - a) - an i) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S last))) (fun n0 : nat => an i + (b + (an i - a) - an i) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S last))) last) (UC_integral_cauchy f (an i) (b + (an i - a)) cont_mod fCont (lebbn i))). apply (CR_cv_eq _ (fun last : nat => IntegralFiniteSum f (fun n0 : nat => an i + (b + (an i - a) - an i) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S last))) (fun n0 : nat => an i + (b + (an i - a) - an i) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S last))) last)). 2: exact c. intros. apply CRsum_eq. intros. rewrite (UniformContProper f cont_mod fCont _ (an i + (b - a) * CR_of_Q R (Z.of_nat i0 # Pos.of_nat (S n0)))). setoid_replace (b + (an i - a) - an i) with (b-a). reflexivity. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l. apply CRplus_0_l. apply CRplus_morph. reflexivity. apply CRmult_morph. 2: reflexivity. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l. apply CRplus_0_l. unfold UC_integral. destruct (CR_complete R (fun last : nat => IntegralFiniteSum f (fun n0 : nat => a + (b - a) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S last))) (fun n0 : nat => a + (b - a) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S last))) last) (UC_integral_cauchy f a b cont_mod fCont leab)). exact c. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont