From a32c4d2f17e84b5405df180551458a3719cb9036 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 29 Nov 2024 13:44:29 +0100 Subject: [PATCH] laplace distribution --- theories/prelude/Coquelicot_ext.v | 7 +++++++ theories/prob/distribution.v | 16 +++++++++++++--- 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/theories/prelude/Coquelicot_ext.v b/theories/prelude/Coquelicot_ext.v index 9634b050..7ac3b70f 100644 --- a/theories/prelude/Coquelicot_ext.v +++ b/theories/prelude/Coquelicot_ext.v @@ -448,3 +448,10 @@ Qed. Proof. intros ?? ?; eapply Series_ext; eauto. Qed. + +Lemma exp_pow x n: (exp x)^n = exp (x * INR n). +Proof. + induction n. + - by rewrite Rmult_0_r exp_0/=. + - rewrite S_INR/=Rmult_plus_distr_l exp_plus IHn. rewrite Rmult_1_r. lra. +Qed. diff --git a/theories/prob/distribution.v b/theories/prob/distribution.v index e129aef6..a45e4fcb 100644 --- a/theories/prob/distribution.v +++ b/theories/prob/distribution.v @@ -2319,8 +2319,8 @@ Section uniform_fin_lists. End uniform_fin_lists. Section laplace. - Definition laplace_f_nat (ε:nonnegreal) (n:nat) := exp (- INR n * ε). - Definition laplace_f (ε:nonnegreal) (z:Z) := laplace_f_nat ε (Z.to_nat (Z.abs z)). + Definition laplace_f_nat (ε:posreal) (n:nat) := exp (- INR n * ε). + Definition laplace_f (ε:posreal) (z:Z) := laplace_f_nat ε (Z.to_nat (Z.abs z)). Lemma laplace_f_nat_pos ε n: 0<=laplace_f_nat ε n. Proof. @@ -2329,7 +2329,17 @@ Section laplace. Lemma ex_seriesC_laplace_f_nat ε: ex_seriesC (λ n, laplace_f_nat ε n). Proof. - Admitted. + rewrite /laplace_f_nat. eapply (ex_seriesC_ext (λ n, (exp (-ε)) ^ n)). + - intros. + rewrite exp_pow. f_equal. lra. + - rewrite -ex_seriesC_nat. apply ex_series_geom. + apply Rabs_def1. + + rewrite exp_Ropp. + rewrite -Rdiv_1_l. rewrite -Rdiv_lt_1; last apply exp_pos. + replace 1 with (exp 0); last apply exp_0. + apply exp_increasing. apply cond_pos. + + trans 0; [lra|apply exp_pos]. + Qed. Lemma ex_seriesC_laplace_f ε: ex_seriesC (λ z, laplace_f ε z). Proof.