proposition: Lemma CompactTotallyBoundedInCompact : forall (s:Compact X) (k d1 d2:Qpos) (khalf : proj1_sig k <= 1#2) (pt:X) Hpt, inCompact (@CompactTotallyBounded_fun s k d1 d2 khalf pt Hpt) s.
proof: Proof. intros s k d1 d2 khalf pt Hpt e1 e2. simpl. destruct (@StreamInCompactApprox (Z.to_nat (CompactTotallyBoundedIndex e1 d1 d2)) s k d1 d2 pt Hpt) as [q Hq Hq0]. apply FinSubset_ball_closed. intros d dpos. apply FinSubset_ball_weak_le with (d + (proj1_sig q + proj1_sig e2)). simpl. rewrite -> Qle_minus_iff. setoid_replace (proj1_sig e1 + proj1_sig e2 + d + - (d + (proj1_sig q + proj1_sig e2))) with (proj1_sig e1 + - proj1_sig q) by (simpl; ring). rewrite <- Qle_minus_iff. unfold QposEq in Hq0. rewrite -> Hq0. eapply Qle_trans;[|apply (CompactTotallyBoundedIndexLemma e1 k d1 d2)]. simpl. rewrite Z2Nat.id. cut (0 <= proj1_sig k ^ (CompactTotallyBoundedIndex e1 d1 d2)). { generalize ( proj1_sig k ^ (CompactTotallyBoundedIndex e1 d1 d2)). intros z Hz. clear - Hz khalf. apply Qle_shift_div_l. unfold Qminus. rewrite <- Qlt_minus_iff. apply (Qle_lt_trans _ _ _ khalf). reflexivity. rewrite <- Qmult_assoc, Qmult_comm. apply Qmult_le_compat_r. 2: exact Hz. apply (Qle_trans _ ((1 + proj1_sig k) * proj1_sig d1 + 0)). rewrite Qplus_0_r, Qmult_comm. apply Qmult_le_compat_r. 2: apply Qpos_nonneg. apply Qplus_le_r. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qplus_le_r, Qpos_nonneg. } apply Qpower_pos. apply Qpos_nonneg. apply Z.log2_up_nonneg. exact khalf. eapply FinSubset_ball_triangle_r;[|apply regFun_prf]. replace d with (proj1_sig (exist _ _ dpos)) by reflexivity. apply FinSubset_ball_weak_le with (e1:=0). apply Qpos_nonneg. assumption. 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