proposition: Lemma UC_right_bound_continuous : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (a b : CRcarrier R) (leab : a <= b) (eps : CRcarrier R) (epsPos : 0 < eps) (cont_mod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f cont_mod), { eta : CRcarrier R & prod (0 < eta) (forall (c:CRcarrier R) (leac : prod (b <= c) (c < b+eta)), CRabs R (UC_integral f a b cont_mod fCont leab - UC_integral f a c cont_mod fCont (CRle_trans a b c leab (fst leac))) <= eps) }.
proof: Proof. intros. destruct (UC_bounded f a b cont_mod fCont leab) as [B Bmaj]. 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 < B) as Bpos. { apply (CRle_lt_trans _ (CRabs R (f a))). apply CRabs_pos. apply Bmaj. apply CRle_refl. exact leab. } assert (0 < eps * CR_of_Q R (1#2) * CRinv R (b-a+1) (inr H)). { destruct fCont. apply CRmult_lt_0_compat. apply CRmult_lt_0_compat. exact epsPos. apply CR_of_Q_pos. reflexivity. apply CRinv_0_lt_compat, H. } exists (CRmin (cont_mod (eps * CR_of_Q R (1#2) * CRinv R (b-a+1) (inr H)) H0) (CRmin (eps * CR_of_Q R (1#2) * CRinv R B (inr Bpos)) 1)). split. apply CRmin_lt. apply (fst fCont). apply CRmin_lt. apply CRmult_lt_0_compat. apply CRmult_lt_0_compat. exact epsPos. apply CR_of_Q_pos. reflexivity. apply CRinv_0_lt_compat, Bpos. exact (CRzero_lt_one R). intros. apply (CR_cv_bound_up (fun last : nat => CRabs R (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 - IntegralFiniteSum f (fun n => a + (c-a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n => a + (c-a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last)) eps _ O). - intros n _. unfold IntegralFiniteSum. unfold CRminus. rewrite <- sum_opp, <- sum_plus. rewrite (CRsum_eq _ (fun n0 => ((f (a + (b + - a) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S n))) * (b + - a) - f (a + (c + - a) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S n))) * (c + - a)) * CR_of_Q R (1 # Pos.of_nat (S n))))). rewrite sum_scale, CRmult_comm. rewrite CRabs_mult, CRabs_right. 2: apply CR_of_Q_le; discriminate. apply (CRle_trans _ (CR_of_Q R (1 # Pos.of_nat (S n)) * CRsum (fun k => CRabs R (f (a + (b + - a) * CR_of_Q R (Z.of_nat k # Pos.of_nat (S n))) * (b-a) - f (a + (c + - a) * CR_of_Q R (Z.of_nat k # Pos.of_nat (S n))) * (c-a))) n)). apply CRmult_le_compat_l. apply CR_of_Q_le; discriminate. apply multiTriangleIneg. apply (CRle_trans _ (CR_of_Q R (1 # Pos.of_nat (S n)) * CRsum (fun _ => eps) n)). + apply CRmult_le_compat_l. apply CR_of_Q_le; discriminate. apply sum_Rle. intros. assert (CR_of_Q R (Z.of_nat k # Pos.of_nat (S n)) <= 1) as inInterval. { apply CR_of_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_l. destruct k. discriminate. unfold Z.of_nat. apply Pos2Z.pos_le_pos. rewrite Pos.of_nat_succ. apply Pos2Nat.inj_le. rewrite Nat2Pos.id, Nat2Pos.id. apply le_S, H1. discriminate. discriminate. } setoid_replace (f (a + (b + - a) * CR_of_Q R (Z.of_nat k # Pos.of_nat (S n))) * (b - a) - f (a + (c + - a) * CR_of_Q R (Z.of_nat k # Pos.of_nat (S n))) * (c - a)) with (f (a + (b + - a) * CR_of_Q R (Z.of_nat k # Pos.of_nat (S n))) * (b - a) - f (a + (b + - a) * CR_of_Q R (Z.of_nat k # Pos.of_nat (S n))) * (c - a) + (f (a + (b + - a) * CR_of_Q R (Z.of_nat k # Pos.of_nat (S n))) * (c - a) - f (a + (c + - a) * CR_of_Q R (Z.of_nat k # Pos.of_nat (S n))) * (c - a))). apply (CRle_trans _ _ _ (CRabs_triang _ _)). apply (CRle_trans _ (eps * CR_of_Q R (1#2) + eps * CR_of_Q R (1#2))). apply CRplus_le_compat. unfold CRminus. rewrite CRopp_mult_distr_r, <- CRmult_plus_distr_l, CRabs_mult. setoid_replace (b + - a + - (c + - a)) with (b-c). apply (CRle_trans _ (B * CRabs R (b-c))). apply CRmult_le_compat_r. apply CRabs_pos. apply CRlt_asym, Bmaj. apply (CRle_trans _ (a + 0)). rewrite CRplus_0_r. apply CRle_refl. apply CRplus_le_compat_l. apply CRmult_le_0_compat. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat_r. exact leab. apply CR_of_Q_le. unfold Qle; simpl. rewrite Z.mul_1_r. apply Nat2Z.is_nonneg. apply (CRplus_le_reg_l (-a)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite <- (CRmult_1_r (-a+b)), (CRplus_comm (-a)). apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat_r. exact leab. exact inInterval. rewrite CRabs_minus_sym, CRabs_right. apply (CRmult_le_reg_r (CRinv R B (inr Bpos))). apply CRinv_0_lt_compat, Bpos. rewrite CRmult_comm, <- CRmult_assoc, CRinv_l, CRmult_1_l. destruct leac. apply (CRplus_lt_compat_l R (-b)) in c1. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l, CRplus_comm in c1. apply CRlt_asym, (CRlt_le_trans _ _ _ c1). apply (CRle_trans _ _ _ (CRmin_r _ _)). apply CRmin_l. rewrite <- (CRplus_opp_r b). apply CRplus_le_compat_r. exact (fst leac). do 2 rewrite <- (CRplus_comm (-a)). exact (addSub (-a) b c). unfold CRminus. rewrite CRopp_mult_distr_l, <- CRmult_plus_distr_r. rewrite CRabs_mult. apply (CRle_trans _ (eps * CR_of_Q R (1 # 2) * CRinv R (b - a + 1) (inr H) * CRabs R (c + - a))). apply CRmult_le_compat_r. apply CRabs_pos. apply CRlt_asym. apply (snd fCont _ _ _ H0). rewrite addSub. apply (CRle_lt_trans _ (c-b)). unfold CRminus. rewrite CRopp_mult_distr_l, <- CRmult_plus_distr_r, CRabs_mult. rewrite <- (CRplus_comm (-a)), <- (CRplus_comm (-a)), (addSub (-a) b c). rewrite <- (CRmult_1_r (c+-b)), CRabs_minus_sym, CRabs_right. apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r b). apply CRplus_le_compat_r. exact (fst leac). rewrite CRabs_right. exact inInterval. apply CR_of_Q_le. unfold Qle; simpl. rewrite Z.mul_1_r. apply Nat2Z.is_nonneg. rewrite <- (CRplus_opp_r b). apply CRplus_le_compat_r. exact (fst leac). destruct leac. apply (CRplus_lt_compat_l R (-b)) in c1. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l, CRplus_comm in c1. apply (CRlt_le_trans _ _ _ c1). apply CRmin_l. rewrite <- (CRmult_1_r (eps * CR_of_Q R (1 # 2))). do 2 rewrite CRmult_assoc. apply CRmult_le_compat_l. apply CRmult_le_0_compat. apply CRlt_asym, epsPos. apply CRlt_asym, CR_of_Q_pos. reflexivity. rewrite CRmult_1_l. apply (CRmult_le_reg_l (b-a+1) _ _ H). rewrite <- CRmult_assoc, CRinv_r, CRmult_1_l, CRmult_1_r. rewrite CRabs_right. unfold CRminus. rewrite (CRplus_comm c), (CRplus_comm b). rewrite CRplus_assoc. apply CRplus_le_compat_l. apply CRlt_asym. destruct leac. apply (CRlt_le_trans _ _ _ c1). apply CRplus_le_compat_l. apply (CRle_trans _ _ _ (CRmin_r _ _)), CRmin_r. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat_r. apply (CRle_trans _ _ _ leab). exact (fst leac). rewrite <- CRmult_plus_distr_l, <- CR_of_Q_plus. rewrite Qinv_plus_distr. setoid_replace (1 + 1 # 2)%Q with 1%Q. rewrite CRmult_1_r. apply CRle_refl. reflexivity. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. + rewrite sum_const. rewrite CRmult_comm, CRmult_assoc. unfold INR. rewrite <- CR_of_Q_mult. setoid_replace ((Z.of_nat (S n) # 1) * (1 # Pos.of_nat (S n)))%Q with 1%Q. rewrite CRmult_1_r. apply CRle_refl. unfold Z.of_nat. rewrite Pos.of_nat_succ. unfold Qeq. simpl. do 2 rewrite Pos.mul_1_r. reflexivity. + intros. unfold CRminus. unfold CRminus in addSub. do 2 rewrite (addSub a). rewrite CRopp_mult_distr_r, <- CRmult_plus_distr_l. rewrite (CRopp_mult_distr_r (c+-a)), <- CRmult_plus_distr_l. setoid_replace (CR_of_Q R (Z.of_nat (S i) # Pos.of_nat (S n)) + - CR_of_Q R (Z.of_nat i # Pos.of_nat (S n))) with (CR_of_Q R (1 # Pos.of_nat (S n))). rewrite <- CRmult_assoc, <- CRmult_assoc, CRopp_mult_distr_l. rewrite <- CRmult_plus_distr_r. reflexivity. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_minus_distr. replace (Z.of_nat (S i) - Z.of_nat i)%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 => 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 c0. unfold UC_integral. destruct (CR_complete R (fun last : nat => IntegralFiniteSum f (fun n0 : nat => a + (c - a) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S last))) (fun n0 : nat => a + (c - a) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S last))) last) (UC_integral_cauchy f a c cont_mod fCont (CRle_trans a b c leab (fst leac)))). exact c0. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont