proposition: Lemma AQsqrt_mid_bounded_prf: is_RegularFunction_noInf _ (AQsqrt_mid_raw : Qpos → AQ_as_MetricSpace).
proof: Proof. assert (∀ n m, m ≤ n → ball (2 ^ (-cast N Z m - 2)) (AQsqrt_mid_bounded_raw (n + 3) : AQ_as_MetricSpace) (AQsqrt_mid_bounded_raw (m + 3))). intros n m E. simpl. apply Qball_Qabs. rewrite Qabs.Qabs_pos. change ('AQsqrt_mid_bounded_raw (n + 3) - 'AQsqrt_mid_bounded_raw (m + 3) ≤ ((2 ^ (-'m - 2))%mc : Q)). rewrite <-rings.preserves_minus, <-(rings.mult_1_l (2 ^ (-'m - 2))). rewrite <-shiftl_int_pow. rewrite <-(rings.preserves_1 (f:=cast AQ Q)), <-(preserves_shiftl (f:=cast AQ Q)). apply (order_preserving _). mc_setoid_replace ((-'m - 2)%mc : Z) with ((1 - '(m + 3))%mc : Z). apply AQsqrt_mid_bounded_regular_aux1. now refine (order_preserving (+ (3%mc:N)) _ _ _). rewrite rings.preserves_plus, rings.preserves_3. ring. change (0 ≤ (('AQsqrt_mid_bounded_raw (n + 3) - 'AQsqrt_mid_bounded_raw (m + 3))%mc : Q)). apply rings.flip_nonneg_minus. apply (order_preserving _). apply AQsqrt_mid_bounded_regular_aux2. now refine (order_preserving (+ (3:N)) _ _ _). assert (∀ ε1 ε2 : Qpos, N_of_Z (-Qdlog2 (proj1_sig ε2)) ≤ N_of_Z (-Qdlog2 (proj1_sig ε1)) → ball (proj1_sig ε1 + proj1_sig ε2) (AQsqrt_mid_raw ε1 : AQ_as_MetricSpace) (AQsqrt_mid_raw ε2)). { intros ε1 ε2 E. unfold AQsqrt_mid_raw. eapply ball_weak_le; auto. change ((2%mc:Q) ^ (-'N_of_Z (-Qdlog2 (proj1_sig ε2)) - 2) ≤ proj1_sig ε1 + proj1_sig ε2). apply semirings.plus_le_compat_l. now apply orders.lt_le, Qpos_ispos. destruct (total (≤) (proj1_sig ε2) 1). rewrite N_of_Z_nonneg. change (- (-Qdlog2 (proj1_sig ε2))%Z) with (- -Qdlog2 (proj1_sig ε2)). rewrite rings.negate_involutive. rewrite int_pow_exp_plus by solve_propholds. transitivity ((2 ^ Qdlog2 (proj1_sig ε2))%mc : Q). 2: now apply Qdlog2_spec, Qpos_ispos. rewrite <-(rings.mult_1_r (2 ^ Qdlog2 (proj1_sig ε2) : Q)) at 2. now apply (order_preserving (_ *.)). change (0 ≤ -Qdlog2 (proj1_sig ε2)). now apply rings.flip_nonpos_negate, Qdlog2_nonpos. transitivity (1:Q); auto. rewrite N_of_Z_nonpos; [easy|]. change (-Qdlog2 (proj1_sig ε2) ≤ 0). now apply rings.flip_nonneg_negate, Qdlog2_nonneg. } intros ε1 ε2. destruct (total (≤) (N_of_Z (-Qdlog2 (proj1_sig ε1))) (N_of_Z (-Qdlog2 (proj1_sig ε2)))); auto. apply ball_sym. rewrite Qplus_comm. auto. 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