From 9f65d6f47ca0b9e77bfbed1854868aa2c7847747 Mon Sep 17 00:00:00 2001
From: Alessandro Bruni <brun@itu.dk>
Date: Thu, 26 Oct 2023 23:19:00 +0200
Subject: [PATCH] wip

---
 theories/probability.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/probability.v b/theories/probability.v
index 8f4e84581..3fef4b1a3 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -1370,8 +1370,8 @@ End uniform_probability.
 
 (* TODO: formalize https://math.uchicago.edu/~may/REU2019/REUPapers/Rajani.pdf *)
 Theorem sampling p (X : {RV P >-> R}^nat) (n : nat) (theta delta : R) :
-  let X_sum x := \sum_(i < n) (X i x) in
-  let X' := X_sum / n%:R in
+  let X_sum x := \sum_(i < n) (X i x)%:E in
+  let X' x := X_sum x * (n%:R)^-1%:E in
   (forall i, bernoulli p (X i)) ->
-  n > 3 / (theta ^+ 2) * ln (2 / delta) ->
-  P [set i | `| X' i - p | < theta] >= 1 - delta.
+  (n%:R > 3 / (theta ^+ 2) * ln (2 / delta))%R ->
+  P [set i | `| X' i - p%:E | < theta%:E] >= 1 - delta%:E.