changelog & doc

CHANGELOG_UNRELEASED.md

@@ -34,6 +34,37 @@
 - in `normedtype.v`:
   + lemma `not_near_at_leftP`
 
+- in `lebesgue_measure.v`:
+  + lemma `measurable_fun_ler`
+
+- in `measure.v`:
+  + lemmas `measurable_fun_TF`, `measurable_and`
+
+- in `signed.v`:
+  + lemma `onem_nonneg_proof`, definition `onem_nonneg`
+
+- in `esum.v`:
+  + lemma `nneseries_sum_bigcup`
+
+- in `lebesgue_measurable.v`:
+  + lemmas `measurable_natmul`, `measurable_fun_pow`
+
+- in `probability.v`:
+  + definition `bernoulli_pmf`
+  + lemmas `bernoulli_pmf_ge0`, `bernoulli_pmf1`, `measurable_bernoulli_pmf`
+  + definition  `bernoulli` (equipped with the `probability` structure)
+  + lemmas `bernoulli_dirac`, `bernoulliE`, `integral_bernoulli`, `measurable_bernoulli`,
+    `measurable_bernoulli2`
+  + definition `binomial_pmf`
+  + lemmas `binomial_pmf_ge0`, `measurable_binomial_pmf`
+  + definitions `binomial_prob` (equipped with the `probability` structure), `bin_prob`
+  + lemmas `bin_prob0`, `bin_prob1`, `binomial_msum`, `binomial_probE`, `integral_binomial`,
+    `integral_binomial_prob`, `measurable_binomial_prob`
+  + definition `uniform_pdf`
+  + lemmas `measurable_uniform_pdf`, `integral_uniform_pdf`, `integral_uniform_pdf1`
+  + definition `uniform_prob` (equipped with the `probability` structure)
+  + lemmas `dominates_uniform_prob`, `integral_uniform`
+
 ### Changed
 
 - in `forms.v`:
@@ -110,6 +141,9 @@
 	(from `measurableType` to `semiRingOfSetsType`)
   + lemmas ` measurable_prod_measurableType`, `measurable_prod_g_measurableTypeR` (from `measurableType` to `algebraOfSetsType`)
 
+- in `lebesgue_integral.v`:
+  + lemma `ge0_emeasurable_fun_sum`
+
 ### Deprecated
 
 - in `classical_sets.v`:

theories/esum.v

@@ -451,6 +451,15 @@ End esum_bigcup.
 Arguments esum_bigcupT {R T K} J a.
 Arguments esum_bigcup {R T K} J a.
 
+Lemma nneseries_sum_bigcup {R : realType} (T : choiceType) (F : (set T)^nat)
+    (f : T -> \bar R) : trivIset [set: nat] F -> (forall i, 0 <= f i)%E ->
+  (\esum_(i in \bigcup_n F n) f i = \sum_(0 <= i <oo) (\esum_(j in F i) f j))%E.
+Proof.
+move=> tF f0; rewrite esum_bigcupT// nneseries_esum//; last first.
+  by move=> k _; exact: esum_ge0.
+by rewrite fun_true; apply: eq_esum => /= i _.
+Qed.
+
 Definition summable (T : choiceType) (R : realType) (D : set T)
   (f : T -> \bar R) := (\esum_(x in D) `| f x | < +oo)%E.
 

theories/lebesgue_measure.v

@@ -1686,6 +1686,20 @@ Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed.
 #[global] Hint Extern 0 (measurable_fun _ expR) =>
   solve [apply: measurable_expR] : core.
 
+Lemma measurable_natmul {R : realType} D n :
+  measurable_fun D ((@GRing.natmul R)^~ n).
+Proof.
+under eq_fun do rewrite -mulr_natr.
+by do 2 apply: measurable_funM => //.
+Qed.
+
+Lemma measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f ->
+  measurable_fun D (fun x => f x ^+ n).
+Proof.
+move=> mf.
+exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f).
+Qed.
+
 Lemma measurable_powR (R : realType) p :
   measurable_fun [set: R] (@powR R ^~ p).
 Proof.

theories/probability.v

@@ -15,24 +15,39 @@ Require Import exp numfun lebesgue_measure lebesgue_integral kernel.
 (* the type probability T R (a measure that sums to 1).                       *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*          {RV P >-> R} == real random variable: a measurable function from  *)
-(*                          the measurableType of the probability P to R      *)
-(*      distribution P X == measure image of the probability measure P by the *)
-(*                          random variable X : {RV P -> R}                   *)
-(*                          P as type probability T R with T of type          *)
-(*                          measurableType.                                   *)
-(*                          Declared as an instance of probability measure.   *)
-(*               'E_P[X] == expectation of the real measurable function X     *)
-(*        covariance X Y == covariance between real random variable X and Y   *)
-(*               'V_P[X] == variance of the real random variable X            *)
-(*         mmt_gen_fun X == moment generating function of the random variable *)
-(*                          X *)
-(*       {dmfun T >-> R} == type of discrete real-valued measurable functions *)
-(*         {dRV P >-> R} == real-valued discrete random variable              *)
-(*             dRV_dom X == domain of the discrete random variable X          *)
-(*            dRV_enum X == bijection between the domain and the range of X   *)
-(*               pmf X r := fine (P (X @^-1` [set r]))                        *)
-(*         enum_prob X k == probability of the kth value in the range of X    *)
+(*         {RV P >-> R} == real random variable: a measurable function from   *)
+(*                         the measurableType of the probability P to R       *)
+(*     distribution P X == measure image of the probability measure P by the  *)
+(*                         random variable X : {RV P -> R}                    *)
+(*                         P as type probability T R with T of type           *)
+(*                         measurableType.                                    *)
+(*                         Declared as an instance of probability measure.    *)
+(*              'E_P[X] == expectation of the real measurable function X      *)
+(*       covariance X Y == covariance between real random variable X and Y    *)
+(*              'V_P[X] == variance of the real random variable X             *)
+(*        mmt_gen_fun X == moment generating function of the random variable  *)
+(*                         X                                                  *)
+(*      {dmfun T >-> R} == type of discrete real-valued measurable functions  *)
+(*        {dRV P >-> R} == real-valued discrete random variable               *)
+(*            dRV_dom X == domain of the discrete random variable X           *)
+(*           dRV_enum X == bijection between the domain and the range of X    *)
+(*             pmf X r := fine (P (X @^-1` [set r]))                          *)
+(*        enum_prob X k == probability of the kth value in the range of X     *)
+(* ```                                                                        *)
+(*                                                                            *)
+(* ```                                                                        *)
+(*      bernoulli_pmf p == Bernoulli pmf                                      *)
+(*          bernoulli p == Bernoulli probability measure when 0 <= p <= 1     *)
+(*                         and \d_false otherwise                             *)
+(*     binomial_pmf n p == binomial pmf                                       *)
+(*    binomial_prob n p == binomial probability measure when 0 <= p <= 1      *)
+(*                         and \d_0%N otherwise                               *)
+(*       bin_prob n k p == $\binom{n}{k}p^k (1-p)^(n-k)$                      *)
+(*                         Computes a binomial distribution term for          *)
+(*                         k successes in n trials with success rate p        *)
+(*      uniform_pdf a b == uniform pdf                                        *)
+(*  uniform_prob a b ab == uniform probability over the interval [a,b]        *)
+(*                         with ab0 a proof that 0 < b - a                    *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -829,39 +844,6 @@ Qed.
 
 End discrete_distribution.
 
-(* TODO: move *)
-Lemma onem_nonneg_proof (R : numDomainType) (p : {nonneg R}) :
-  (p%:num <= 1 -> 0 <= `1-(p%:num))%R.
-Proof. by rewrite /onem/= subr_ge0. Qed.
-
-Definition onem_nonneg (R : numDomainType) (p : {nonneg R})
-   (p1 : (p%:num <= 1)%R) :=
-  NngNum (onem_nonneg_proof p1).
-
-Lemma nneseries_sum_bigcup {R : realType} (T : choiceType) (F : (set T)^nat)
-    (f : T -> \bar R) : trivIset [set: nat] F -> (forall i, 0 <= f i)%E ->
-  (\esum_(i in \bigcup_n F n) f i = \sum_(0 <= i <oo) (\esum_(j in F i) f j))%E.
-Proof.
-move=> tF f0; rewrite esum_bigcupT// nneseries_esum//; last first.
-  by move=> k _; exact: esum_ge0.
-by rewrite fun_true; apply: eq_esum => /= i _.
-Qed.
-
-Lemma measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f ->
-  measurable_fun D (fun x => f x ^+ n).
-Proof.
-move=> mf.
-apply: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f) => //.
-Qed.
-
-Lemma measurable_natmul {R : realType} D n :
-  measurable_fun D ((@GRing.natmul R)^~ n).
-Proof.
-under eq_fun do rewrite -mulr_natr.
-by do 2 apply: measurable_funM => //.
-Qed.
-(* /TODO: move *)
-
 Section bernoulli_pmf.
 Context {R : realType} (p : R).
 Local Open Scope ring_scope.

theories/signed.v

@@ -1225,4 +1225,10 @@ Lemma onemX_NngNum r (r1 : r <= 1) (r0 : 0 <= r) n :
   `1-(r ^+ n) = (NngNum (onemX_ge0 n r0 r1))%:num.
 Proof. by []. Qed.
 
+Lemma onem_nonneg_proof (p : {nonneg R}) : p%:num <= 1 -> 0 <= `1-(p%:num).
+Proof. by rewrite /onem/= subr_ge0. Qed.
+
+Definition onem_nonneg (p : {nonneg R}) (p1 : p%:num <= 1) :=
+  NngNum (onem_nonneg_proof p1).
+
 End onem_signed.