proposition: Lemma CompactImproveApproxCauchy2 : forall (m n:nat) s (k d1 d2:Qpos) pt Hpt, proj1_sig k < 1 -> ball (proj1_sig k ^ (Z.of_nat m) * ((((1#1)+proj1_sig k)*proj1_sig d1+proj1_sig d2) *(1-proj1_sig k^Z.of_nat (S n))/(1-proj1_sig k))) (@CompactImproveApproximation s k d1 d2 pt Hpt m) (@CompactImproveApproximation s k d1 d2 pt Hpt (m + n)).
proof: Proof. induction m; intros n s k d1 d2 pt Hpt Hk. simpl (proj1_sig k ^ Z.of_nat 0). rewrite Qmult_1_l. apply CompactImproveApproxCauchy1; assumption. pose (e':=(CompactTotallyBoundedStreamCauchyLemma n _ (((1#1)+k)*(k*d1) + (k*d2)) Hk)%Qpos). assert (~proj1_sig k==0) as knz. { destruct k. simpl. intro abs. apply (Qlt_not_le _ _ q). rewrite abs. apply Qle_refl. } assert (Qeq (proj1_sig k ^ (Z.of_nat (S m)) * ((((1#1)+proj1_sig k)*proj1_sig d1+proj1_sig d2) *(1-proj1_sig k^Z.of_nat (S n))/(1-proj1_sig k))) (proj1_sig (Qpos_power k (Z.of_nat m)*exist _ _ e')%Qpos)). { rewrite Nat2Z.inj_succ. simpl. setoid_replace (proj1_sig k ^ (Z.succ (Z.of_nat m))) with (proj1_sig k ^ (1+Z.of_nat m)). rewrite Qpower_plus. simpl. field. intros H0. apply (Qlt_not_le _ _ Hk). rewrite -> Qle_minus_iff. setoid_replace (proj1_sig k + - (1)) with (-(1-proj1_sig k)) by (simpl; ring). rewrite -> H0. discriminate. exact knz. rewrite <- Z.add_1_l. reflexivity. } rewrite H. clear H. change (S m + n)%nat with (S (m + n))%nat. unfold Str_nth. simpl. destruct (@HausdorffBallHausdorffBallStrong X locatedX (@proj1_sig Q (Qlt 0) d1 + @proj1_sig Q (Qlt 0) k * @proj1_sig Q (Qlt 0) d1) (@approximate _ (FinEnum_ball X) s d1) (@approximate _ (FinEnum_ball X) s (k * d1)%Qpos) (@regFun_prf _ (FinEnum_ball X) s d1 (k * d1)%Qpos)) as [f _]. destruct (f pt Hpt d2) as [pt' [Hpt' _]]. simpl. apply (IHm n s k (k*d1)%Qpos (k*d2)%Qpos pt' Hpt'); 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