proposition: Lemma CRpower_N_bounded_correct : forall (n:N) (c:Qpos) (x : CR), (- (' (proj1_sig c)) <= x /\ x <= 'proj1_sig c)%CR -> (CRpower_slow x (N.to_nat n) == CRpower_N_bounded n c x)%CR.
proof: Proof. assert (∀ (n : nat) (c : Qpos) (x : CR), (forall e, - (proj1_sig c) <= approximate x e) -> (forall e, approximate x e <= proj1_sig c) → msp_eq (CRpower_slow x n) (CRpower_N_bounded (N.of_nat n) c x)). induction n. - intros. intros e1 e2. simpl. apply Qball_Reflexive. rewrite Qplus_0_r. apply (Qpos_nonneg (e1+e2)). - intros. change (S n) with (1+n)%nat. rewrite Nnat.Nat2N.inj_add. change (N.of_nat 1) with 1%N. rewrite CRpower_N_bounded_step. 2: exact H. change (CRpower_slow x (1 + n)) with (x * CRpower_slow x n)%CR. apply CRmult_wd. reflexivity. apply IHn. exact H. exact H0. exact H0. - intros. transitivity (CRpower_N_bounded (N.of_nat (N.to_nat n)) c x). 2: rewrite Nnat.N2Nat.id; reflexivity. transitivity (CRpower_N_bounded (N.of_nat (N.to_nat n)) c (CRboundAbs c x)). transitivity (CRpower_slow (CRboundAbs c x) (N.to_nat n)). apply CRpower_slow_wd. symmetry. apply CRboundAbs_Eq. apply H0. apply H0. apply H. intro e. simpl. apply Qmax_ub_l. intros e. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. apply Cmap_wd. apply ucEq_equiv; intro a; reflexivity. apply CRboundAbs_Eq. apply H0. apply H0. 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