proposition: Lemma CompactImproveApproxCauchy1 : forall n s (k d1 d2:Qpos) pt Hpt, proj1_sig k < 1 -> ball ((((1#1)+proj1_sig k)*proj1_sig d1+ proj1_sig d2) * (1-proj1_sig k^Z.of_nat(S n))/(1-proj1_sig k)) pt (@CompactImproveApproximation s k d1 d2 pt Hpt n).
proof: Proof. induction n; intros s k d1 d2 pt Hpt Hk. apply ball_refl. apply Qlt_le_weak. apply (CompactTotallyBoundedStreamCauchyLemma O k (((1#1) + k) * d1 + d2)%Qpos), Hk. simpl (CompactImproveApproximation s k d1 d2 Hpt (S n)). set (e:=(((1#1) + proj1_sig k) * proj1_sig d1 + proj1_sig d2) * (1 - proj1_sig k ^ Z.of_nat (S (S n))) / (1 - proj1_sig k)) in *. set (e0:=((d1 + k * d1 + d2) + exist _ _ (CompactTotallyBoundedStreamCauchyLemma n _ (((1#1) + k)*(k*d1) + (k*d2)) Hk))%Qpos). setoid_replace e with (proj1_sig e0). - 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 (Qpos2QposInf d1)) (@approximate _ (FinEnum_ball X) s (Qpos2QposInf (k * d1))) (@regFun_prf _ (FinEnum_ball X) s d1 (k * d1)%Qpos)) as [f _]. destruct (f pt Hpt d2) as [pt' [Hpt' Hpt'']]. unfold e0. apply ball_triangle with pt'. assumption. apply (IHn s k (k * d1)%Qpos (k * d2)%Qpos pt' Hpt' Hk). - unfold e0, e. simpl. assert (~proj1_sig k==0). { destruct k. simpl. intro abs. apply (Qlt_not_le _ _ q). rewrite abs. apply Qle_refl. } rewrite <- Pos.add_1_l. rewrite Qpower_plus_positive. 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. 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