proposition: Lemma Qdlog_spec_bounded (b : nat) (n : Z) (x : Q) : 2 ≤ n → Qdlog2 x ≤ ('b) → 1 ≤ x → 'n ^ Qdlog_bounded b n x ≤ x ∧ x < 'n ^ (1 + Qdlog_bounded b n x).
proof: Proof. intros En Eb Ex. apply (order_preserving (cast Z Q)) in En. assert (0 < ('n : Q)) by (apply orders.lt_le_trans with 2; [solve_propholds | assumption]). revert x Eb Ex. induction b. intros x Eb Ex. split; [assumption|]. apply orders.lt_le_trans with 2; try assumption. apply Qdlog2_0. apply orders.lt_le_trans with 1; [ solve_propholds | easy]. apply (antisymmetry (≤)); try assumption. now apply Qdlog2_nonneg. intros x Eb Ex. unfold Qdlog_bounded. case (decide_rel); [intuition |]; intros E. apply orders.not_lt_le_flip in E. assert (x = 'n * (x / 'n)) as Ex2. rewrite (commutativity x), associativity. rewrite dec_recip_inverse, rings.mult_1_l; [reflexivity |]. now apply orders.lt_ne_flip. rewrite peano_naturals.S_nat_plus_1, rings.preserves_plus, rings.preserves_1 in Eb. assert (1 ≤ x / 'n). apply (order_reflecting (('n:Q) *.)). now rewrite <-Ex2, rings.mult_1_r. destruct (IHb (x / 'n)); trivial. transitivity (Qdlog2 (x /2)%mc). apply Qdlog2_preserving. apply orders.lt_le_trans with 1; [solve_propholds | assumption]. apply (maps.order_preserving_nonneg (.*.) x). now transitivity (1:Q). apply dec_fields.flip_le_dec_recip; [solve_propholds | assumption]. rewrite <-Qdlog2_half. now apply rings.flip_le_minus_l. now apply orders.lt_le_trans with 1; [solve_propholds | assumption]. fold Qdlog_bounded. setoid_rewrite int_pow_S_nonneg at 1. 2: apply Qdlog_bounded_nonneg. setoid_rewrite int_pow_S_nonneg. 2: (apply semirings.nonneg_plus_compat; [easy | now apply Qdlog_bounded_nonneg]). setoid_rewrite Ex2 at 2 3. split. now apply (order_preserving (('n:Q) *.)). now apply (strictly_order_preserving (('n:Q) *.)). 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