proposition: Lemma Qdiff_power : forall (n : nat) (x y : Q) (c : Qpos), (-`c <= x <= `c) -> (-`c <= y <= `c) -> Qabs (x^Z.of_nat n - y^Z.of_nat n) <= Qabs(x-y) * (Z.of_nat n#1) * (`c) ^ (Z.pred (Z.of_nat n)).
proof: Proof. induction n. - intros. apply Qmult_le_0_compat. apply Qmult_le_0_compat. apply Qabs_nonneg. discriminate. apply (Qpos_nonneg (Qpos_power c (Z.pred (Z.of_nat 0)))). - intros. change (S n) with (1 + n)%nat. rewrite Nat2Z.inj_add, Qpower_plus', Qpower_plus'. simpl (x ^ Z.of_nat 1). simpl (y ^ Z.of_nat 1). setoid_replace (x * x ^ Z.of_nat n - y * y ^ Z.of_nat n)%Q with ((x-y)*x ^ Z.of_nat n + y * (x ^ Z.of_nat n - y ^ Z.of_nat n))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply (Qle_trans _ _ _ (Qabs_triangle _ _)). rewrite Qabs_Qmult, Qabs_Qmult. apply (Qle_trans _ (Qabs (x-y) * (`c) ^ Z.of_nat n + Qabs (x - y) * (Z.of_nat n # 1) * ` c ^ Z.pred (Z.of_nat n) * Qabs y)). apply Qplus_le_compat. + rewrite Qmult_comm, (Qmult_comm (Qabs (x-y))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. destruct n. apply Qle_refl. apply Qpower_positive_abs_le. apply AbsSmall_Qabs, H. + rewrite Qmult_comm. apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply IHn. exact H. exact H0. + clear IHn. rewrite <- Qmult_assoc, <- Qmult_assoc, <- Qmult_plus_distr_r. rewrite Qmult_comm, <- Qmult_assoc, (Qmult_comm (Qabs (x-y))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply (Qle_trans _ (` c ^ Z.of_nat n + (Z.of_nat n # 1) * (` c ^ (Z.of_nat n)))). apply Qplus_le_r. rewrite Qmult_comm, (Qmult_comm (Z.of_nat n # 1)). apply Qmult_le_compat_r. apply (Qle_trans _ (`c ^ Z.of_nat 1 * ` c ^ Z.pred (Z.of_nat n))). rewrite Qmult_comm. apply Qmult_le_compat_r. simpl. apply AbsSmall_Qabs. exact H0. apply Qpower_pos. apply Qpos_nonneg. rewrite <- Qpower_plus. 2: apply Qpos_nonzero. replace (Z.of_nat 1 + Z.pred (Z.of_nat n))%Z with (Z.of_nat n). apply Qle_refl. rewrite Z.add_1_l. rewrite Z.succ_pred. reflexivity. unfold Qle; simpl. rewrite Z.mul_1_r. apply Nat2Z.is_nonneg. rewrite <- (Qmult_1_l (` c ^ Z.of_nat n)) at 1. rewrite <- Qmult_plus_distr_l. setoid_replace (1 + (Z.of_nat n # 1)) with (Z.of_nat 1 + Z.of_nat n#1). rewrite Qmult_comm. rewrite (Qmult_comm (Z.of_nat 1 + Z.of_nat n#1)). apply Qmult_le_compat_r. replace (Z.pred (Z.of_nat 1 + Z.of_nat n)) with (Z.of_nat n). apply Qle_refl. rewrite <- Nat2Z.inj_add. rewrite Nat2Z.inj_succ. rewrite <- Zpred_succ. reflexivity. rewrite <- Nat2Z.inj_add. discriminate. unfold equiv, stdlib_rationals.Q_eq, Qeq, Qplus, Qnum, Qden. simpl (1*1)%Z. rewrite Z.mul_1_r, Z.mul_1_r. simpl (1*1)%positive. rewrite Z.mul_1_r. reflexivity. + rewrite <- Nat2Z.inj_add. discriminate. + rewrite <- Nat2Z.inj_add. discriminate. 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