From 9cf66fc3d87239ba6a73c2d65fdeb27dbd696b9e Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 29 Nov 2024 14:06:10 +0100 Subject: [PATCH] Full laplace --- theories/prob/distribution.v | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/theories/prob/distribution.v b/theories/prob/distribution.v index 65d9de4c..af1fbbb5 100644 --- a/theories/prob/distribution.v +++ b/theories/prob/distribution.v @@ -2402,7 +2402,7 @@ Section laplace. * apply ex_seriesC_scal_l, ex_seriesC_laplace_f_nat. Qed. - Program Definition laplace ε : distr (Z) := + Program Definition laplace' ε : distr (Z) := MkDistr (λ z, laplace_f ε z / SeriesC (λ z, laplace_f ε z)) _ _ _. Next Obligation. intros. rewrite /laplace_f. @@ -2428,7 +2428,32 @@ Section laplace. - apply exp_pos. - intros; left. apply exp_pos. - apply ex_seriesC_laplace_f. - Qed. + Qed. + + Program Definition laplace ε m :distr (Z) := + MkDistr (λ z, laplace' ε (z-m)%Z) _ _ _. + Next Obligation. + simpl; intros. + apply pmf_pos. + Qed. + Next Obligation. + intros. + pose (h:= (λ '(z1, z2), if bool_decide (z2 -z1 = m)%Z then laplace' ε z1 else 0)). + apply (ex_seriesC_ext (λ z2, SeriesC (λ z1, h (z1, z2)))). + { rewrite /h. + intros z2. + erewrite SeriesC_ext; first apply SeriesC_singleton_dependent. + simpl. intros; repeat case_bool_decide; try done; lia. + } + apply fubini_pos_seriesC_ex_double; rewrite /h. + - intros. case_bool_decide; [apply pmf_pos|done]. + - intros. eapply ex_seriesC_ext; last apply (ex_seriesC_singleton (m+a)%Z). + intros. simpl. repeat case_bool_decide; try lia; done. + - eapply ex_seriesC_ext; last apply (pmf_ex_seriesC (laplace' ε)). + intros n. + erewrite SeriesC_ext; first by erewrite (SeriesC_singleton (n+m)%Z). + intros. simpl. repeat case_bool_decide; try lia; done. + Qed. End laplace. Ltac inv_distr :=