proposition: Lemma root_loop_error : forall (e:Qpos) n b err, (1 <= b) -> root_has_error (1#err) b -> (1#(iter_nat n _ (fun x => (x * x)%positive) err))<=proj1_sig e -> root_has_error (Qpos_min (1 # err) e) (root_loop e n b err).
proof: Proof. induction n. intros b err Hb0 Hb1 He. simpl in *. setoid_replace (Qpos_min (1 # err) e) with (1#err)%Qpos; try assumption. unfold QposEq. rewrite <- Qpos_le_min_l. assumption. intros b err Hb0 Hb1 He. simpl in *. destruct (Qlt_le_dec_fast (proj1_sig e) (1 # err)) as [A|A]. apply root_has_error_le with (Qpos_min (1#(err*err)) e). apply Qle_trans with 1. apply Qle_trans with (1#err); auto with *. apply Qpos_min_lb_l. apply root_loop_one_le. apply approximateQ_big. apply root_step_one_le; assumption. apply Qpos_min_glb. apply Qle_trans with (1#err*err). apply Qpos_min_lb_l. change (1*err <= err*err)%Z; auto with *. apply Qpos_min_lb_r. apply IHn; try assumption. apply approximateQ_big. apply root_step_one_le; assumption. assert (QposEq (1#err*err) ((1#(2*(err * err)))+(1#(2*(err * err))))). { unfold QposEq. simpl. ring_simplify. constructor. } rewrite H. clear H. apply root_has_error_ball with (root_step b). simpl. ring_simplify. unfold Qmult, Qle; simpl. auto with *. apply root_step_one_le; assumption. apply approximateQ_big. apply root_step_one_le; assumption. apply (root_step_error b (1#err)); try assumption. unfold Qle; simpl; auto with *. apply approximateQ_correct. replace (iter_nat n positive (fun x : positive => (x * x)%positive) (err * err)%positive) with (iter_nat n positive (fun x : positive => (x * x)%positive) err * iter_nat n positive (fun x : positive => (x * x)%positive) err)%positive. assumption. clear - n. induction n; try constructor. simpl in *. rewrite IHn. reflexivity. setoid_replace (Qpos_min (1 # err) e) with (1#err)%Qpos; try assumption. unfold QposEq. rewrite <- Qpos_le_min_l. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.Q_in_CReals CoRN.reals.fast.CRpower CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.NRootIR CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.PowerBound CoRN.transc.RealPowers CoRN.reals.fast.ContinuousCorrect CoRN.tactics.Qauto CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra