minor fixes and additions (#1499)

* fixes #1497

* fixes #1498

* minor additions coming from the sampling branch

---------

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>
Co-authored-by: Alessandro Bruni <brun@itu.dk>

CHANGELOG_UNRELEASED.md

@@ -9,6 +9,16 @@
 
 - new file `internal_Eqdep_dec.v` (don't use, internal, to be removed)
 
+- file `constructive_ereal.v`:
+  + definition `iter_mule`
+  + lemma `prodEFin`
+
+- file `exp.v`:
+  + lemma `expR_sum`
+
+- file `lebesgue_integral.v`:
+  + lemma `measurable_fun_le`
+
 ### Changed
 
 - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package

reals/constructive_ereal.v

@@ -796,6 +796,10 @@ Lemma EFinB r r' : (r - r')%:E = r%:E - r'%:E. Proof. by []. Qed.
 
 Lemma EFinM r r' : (r * r')%:E = r%:E * r'%:E. Proof. by []. Qed.
 
+Lemma prodEFin T s (P : pred T) (f : T -> R) :
+  \prod_(i <- s | P i) (f i)%:E = (\prod_(i <- s | P i) f i)%:E.
+Proof. by elim/big_ind2 : _ => // _ x _ y -> ->; rewrite EFinM. Qed.
+
 Lemma sumEFin I s P (F : I -> R) :
   \sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E.
 Proof. by rewrite (big_morph _ EFinD erefl). Qed.
@@ -2272,7 +2276,8 @@ case: z z0 => [z z0| |//]; last by rewrite !gt0_muley ?mule_gt0.
 by rewrite /mule/= mulrA.
 Qed.
 
-Local Open Scope ereal_scope.
+Lemma iter_mule n x y : iter n ( *%E x) y = x ^+ n * y.
+Proof. by elim: n => [|n ih]; rewrite ?mul1e// [LHS]/= ih expeS muleA. Qed.
 
 HB.instance Definition _ := Monoid.isComLaw.Build (\bar R) 1%E mule
   muleA muleC mul1e.
@@ -4273,7 +4278,6 @@ Qed.
 Section contract_expand.
 Variable R : realFieldType.
 Implicit Types (x : \bar R) (r : R).
-Local Open Scope ereal_scope.
 
 Definition contract x : R :=
   match x with

theories/exp.v

@@ -415,6 +415,10 @@ rewrite expRxDyMexpx expRN [_ * expR y]mulrC mulfK //.
 by case: ltrgt0P (expR_gt0 x).
 Qed.
 
+Lemma expR_sum T s (P : pred T) (f : T -> R) :
+  expR (\sum_(i <- s | P i) f i) = \prod_(i <- s | P i) expR (f i).
+Proof. by elim/big_ind2 : _ => [|? ? ? ? <- <-|]; rewrite ?expR0// expRD. Qed.
+
 Lemma expRM_natl n x : expR (n%:R * x) = expR x ^+ n.
 Proof.
 elim: n x => [x|n IH x] /=; first by rewrite mul0r expr0 expR0.

theories/lebesgue_integral.v

@@ -239,14 +239,15 @@ HB.instance Definition _ :=
 End mfun_realType.
 
 Section mfun_measurableType.
-Context {d d'} {aT : measurableType d} {rT : measurableType d'}.
+Context {d1} {T1 : measurableType d1} {d2} {T2 : measurableType d2}
+  {d3} {T3 : measurableType d3}.
+Variables (f : {mfun T2 >-> T3}) (g : {mfun T1 >-> T2}).
 
-Lemma measurableT_comp_subproof (f : {mfun _ >-> rT}) (g : {mfun aT >-> rT}) :
-  measurable_fun setT (f \o g).
+Lemma measurableT_comp_subproof : measurable_fun setT (f \o g).
 Proof. exact: measurableT_comp. Qed.
 
-HB.instance Definition _ (f : {mfun _ >-> rT}) (g : {mfun aT >-> rT}) :=
-  isMeasurableFun.Build _ _ _ _ (f \o g) (measurableT_comp_subproof _ _).
+HB.instance Definition _ := isMeasurableFun.Build _ _ _ _ (f \o g)
+  measurableT_comp_subproof.
 
 End mfun_measurableType.
 
@@ -2045,25 +2046,9 @@ Notation emeasurable_fun_fsum := emeasurable_fsum (only parsing).
 #[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `ge0_emeasurable_sum`")]
 Notation ge0_emeasurable_fun_sum := ge0_emeasurable_sum (only parsing).
 
-Section measurable_fun.
-Context d (T : measurableType d) (R : realType).
-Implicit Types (D : set T) (f g : T -> R).
-
-Lemma measurable_sum D I s (h : I -> (T -> R)) :
-  (forall n, measurable_fun D (h n)) ->
-  measurable_fun D (fun x => \sum_(i <- s) h i x).
-Proof.
-move=> mh; apply/measurable_EFinP.
-rewrite (_ : _ \o _ = (fun t => \sum_(i <- s) (h i t)%:E)); last first.
-  by apply/funext => t/=; rewrite -sumEFin.
-by apply/emeasurable_sum => i; exact/measurable_EFinP.
-Qed.
-
-End measurable_fun.
-
-Section measurable_fun_measurable2.
+Section emeasurable_fun_cmp.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
+Context d {T : measurableType d} {R : realType}.
 Variables (D : set T) (mD : measurable D).
 Implicit Types f g : T -> \bar R.
 
@@ -2095,7 +2080,31 @@ move=> mf mg; rewrite set_neq_lt setIUr.
 by apply: measurableU; exact: emeasurable_fun_lt.
 Qed.
 
-End measurable_fun_measurable2.
+End emeasurable_fun_cmp.
+
+Section measurable_fun.
+Context d (T : measurableType d) (R : realType).
+Implicit Types (D : set T) (f g : T -> R).
+
+Lemma measurable_sum D I s (h : I -> (T -> R)) :
+  (forall n, measurable_fun D (h n)) ->
+  measurable_fun D (fun x => \sum_(i <- s) h i x).
+Proof.
+move=> mh; apply/measurable_EFinP.
+rewrite (_ : _ \o _ = (fun t => \sum_(i <- s) (h i t)%:E)); last first.
+  by apply/funext => t/=; rewrite -sumEFin.
+by apply/emeasurable_sum => i; exact/measurable_EFinP.
+Qed.
+
+Lemma measurable_fun_le D f g :
+  d.-measurable D -> measurable_fun D f -> measurable_fun D g ->
+  measurable (D `&` [set x | f x <= g x]).
+Proof.
+move=> mD mf mg; under eq_set => x do rewrite -lee_fin.
+by apply: emeasurable_fun_le => //; exact: measurableT_comp.
+Qed.
+
+End measurable_fun.
 
 Section ge0_integral_sum.
 Local Open Scope ereal_scope.

theories/probability.v

@@ -39,18 +39,21 @@ From mathcomp Require Import ftc gauss_integral.
 (* ```                                                                        *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*      bernoulli_pmf p == Bernoulli pmf                                      *)
+(*      bernoulli_pmf p == Bernoulli pmf with parameter p : R                 *)
 (*          bernoulli p == Bernoulli probability measure when 0 <= p <= 1     *)
 (*                         and \d_false otherwise                             *)
-(*     binomial_pmf n p == binomial pmf                                       *)
+(*     binomial_pmf n p == binomial pmf with parameters n : nat and p : R     *)
 (*    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_pdf a b == uniform pdf over the interval [a,b]                *)
 (*  uniform_prob a b ab == uniform probability over the interval [a,b]        *)
-(*                         with ab0 a proof that 0 < b - a                    *)
+(*                         where ab0 a proof that 0 < b - a                   *)
+(*       normal_pdf m s == pdf of the normal distribution with mean m and     *)
+(*                         standard deviation s                               *)
+(*      normal_prob m s == normal probability measure                         *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)