proposition: Lemma bla: forall n m:nat, forall x:X, (ball (c^m) (@Banach_seq _ F n x) (@Banach_seq _ F (n+m) x)).
proof: Proof. Admitted. Lemma bla2: forall n:nat, forall x:X, (ball (Qpos_inv oneminc) x (@Banach_seq _ F n x)). Admitted. Lemma bla3: forall n m:nat, forall x:X, forall e, (ball e x (F x)) -> (ball (c^m*(Qpos_inv oneminc)*e) (@Banach_seq _ F n x) (@Banach_seq _ F m x)). Admitted. Variable x:X. Definition DiffSeries:=fun n => d (@Banach_seq _ F n x) (@Banach_seq _ F (S n) x). Require Import StreamMemo. Definition DiffStream:=(memo_list _ DiffSeries). Require Import CoqStreams. Definition GeometricSeriesCR (c:CR):= (ForAll (fun s:Stream CR => (CRabs ((hd (tl s))) <= c*(CRabs(hd s)))%CR)). Lemma GeomDiff:GeometricSeriesCR ('c)%CR DiffStream. unfold GeometricSeriesCR. unfold DiffStream. unfold memo_list. unfold memo_make. simpl. admit. Qed.
imports: CRtrans Qmetric ProductMetric CompleteProduct Unicode.Utf8 CPoly_Newton metric2.Classified Circle AbstractIntegration SimpleIntegration Qabs CRabs Interval CRGeometricSum