proposition: Lemma Qdlog2_spec (x : Q) : 0 < x → 2 ^ Qdlog2 x ≤ x ∧ x < 2 ^ (1 + Qdlog2 x).
proof: Proof. intros E1. unfold Qdlog2. case (decide_rel _); intros E2. destruct (decide (x = 1)) as [E3|E3]. rewrite E3. compute; repeat split; discriminate. assert (1 < Qceiling (/x))%Z. apply (strictly_order_reflecting (cast Z Q)). apply orders.lt_le_trans with (/x). apply dec_fields.flip_lt_dec_recip_r; trivial. apply orders.lt_iff_le_ne. tauto. now apply Qle_ceiling. split. setoid_rewrite int_pow_negate. apply dec_fields.flip_le_dec_recip_l; trivial. transitivity ('Qceiling (/x)). now apply Qle_ceiling. change 2 with ('(2 : Z)). rewrite <-Qpower.Zpower_Qpower. apply (order_preserving _). now apply Z.log2_up_spec. now apply Z.log2_up_nonneg. mc_setoid_replace (1 - Z.log2_up (Qceiling (/x))) with (-Z.pred (Z.log2_up (Qceiling (/x)))). rewrite int_pow_negate. apply dec_fields.flip_lt_dec_recip_r. solve_propholds. apply orders.le_lt_trans with ('Z.pred (Qceiling (/x))). change 2 with ('(2 : Z)). rewrite <-Qpower.Zpower_Qpower. apply (order_preserving _). now apply Z.lt_le_pred, Z.log2_up_spec. now apply Z.lt_le_pred, Z.log2_up_pos. rewrite <-Z.sub_1_r. now apply Qceiling_lt. rewrite <-Z.sub_1_r. change (1 - Z.log2_up (Qceiling (/ x)) = -(Z.log2_up (Qceiling (/ x)) - 1)). now rewrite <-rings.negate_swap_l, commutativity. apply orders.le_flip in E2. split. transitivity ('Qfloor x). change 2 with ('(2 : Z)). rewrite <-Qpower.Zpower_Qpower. apply (order_preserving _). now apply Z.log2_spec, Qfloor_pos. now apply Z.log2_nonneg. now apply Qfloor_le. apply orders.lt_le_trans with ('Z.succ (Qfloor x)). rewrite <-Z.add_1_r. now apply Qlt_floor. rewrite Z.add_1_l. change 2 with ('(2 : Z)). rewrite <-Qpower.Zpower_Qpower. apply (order_preserving _). now apply Z.le_succ_l, Z.log2_spec, Qfloor_pos. now apply Zle_le_succ, Z.log2_nonneg. Qed.
imports: Coq.ZArith.ZArith Coq.QArith.QArith Coq.QArith.Qround CoRN.stdlib_omissions.Q MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.theory.int_pow MathClasses.orders.rationals MathClasses.implementations.stdlib_rationals MathClasses.implementations.positive_semiring_elements