proposition: Lemma UC_scale : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (modF : forall x:CRcarrier R, 0 < x -> CRcarrier R) (a : CRcarrier R), UniformCont f modF -> UniformCont (fun x:CRcarrier R => a * f x) (fun (eps:CRcarrier R) epsPos => modF (eps * (CRinv R (CRmax 1 (CRabs _ a)) (inr (posScale a)))) (CRmult_lt_0_compat _ eps _ epsPos (CRinv_0_lt_compat _ _ (inr (posScale a)) (posScale a)))).
proof: Proof. split. - intros x xPos. destruct H. apply c. - intros. unfold CRminus. rewrite CRopp_mult_distr_r, <- CRmult_plus_distr_l. rewrite CRabs_mult. apply (CRle_lt_trans _ (CRmax 1 (CRabs _ a) * CRabs _ (f x - f y))). apply CRmult_le_compat_r. apply CRabs_pos. apply CRmax_r. destruct H. specialize (c0 _ _ _ _ H0). apply (CRmult_lt_compat_r (CRmax 1 (CRabs _ a))) in c0. rewrite CRmult_assoc, CRinv_l, CRmult_1_r in c0. rewrite CRmult_comm. exact c0. apply posScale. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal