proposition: Lemma CompactTotallyBoundedIndexLemma : forall (e k d1 d2:Qpos), proj1_sig k <= 1#2 -> ((1+proj1_sig k)*proj1_sig d1 + proj1_sig d2) *proj1_sig k^(CompactTotallyBoundedIndex e d1 d2)/(1-proj1_sig k) <= proj1_sig e.
proof: Proof. intros e k d1 d2 khalf. unfold Qdiv. rewrite Qmult_comm, Qmult_assoc. apply (Qle_trans _ (((3#1)*proj1_sig d1+(2#1)*proj1_sig d2) * proj1_sig k ^(CompactTotallyBoundedIndex e d1 d2))). - apply Qmult_le_compat_r. 2: apply Qpower_pos, Qpos_nonneg. apply (Qle_trans _ ((2#1) * ((1 + proj1_sig k) * proj1_sig d1 + proj1_sig d2))). apply Qmult_le_compat_r. 2: apply (Qpos_nonneg (((1#1)+k)*d1+d2)%Qpos). apply Qle_shift_inv_r. unfold Qminus. rewrite <- Qlt_minus_iff. apply (Qle_lt_trans _ _ _ khalf). reflexivity. setoid_replace 1%Q with ((2#1)*(1#2)) at 1 by reflexivity. apply Qmult_le_l. reflexivity. apply (Qplus_le_l _ _ (proj1_sig k - (1#2))). ring_simplify. exact khalf. rewrite Qmult_plus_distr_r. apply Qplus_le_l. rewrite Qmult_assoc. apply Qmult_le_r. apply Qpos_ispos. apply (Qplus_le_r _ _ (-(2#1))). ring_simplify. setoid_replace 1%Q with ((2#1)*(1#2)) by reflexivity. apply Qmult_le_l. reflexivity. exact khalf. - apply (Qle_trans _ (((3#1) * proj1_sig d1 + (2#1) * proj1_sig d2) * (1#2) ^ (CompactTotallyBoundedIndex e d1 d2))). apply Qmult_le_l. apply (Qpos_ispos ((3#1) * d1 + (2#1) * d2)%Qpos). rewrite <- (Z2Nat.id (CompactTotallyBoundedIndex e d1 d2)). apply Qpower_inc. apply Qpos_ispos. exact khalf. apply Z.log2_up_nonneg. rewrite <- (Qmult_1_r (proj1_sig e)). rewrite <- (Qpower_1 (CompactTotallyBoundedIndex e d1 d2)). setoid_replace (1#1)%Q with ((2#1)*(1#2))%Q by reflexivity. rewrite Qmult_power, Qmult_assoc. apply Qmult_le_compat_r. 2: apply Qpower_pos; discriminate. rewrite <- (Zpower_Qpower 2 (CompactTotallyBoundedIndex e d1 d2)). 2: apply Z.log2_up_nonneg. rewrite (Qmult_comm (proj1_sig e)). apply (Qmult_le_r _ _ (/proj1_sig e)). apply Qinv_lt_0_compat, Qpos_ispos. rewrite <- Qmult_assoc, Qmult_inv_r, Qmult_1_r. unfold CompactTotallyBoundedIndex. unfold Qdiv. assert (0 < ((3#1) * proj1_sig d1 + (2#1) * proj1_sig d2) * / proj1_sig e). { apply (Qle_lt_trans _ (((3#1) * proj1_sig d1 + (2#1) * proj1_sig d2)*0)). rewrite Qmult_0_r. discriminate. apply Qmult_lt_l. apply (Qpos_ispos ((3#1)*d1 + (2#1)*d2)). apply Qinv_lt_0_compat, Qpos_ispos. } revert H. generalize (((3#1) * proj1_sig d1 + (2#1) * proj1_sig d2) * / proj1_sig e). intros q qpos. apply (Qle_trans _ _ _ (Qle_ceiling q)). rewrite <- Q.Zle_Qle. apply Z.log2_up_le_pow2. rewrite Q.Zlt_Qlt. exact (Qlt_le_trans _ _ _ qpos (Qle_ceiling q)). apply Z.le_refl. apply Qpos_nonzero. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround