proposition: Lemma Qpower_N_uc_prf (c:Qpos) : @is_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace (fun x => Qpower (QboundAbs c x) (Z_of_N n)) (Qpower_N_modulus c).
proof: Proof. unfold Qpower_N_modulus. destruct n as [|p]. - simpl. intros e x y E. apply ball_refl, Qpos_nonneg. - clear n. intros e x y E. unfold ball_ex in E. simpl (Z.of_N (N.pos p)). apply AbsSmall_Qabs. apply AbsSmall_Qabs in E. assert (-` c <= QboundAbs c x ∧ QboundAbs c x <= ` c). { split. apply Qmax_ub_l. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. } assert (- ` c <= QboundAbs c y ∧ QboundAbs c y <= ` c). { split. apply Qmax_ub_l. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. } pose proof (positive_nat_Z p). rewrite <- H1. apply (Qle_trans _ _ _ (Qdiff_power (Pos.to_nat p) _ _ c H H0)). clear H H0. rewrite <- Qmult_assoc. apply (Qle_trans _ (Qabs (x-y) * ((Z.pos p # 1) * ` c ^ Z.pred (Z.pos p)))). rewrite H1. apply Qmult_le_compat_r. apply QboundAbs_contract. apply (Qpos_nonneg ((p#1) * Qpos_power c (Z.pred (Z.pos p)))). apply (Qle_trans _ (`e * / proj1_sig ((Z.pos p # 1)%Q ↾ eq_refl * Qpos_power c (Z.pred (Z.pos p)))%Qpos * ((Z.pos p # 1) * ` c ^ Z.pred (Z.pos p)))). apply Qmult_le_compat_r. apply E. apply (Qpos_nonneg ((p#1) * Qpos_power c (Z.pred (Z.pos p)))). rewrite Qmult_comm, Qmult_assoc. apply Qle_shift_div_r. apply (Qpos_ispos ((p#1) * Qpos_power c (Z.pred (Z.pos p)))). rewrite Qmult_comm. apply Qle_refl. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.ProductMetric CoRN.reals.fast.CRArith Coq.QArith.Qpower Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax MathClasses.interfaces.canonical_names MathClasses.interfaces.additional_operations