proposition: Lemma InfiniteGeometricSum_wd : forall (s : Stream Q) (a b : Q) (Gsa : GeometricSeries a s) (Gsb : GeometricSeries b s) (apos : 0 <= a) (aone : a < 1) (bpos : 0 <= b) (bone : b < 1), msp_eq (InfiniteGeometricSum apos aone Gsa) (InfiniteGeometricSum bpos bone Gsb).
proof: Proof. assert (forall (s : Stream Q) (a b : Q) (Gsa : GeometricSeries a s) (Gsb : GeometricSeries b s) (apos : 0 <= a) (aone : a < 1) (bpos : 0 <= b) (bone : b < 1), a <= b -> msp_eq (InfiniteGeometricSum apos aone Gsa) (InfiniteGeometricSum bpos bone Gsb)). { intros. intros e1 e2. change (approximate (InfiniteGeometricSum apos aone Gsa) e1) with (InfiniteGeometricSum_raw a s e1). rewrite (InfiniteGeometricSum_raw_correct apos aone _ Gsa). change (approximate (InfiniteGeometricSum bpos bone Gsb) e2) with (InfiniteGeometricSum_raw b s e2). rewrite (InfiniteGeometricSum_raw_correct bpos bone _ Gsb). simpl. pose proof (@InfiniteSum_fat_remove_filter (Pos.to_nat (InfiniteGeometricSum_maxIter a s e1)) (fun s0 : Stream Q => match Qabs (hd s0) / (1 - a) ?= proj1_sig e1 with | Gt => false | _ => true end) s 0%Q) as [i [H2 H3]]. apply (InfiniteGeometricSum_maxIter_correct apos aone _ Gsa). rewrite H2. pose proof (@InfiniteSum_fat_remove_filter (Pos.to_nat (InfiniteGeometricSum_maxIter b s e2)) (fun s0 : Stream Q => match Qabs (hd s0) / (1 - b) ?= proj1_sig e2 with | Gt => false | _ => true end) s 0%Q) as [j [H4 H5]]. apply (InfiniteGeometricSum_maxIter_correct bpos bone _ Gsb). rewrite H4. destruct (Nat.lt_ge_cases i j) as [H0|H0]. - rewrite Qplus_0_r. apply Nat.le_exists_sub in H0. destruct H0 as [k [H0 _]]. subst j. unfold Qball. clear H5. rewrite <- AbsSmall_Qabs, Qabs_Qminus. replace (k + S i)%nat with (S k + i)%nat by (rewrite Nat.add_succ_r; reflexivity). rewrite InfiniteSum_fat_minus. apply (Qle_trans _ (proj1_sig e1 + 0)). rewrite Qplus_0_r. apply (err_prop_correct apos aone). apply ForAll_Str_nth_tl, Gsa. apply H3. apply Qplus_le_r, Qpos_nonneg. - rewrite Qplus_0_r. apply Nat.le_exists_sub in H0. destruct H0 as [k [H0 _]]. subst i. unfold Qball. clear H3. rewrite <- AbsSmall_Qabs, Qabs_Qminus. rewrite Qabs_Qminus. rewrite InfiniteSum_fat_minus. apply (Qle_trans _ (0 + proj1_sig e2)). rewrite Qplus_0_l. apply (err_prop_correct bpos bone). apply ForAll_Str_nth_tl, Gsb. apply H5. apply Qplus_le_l, Qpos_nonneg. } intros. destruct (Qle_total a b). apply H, q. symmetry. apply H, q. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qpower Coq.QArith.Qabs Coq.ZArith.Zdiv