proposition: Lemma CSUC_func_mult_stable : forall {R : ConstructiveReals} (f g : CRcarrier R -> CRcarrier R) (a b : CRcarrier R) (modF modG : forall x:CRcarrier R, 0 < x -> CRcarrier R), CSUC f a b modF -> a <= b -> UniformCont g modG -> { modFG : forall x:CRcarrier R, 0 < x -> CRcarrier R & CSUC (fun x => f x * g x) a b modFG }.
proof: Proof. intros. destruct (CSUC_bounded f a b modF H H0) as [Bf majf]. destruct H. assert (0 < Bf) as Bfpos. { specialize (majf a). apply (CRle_lt_trans _ (CRabs _ (f a))). apply CRabs_pos. apply majf. } destruct (UC_bounded g (a-1) (b+1) modG H1 (Rminus_plus_one_lower a b H0)) as [Bg majg]. assert (0 < Bg) as Bgpos. { specialize (majg a). apply (CRle_lt_trans _ (CRabs _ (g a))). apply CRabs_pos. apply majg. apply CRlt_asym, Rminus_pos_lower. apply CRzero_lt_one. apply (CRle_trans _ b _ H0). apply CRlt_asym, Rplus_pos_higher. apply CRzero_lt_one. } assert (forall eps:CRcarrier R, 0 < eps -> 0 < eps * CR_of_Q R (1#2) * (CRinv R Bg (inr Bgpos))). { intros. apply CRmult_lt_0_compat. apply CRmult_lt_0_compat. exact H. apply CR_of_Q_pos; reflexivity. apply CRinv_0_lt_compat, Bgpos. } assert (forall eps:CRcarrier R, 0 < eps -> 0 < eps * CR_of_Q R (1#2) * (CRinv R Bf (inr Bfpos))). { intros. apply CRmult_lt_0_compat. apply CRmult_lt_0_compat. exact H2. apply CR_of_Q_pos; reflexivity. apply CRinv_0_lt_compat, Bfpos. } exists (fun eps epsPos => CRmin (modF (eps * CR_of_Q R (1#2) * CRinv R Bg (inr Bgpos)) (H eps epsPos)) (modG (eps * CR_of_Q R (1#2) * CRinv R Bf (inr Bfpos)) (H2 eps epsPos))). split. split. - intros. apply CRmin_lt. apply (fst u). apply (fst H1). - intros. destruct (CRltLinear R). destruct (s (a-1) x a (Rminus_pos_lower a 1 (CRzero_lt_one R))). + destruct (s b x (b+1) (Rplus_pos_higher b 1 (CRzero_lt_one R))). destruct (s (a-1) y a (Rminus_pos_lower a 1 (CRzero_lt_one R))). destruct (s b y (b+1) (Rplus_pos_higher b 1 (CRzero_lt_one R))). rewrite c,c. do 2 rewrite CRmult_0_l. unfold CRminus. rewrite CRplus_0_l. rewrite CRopp_0. rewrite CRabs_right. apply epsPos. apply CRle_refl. right. exact c3. right. exact c1. specialize (c x (inr c1)). setoid_replace (f x * g x - f y * g y) with ((f x - f y) * g y). 2: rewrite c. rewrite CRabs_mult. rewrite CRmult_comm. apply (CRle_lt_trans _ (Bg * CRabs _ (f x - f y))). apply CRmult_le_compat_r. apply CRabs_pos. apply CRlt_asym, majg. apply CRlt_asym, c2. apply CRlt_asym, c3. apply (CRlt_le_trans _ (Bg * (eps * CR_of_Q R (1#2) * CRinv R Bg (inr Bgpos)))). apply CRmult_lt_compat_l. apply Bgpos. destruct u. apply (c5 _ _ _ (H _ epsPos)). apply (CRlt_le_trans _ _ _ H3). apply CRmin_l. rewrite CRmult_comm, CRmult_assoc, CRinv_l, CRmult_1_r. rewrite <- (CRmult_1_r eps), CRmult_assoc. apply CRmult_le_compat_l. apply CRlt_asym, epsPos. rewrite CRmult_1_l. apply CR_of_Q_le; discriminate. unfold CRminus. rewrite CRmult_0_l, CRplus_0_l, CRplus_0_l. apply CRopp_mult_distr_l. rewrite c, c. do 2 rewrite CRmult_0_l. unfold CRminus. rewrite CRplus_0_l. rewrite CRopp_0. rewrite CRabs_right. apply epsPos. apply CRle_refl. left. exact c2. right. exact c1. setoid_replace (f x * g x - f y * g y) with (g x * (f x - f y) + f y *(g x - g y)). apply (CRle_lt_trans _ _ _ (CRabs_triang _ _)). setoid_replace eps with (eps*CR_of_Q R (1#2) + eps*CR_of_Q R (1#2)). apply CRplus_le_lt_compat. apply CRlt_asym. * rewrite CRabs_mult. apply (CRle_lt_trans _ (Bg * CRabs _ (f x - f y))). apply CRmult_le_compat_r. apply CRabs_pos. apply CRlt_asym, majg. apply CRlt_asym, c0. apply CRlt_asym, c1. apply (CRlt_le_trans _ (Bg * (eps * CR_of_Q R (1#2) * CRinv R Bg (inr Bgpos)))). apply CRmult_lt_compat_l. apply Bgpos. destruct u. apply (c3 _ _ _ (H _ epsPos)). apply (CRlt_le_trans _ _ _ H3). apply CRmin_l. rewrite CRmult_comm, CRmult_assoc, CRinv_l. rewrite CRmult_1_r. apply CRle_refl. * rewrite CRabs_mult. apply (CRle_lt_trans _ (Bf * CRabs _ (g x - g y))). apply CRmult_le_compat_r. apply CRabs_pos. apply CRlt_asym, majf. apply (CRlt_le_trans _ (Bf * (eps *CR_of_Q R (1#2) * CRinv R Bf (inr Bfpos)))). apply CRmult_lt_compat_l. apply Bfpos. destruct H1. apply (c3 _ _ _ (H2 _ epsPos)). apply (CRlt_le_trans _ _ _ H3). apply CRmin_r. rewrite CRmult_comm, CRmult_assoc, CRinv_l. rewrite CRmult_1_r. apply CRle_refl. * rewrite <- CRmult_plus_distr_l, <- CR_of_Q_plus. setoid_replace ((1#2) + (1#2))%Q with 1%Q. rewrite CRmult_1_r. reflexivity. reflexivity. * unfold CRminus. do 2 rewrite CRmult_plus_distr_l. rewrite CRplus_assoc. apply CRplus_morph. apply CRmult_comm. rewrite <- CRplus_assoc, (CRmult_comm (g x)). rewrite <- CRmult_plus_distr_r, CRplus_opp_l, CRmult_0_l. rewrite CRplus_0_l, CRopp_mult_distr_r. reflexivity. + destruct (s (a-1) y a (Rminus_pos_lower a 1 (CRzero_lt_one R))). destruct (s b y (b+1) (Rplus_pos_higher b 1 (CRzero_lt_one R))). * rewrite c,c. do 2 rewrite CRmult_0_l. unfold CRminus. rewrite CRplus_0_l. rewrite CRopp_0. rewrite CRabs_right. apply epsPos. apply CRle_refl. right. exact c2. left. exact c0. * specialize (c x (inl c0)). setoid_replace (f x * g x - f y * g y) with ((f x - f y) * g y). 2: rewrite c. rewrite CRabs_mult. rewrite CRmult_comm. apply (CRle_lt_trans _ (Bg * CRabs _ (f x - f y))). apply CRmult_le_compat_r. apply CRabs_pos. apply CRlt_asym, majg. apply CRlt_asym, c1. apply CRlt_asym, c2. apply (CRlt_le_trans _ (Bg * (eps * CR_of_Q R (1#2) * CRinv R Bg (inr Bgpos)))). apply CRmult_lt_compat_l. apply Bgpos. destruct u. apply (c4 _ _ _ (H _ epsPos)). apply (CRlt_le_trans _ _ _ H3). apply CRmin_l. rewrite CRmult_comm, CRmult_assoc, CRinv_l. rewrite CRmult_1_r. rewrite <- (CRmult_1_r eps), CRmult_assoc. apply CRmult_le_compat_l. apply CRlt_asym, epsPos. rewrite CRmult_1_l. apply CR_of_Q_le; discriminate. rewrite CRmult_0_l. unfold CRminus. do 2 rewrite CRplus_0_l. rewrite CRopp_mult_distr_l. reflexivity. * rewrite c,c. do 2 rewrite CRmult_0_l. unfold CRminus. rewrite CRplus_0_l. rewrite CRopp_0. rewrite CRabs_right. apply epsPos. apply CRle_refl. left. exact c1. left. exact c0. - intros. destruct H3. rewrite c, CRmult_0_l. reflexivity. left. exact c0. rewrite c, CRmult_0_l. reflexivity. right. exact c0. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal