From bdc11d7bfa29e3d9d60efb29f6bc6d266e4f84ff Mon Sep 17 00:00:00 2001
From: Alessandro Bruni <brun@itu.dk>
Date: Thu, 26 Oct 2023 16:31:38 +0200
Subject: [PATCH] sampling_lemma

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

diff --git a/theories/probability.v b/theories/probability.v
index a5987066f..6bcde9663 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -1368,3 +1368,11 @@ apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=.
 Qed.
 
 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
+  (forall i, bernoulli p (X i)) ->
+  n > 3 / (theta ^+ 2) * ln (2 / delta) ->
+  P [set i | `| X' i - p | < theta] >= 1 - delta.