proposition: Lemma CRpower_N_bounded_step : forall (n:N) (c:Qpos) (x : CR), (forall e, - (proj1_sig c) <= approximate x e) -> (forall e, approximate x e <= proj1_sig c) -> (CRpower_N_bounded (1+n) c x == x * CRpower_N_bounded n c x)%CR.
proof: Proof. assert (forall i j : Q, i<=j -> Qmax i j == j)%Q as elim_max. { intros. apply (Qle_max_r i j), H. } assert (forall i j : Q, j<=i -> Qmin i j == j)%Q as elim_min. { intros. apply (Qle_min_r i j), H. } intros. assert (x <= ' ` c)%CR as xupper. { intro e. simpl. unfold Cap_raw. simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply H0. } assert (- ' ` c <= x)%CR as xlower. { intro e. simpl. unfold Cap_raw. simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply H. } destruct n as [|n]. - setoid_replace (CRpower_N_bounded 0 c x) with 1%CR. 2: intros e1 e2; apply Qball_Reflexive; rewrite Qplus_0_r; apply (Qpos_nonneg (e1+e2)). rewrite CRmult_1_r. simpl (1+0)%N. intros e1 e2. simpl. rewrite Qplus_0_r. rewrite elim_min. 2: apply H0. rewrite elim_max. 2: apply H. setoid_replace (` e1 + ` e2)%Q with (` (e1 * Qpos_inv (1 ↾ eq_refl * Qpos_power c 0))%Qpos + ` e2). apply (regFun_prf x). apply Qplus_comp. 2: reflexivity. simpl. change (/ (1*1)) with 1. rewrite Qmult_1_r. reflexivity. - rewrite CRmult_comm. pose (Qpos_max c (Qpos_power c (Z_of_N (N.pos n)))) as b. rewrite <- (CRmult_bounded_mult c). 2: exact xlower. 2: exact xupper. rewrite (CRmult_bounded_weaken c b). 2: exact xlower. 2: exact xupper. 2: apply Qpos_max_ub_l. rewrite (CRmult_uncurry_eq b). unfold CRpower_N_bounded. transitivity (Cmap QPrelengthSpace (uc_compose (Qmult_uncurry b) (uc_compose (together (Qpower_N_uc (N.pos n) c) (uc_id Q_as_MetricSpace)) (diag Q_as_MetricSpace))) x). + apply Cmap_wd_bounded with (c:=c). intros q H1. destruct H1. apply Qball_0. change (Qpower_positive (Qmax (- ` c) (Qmin (` c) q)) (1+n) == Qmax (- ` b) (Qmin (` b) (Qpower_positive (Qmax (- ` c) (Qmin (` c) q)) n)) * Qmax (- ` b) (Qmin (` b) q)). rewrite (elim_min _ q). 2: exact H2. rewrite (elim_max _ q). 2: exact H1. 2: exact (conj xlower xupper). rewrite (elim_min _ q). rewrite (elim_max _ q). rewrite Qpower_plus_positive. simpl. rewrite Qmult_comm. apply Qmult_comp. 2: reflexivity. assert (Qabs q <= `c). { apply AbsSmall_Qabs. split. exact H1. exact H2. } pose proof (Qpower_positive_abs_le q c n H3). clear H3. apply AbsSmall_Qabs in H4. destruct H4. rewrite elim_min, elim_max. reflexivity. apply (Qle_trans _ (-(Qpower_positive (`c) n))). apply Qopp_le_compat. apply (Qpos_max_ub_r c (Qpower_positive (` c) n ↾ Qpos_power_ispos c (Z.pos n))). exact H3. apply (Qle_trans _ (Qpower_positive (`c) n)). exact H4. apply (Qpos_max_ub_r c (Qpower_positive (` c) n ↾ Qpos_power_ispos c (Z.pos n))). apply (Qle_trans _ (-`c)). apply Qopp_le_compat, Qpos_max_ub_l. exact H1. apply (Qle_trans _ (`c)). apply H2. apply Qpos_max_ub_l. + rewrite (fast_MonadLaw2 QPrelengthSpace (ProductMS_prelength QPrelengthSpace QPrelengthSpace)). apply Cmap_wd. apply ucEq_equiv. intro a; reflexivity. intros e1 e2. split. rewrite Qplus_0_r. apply (mu_sum QPrelengthSpace e2 (cons e1 nil) (Qpower_N_uc (N.pos n) c)). apply (@ball_weak_le Q_as_MetricSpace (proj1_sig (Qpos_min (e1 * Qpos_inv ((n # 1) * Qpos_power c (Z.pred (Zpos n)) )) e1 + (e2 * Qpos_inv ((n # 1) * Qpos_power c (Z.pred (Zpos n)) )))%Qpos)). apply Qplus_le_l. apply Qpos_min_lb_l. apply (regFun_prf x). apply (@ball_weak_le Q_as_MetricSpace (proj1_sig (Qpos_min (e1 * Qpos_inv ((n # 1) * Qpos_power c (Z.pred (Zpos n)) )) e1 + e2)%Qpos)). apply Qplus_le_l. rewrite Qplus_0_r. apply Qpos_min_lb_r. apply (regFun_prf x). + intro e. simpl. unfold Cap_raw; simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply (Qle_trans _ (-Qpower_positive (` c) n)). apply Qopp_le_compat. apply (Qpos_max_ub_r c (Qpower_positive (` c) n ↾ Qpos_power_ispos c (Z.pos n))). assert (forall i j :Q, -j <= i -> -i <= j). { intros. rewrite <- (Qopp_involutive j). apply Qopp_le_compat, H1. } apply H1. clear H1. apply (Qle_trans _ _ _ (Qle_Qabs _)). rewrite Qabs_opp. apply (Qpower_positive_abs_le (Qmax (- ` c) (Qmin (` c) (approximate x ((1 # 2) * e * Qpos_inv ((n # 1) * Qpos_power c (Z.pred (Zpos n)) ))%Qpos))) c n). apply AbsSmall_Qabs. 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. + intro e. simpl. unfold Cap_raw; simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply (Qle_trans _ _ _ (Qle_Qabs _)). apply (Qle_trans _ (Qpower_positive (` c) n)). apply (Qpower_positive_abs_le (Qmax (- ` c) (Qmin (` c) (approximate x ((1 # 2) * e * Qpos_inv ((n # 1) * Qpos_power c (Z.pred (Zpos n)) ))%Qpos))) c n). apply AbsSmall_Qabs. 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. apply (Qpos_max_ub_r c (Qpower_positive (` c) n ↾ Qpos_power_ispos c (Z.pos n))). 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