proposition: Lemma lowDistApprox_repeat_scale_limit : forall (A : Set)(c : Comp A)(P : A -> bool), well_formed_comp c -> (exists a, In a (filter P (getSupport c))) -> (forall a, rat_inf_limit (lowDistApprox c a) (evalDist c a)) -> rat_inf_limit (fun n : nat => sumList_rel (fun i : nat => expRat_rel (sumList_rel (fun a0 : A => lowDistApprox c a0 n) (filter (fun a0 : A => negb (P a0)) (getSupport c))) i) (getNats O n)) (ratInverse (sumList (filter P (getSupport c)) (evalDist c))).
proof: Proof. intuition. eapply rat_inf_limit_eq. eapply power_series_limit_2. eapply rat_inf_limit_summation. eauto. intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. intuition. eapply lowDistApprox_func; eauto. intuition. destruct H0. assert (sumList (filter (fun a0 : A => negb (P a0)) (getSupport c)) (evalDist c) == 1). eapply leRat_impl_eqRat. eapply leRat_trans. eapply sumList_filter_le. rewrite evalDist_lossless. intuition. trivial. eapply leRat_trans. eapply H3. eapply sumList_rel_le. eapply H2. eapply sumList_rel_sumList. intuition. rewrite <- H6. eapply lowDistApprox_low. eauto. eauto. rewrite <- evalDist_lossless in H4; eauto. rewrite (sumList_filter_partition P (getSupport c)) in H4. symmetry in H4. rewrite ratAdd_comm in H4. apply ratAdd_arg_0 in H4. eapply sumList_0 in H4; eauto. eapply getSupport_In_evalDist. eapply filter_In; eauto. trivial. destruct H0. intuition. eapply sumList_filter_evalDist_le_1; eauto. intuition. eapply sumList_rel_left_total. intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. intuition. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. eapply ratInverse_eqRat_compat. intuition. apply ratSubtract_0_inv in H2. destruct H0. eapply sumList_filter_evalDist_le_1; eauto. eapply (@eqRat_ratAdd_same_r (sumList (filter (fun a => negb (P a)) (getSupport c)) (evalDist c))). rewrite <- sumList_filter_partition. rewrite evalDist_lossless. rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_inverse_2. intuition. eapply leRat_trans. eapply sumList_filter_le. rewrite evalDist_lossless. intuition. trivial. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat