proposition: Lemma CompactTotallyBounded_prf : forall (s:Compact X) (k d1 d2:Qpos) (pt:X) Hpt, proj1_sig k <= 1#2 -> is_RegularFunction (@ball X) (@CompactTotallyBounded_raw s k d1 d2 pt Hpt).
proof: Proof. unfold CompactTotallyBounded_raw, is_RegularFunction. cut (forall (s : Compact X) (k d1 d2 : Qpos) (pt : X) (Hpt : InFinEnumC pt (approximate s d1)) (e1 e2 : Qpos), proj1_sig k <= 1#2 -> (Z.to_nat (CompactTotallyBoundedIndex e1 d1 d2) <= Z.to_nat (CompactTotallyBoundedIndex e2 d1 d2))%nat -> ball (proj1_sig e1 + proj1_sig e2) (@CompactImproveApproximation s k d1 d2 pt Hpt (Z.to_nat (CompactTotallyBoundedIndex e1 d1 d2))) (@CompactImproveApproximation s k d1 d2 pt Hpt (Z.to_nat (CompactTotallyBoundedIndex e2 d1 d2)))). - intros Z s k d1 d2 pt Hpt khalf e1 e2. destruct (le_lt_dec (Z.to_nat (CompactTotallyBoundedIndex e1 d1 d2)) (Z.to_nat (CompactTotallyBoundedIndex e2 d1 d2))). apply Z; auto. rewrite Qplus_comm. apply ball_sym. apply Z; auto with *. - intros s k d1 d2 pt Hpt e1 e2 khalf H. set (A:=Z.to_nat (CompactTotallyBoundedIndex e1 d1 d2)) in *. set (B:=Z.to_nat (CompactTotallyBoundedIndex e2 d1 d2)) in *. rewrite <- (Nat.sub_add _ _ H). rewrite Nat.add_comm. assert (proj1_sig k < 1) as Y. { apply (Qle_lt_trans _ _ _ khalf). reflexivity. } assert (Y0:= (CompactTotallyBoundedStreamCauchyLemma (B-A) k (((1#1)+k)*d1 + d2) Y)%Qpos). apply ball_weak_le with (proj1_sig (Qpos_power k (Z.of_nat A)*(exist _ _ Y0))%Qpos). 2: apply CompactImproveApproxCauchy2; exact Y. simpl. unfold Qdiv. set (C:=(((1 + proj1_sig k) * proj1_sig d1 + proj1_sig d2) * proj1_sig k ^ Z.of_nat A * / (1 - proj1_sig k))). setoid_replace ( proj1_sig k ^ Z.of_nat A * (((1 + proj1_sig k) * proj1_sig d1 + proj1_sig d2) * (1 - Qpower_positive (proj1_sig k) (Pos.of_succ_nat (B - A))) * / (1 - proj1_sig k))) with ((1 - proj1_sig k ^ Z.of_nat (S (B - A))) * C) by (unfold C; simpl; ring). apply Qle_trans with (1*C). apply Qmult_le_r. unfold C. apply (Qle_lt_trans _ (0 *(/(1-proj1_sig k)))). rewrite Qmult_0_l. discriminate. apply Qmult_lt_r. apply Qinv_lt_0_compat. unfold Qminus. rewrite <- Qlt_minus_iff. exact Y. apply (Qpos_ispos ((((1#1) + k) * d1 + d2) * Qpos_power k (Z.of_nat A))). rewrite -> Qle_minus_iff. ring_simplify. apply Qpower_pos_positive. apply Qpos_nonneg. rewrite Qmult_1_l. apply Qle_trans with (proj1_sig e1). unfold A in C. unfold C. rewrite Z2Nat.id. apply CompactTotallyBoundedIndexLemma. exact khalf. apply Z.log2_up_nonneg. rewrite <- Qplus_0_r at 1. apply Qplus_le_r, Qpos_nonneg. 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