bernoulli probability measure

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,13 @@
 
 ### Added
 
+- in `signed.v`:
+  + definition `onem_NngNum`
+- in `measure.v`:
+  + definition `bernoulli`, declared as a probability measure instance
+- in `itv.v`:
+  + canonical `onem_itv01`
+
 ### Changed
 
 ### Renamed

theories/itv.v

@@ -843,6 +843,9 @@ Lemma inum_lt : {mono inum : x y / (x < y)%O}. Proof. by []. Qed.
 
 End Morph.
 
+Canonical onem_itv01 {R : realDomainType} (p : {i01 R}) : {i01 R} :=
+  @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
+
 Section Test1.
 
 Variable R : numDomainType.
@@ -882,8 +885,6 @@ apply/val_inj => /=.
 by rewrite subr0 mulr1 opprB addrCA subrr addr0.
 Qed.
 
-Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
-  @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
 
 Definition s_of_pq' (p q : {i01 R}) : {i01 R} :=
   (`1- (`1-(p%:inum) * `1-(q%:inum)))%:i01.

theories/measure.v

@@ -3,6 +3,7 @@ From mathcomp Require Import all_ssreflect all_algebra finmap.
 From mathcomp.classical Require Import boolp classical_sets functions.
 From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
 Require Import reals ereal signed topology normedtype sequences esum numfun.
+Require Import itv.
 From HB Require Import structures.
 
 (******************************************************************************)
@@ -137,6 +138,8 @@ From HB Require Import structures.
 (*     probability T R == probability measure over the measurableType T with  *)
 (*                        value in R : realType                               *)
 (*     Measure_isProbability == factor for probability measures               *)
+(*     bernoulli p1 == the p-Bernoulli probability where p1 is a proof that   *)
+(*                     p : {nonneg R} is <= 1                                 *)
 (*                                                                            *)
 (*   mu.-negligible A == A is mu negligible                                   *)
 (*   {ae mu, forall x, P x} == P holds almost everywhere for the measure mu,  *)
@@ -2826,6 +2829,26 @@ HB.instance Definition _ x :=
 
 End pdirac.
 
+Section bernoulli.
+Variables (R : realType) (p : {i01 R}).
+
+Definition bernoulli : set _ -> \bar R := measure_add
+  (mscale (NngNum (itv_ge0 p)) (dirac true))
+  (mscale (NngNum (itv_ge0 ((`1-(p%:inum))%:i01))) (dirac false)).
+
+HB.instance Definition _ := Measure.on bernoulli.
+
+Let bernoulli_setT : bernoulli [set: _] = 1.
+Proof.
+rewrite /bernoulli/= /measure_add/= /msum 2!big_ord_recr/= big_ord0 add0e/=.
+by rewrite /mscale/= !diracT !mule1 -EFinD add_onemK.
+Qed.
+
+HB.instance Definition _ :=
+  @Measure_isProbability.Build _ _ R bernoulli bernoulli_setT.
+
+End bernoulli.
+
 Lemma sigma_finite_counting (R : realType) :
   sigma_finite [set: nat] (@counting _ R).
 Proof.

theories/signed.v

@@ -106,6 +106,9 @@ From mathcomp.classical Require Import mathcomp_extra.
 (* --> Canonical instances are also provided according to types, as a         *)
 (* fallback when no known operator appears in the expression. Look to         *)
 (* nat_snum below for an example on how to add your favorite type.            *)
+(*                                                                            *)
+(*   onem_NngNum p1 == where p1 is a proof that p : {nonneg R} is <= 1 is the *)
+(*                     the number `1-p with type {nonneg R}                   *)
 (******************************************************************************)
 
 Reserved Notation "{ 'compare' x0 & nz & cond }"
@@ -1182,4 +1185,7 @@ Lemma onemX_NngNum r (r1 : r <= 1) (r0 : 0 <= r) n :
   `1-(r ^+ n) = (NngNum (onemX_ge0 n r0 r1))%:num.
 Proof. by []. Qed.
 
+Definition onem_NngNum (p : {nonneg R}) (p1 : (p%:num <= 1)%R) :=
+  NngNum (onem_ge0 p1).
+
 End onem_signed.