proposition: Lemma AQsqrt_mid_spec : AQsqrt_mid ^ (2:N)= 'a.
proof: Proof. assert (∀ ε, Qball (proj1_sig ε) ('(AQsqrt_mid_raw ε ^ (2:N))) ('a)) as P. { intros ε. apply Qball_Qabs. rewrite Qabs.Qabs_neg. eapply Qle_trans. 2: now apply Qpos_dlog2_spec. change (-( '(AQsqrt_mid_raw ε ^ 2) - 'a) ≤ ((2 ^ Qdlog2 (proj1_sig ε))%mc : Q)). rewrite <-rings.negate_swap_r. unfold AQsqrt_mid_raw. rewrite AQsqrt_mid_bounded_spec. rewrite rings.preserves_minus, preserves_shiftl. ring_simplify. apply shiftl_le_flip_l. etransitivity. apply (order_preserving _). now apply AQsqrt_loop_fst_upper_bound. rewrite preserves_nat_pow, rings.preserves_2. rewrite <-(int_pow_nat_pow (f:=cast nat Z)). rewrite shiftl_int_pow, <-int_pow_exp_plus by solve_propholds. apply int_pow_exp_le; [apply semirings.le_1_2|]. rewrite rings.preserves_plus, (naturals.to_semiring_twice _ _ (cast N Z)). rewrite (rings.preserves_plus _ 3), !rings.preserves_3. apply (order_reflecting (+ -(3 + 3))). ring_simplify. destruct (total (≤) (proj1_sig ε) 1). rewrite N_of_Z_nonneg. apply orders.eq_le. change (-Qdlog2 (proj1_sig ε) = 2 * -Qdlog2 (proj1_sig ε) + Qdlog2 (proj1_sig ε)). ring. change (0 ≤ -Qdlog2 (proj1_sig ε)). now apply rings.flip_nonpos_negate, Qdlog2_nonpos. rewrite N_of_Z_nonpos. now apply Qdlog2_nonneg. change (-Qdlog2 (proj1_sig ε) ≤ 0). now apply rings.flip_nonneg_negate, Qdlog2_nonneg. change ('(AQsqrt_mid_raw ε ^ 2) - 'a ≤ (0:Q)). apply rings.flip_nonpos_minus. apply (order_preserving _). now apply AQsqrt_mid_bounded_raw_square_upper_bound. } rewrite <-(ARpower_N_bounded_N_power _ _ 4). - intros ε1 ε2. rewrite Qplus_0_r. simpl. rewrite lattices.meet_r, lattices.join_r. + apply ball_weak. apply Qpos_nonneg. apply ball_weak_le with (proj1_sig (ε1 * Qpos_inv (8 # 1))%Qpos). change ('ε1 / (8#1) ≤ 'ε1). rewrite <-(rings.mult_1_r ('ε1)) at 2. apply Qmult_le_l. apply Qpos_ispos. discriminate. assert (QposEq (ε1 * Qpos_inv ((2#1) * Qpos_power (' 4) 1)) (ε1 * Qpos_inv (8#1))). unfold QposEq. simpl. pose proof AQposAsQpos_preserves_4. unfold equiv, sig_equiv, equiv, stdlib_rationals.Q_eq in H5. simpl. rewrite H5. reflexivity. rewrite H5. apply P. + transitivity (0:AQ). apply rings.flip_nonneg_negate. now apply semirings.le_0_4. now apply AQsqrt_mid_bounded_raw_lower_bound. + now apply AQsqrt_mid_bounded_raw_upper_bound. - split. transitivity (0:AR). apply rings.flip_nonneg_negate. apply (semirings.preserves_nonneg (f:=cast AQ AR)). now apply semirings.le_0_4. now apply AQsqrt_mid_nonneg. now apply AQsqrt_mid_upper_bound. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.setoid_ring.Ring CoRN.stdlib_omissions.Z CoRN.model.totalorder.QposMinMax CoRN.metric2.Complete CoRN.model.metric2.Qmetric Coq.ZArith.ZArith CoRN.util.Qdlog CoRN.reals.fast.CRroot CoRN.reals.faster.ARabs MathClasses.interfaces.abstract_algebra MathClasses.theory.shiftl MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.reals.faster.ARArith