generic lemmas from the prob_lang PR

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,24 @@
 
 ### Added
 
+- in `probability.v`:
+  + lemmas `eq_bernoulli`, `eq_bernoulliV2`
+
+- in `measure.v`:
+  + lemmas `mnormalize_id`, `measurable_fun_eqP`
+
+- in `ftc.v`:
+  + lemma `integrable_locally`
+
+- in `constructive_ereal.v`:
+  + lemma `EFin_bigmax`
+
+- in `mathcomp_extra.v`:
+  + lemmas `inr_inj`, `inl_inj`
+
+- in `classical_sets.v`:
+  + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f`
+
 ### Changed
 
 ### Renamed

classical/classical_sets.v

@@ -555,6 +555,7 @@ Qed.
 Notation setTP := setTPn (only parsing).
 
 Lemma in_set0 (x : T) : (x \in set0) = false. Proof. by rewrite memNset. Qed.
+
 Lemma in_setT (x : T) : x \in setT. Proof. by rewrite mem_set. Qed.
 
 Lemma in_setC (x : T) A : (x \in ~` A) = (x \notin A).
@@ -1441,9 +1442,15 @@ Implicit Types (A B : set aT) (f : aT -> rT) (Y : set rT).
 
 Lemma imageP f A a : A a -> (f @` A) (f a). Proof. by exists a. Qed.
 
+Lemma image_f f A a : a \in A -> f a \in [set f x | x in A].
+Proof. by rewrite !inE; apply/imageP. Qed.
+
 Lemma imageT (f : aT -> rT) (a : aT) : range f (f a).
 Proof. by apply: imageP. Qed.
 
+Lemma mem_range f a : f a \in range f.
+Proof. by rewrite !inE; apply/imageT. Qed.
+
 End base_image_lemmas.
 #[global]
 Hint Extern 0 ((?f @` _) (?f _)) =>  solve [apply: imageP; assumption] : core.
@@ -1458,6 +1465,10 @@ Proof.
 by move=> f_inj; rewrite propeqE; split => [[b Ab /f_inj <-]|/(imageP f)//].
 Qed.
 
+Lemma mem_image {f A a} : injective f ->
+   (f a \in [set f x | x in A]) = (a \in A).
+Proof. by move=> /image_inj finj; apply/idP/idP; rewrite !inE finj. Qed.
+
 Lemma image_id A : id @` A = A.
 Proof. by rewrite eqEsubset; split => a; [case=> /= x Ax <-|exists a]. Qed.
 
@@ -1732,6 +1743,15 @@ Proof.
 by apply/disj_setPS/disj_setPS; rewrite -some_setI -some_set0 sub_image_someP.
 Qed.
 
+
+Lemma inl_in_set_inr A B (x : A) (Y : set B) :
+  inl x \in [set inr y | y in Y] = false.
+Proof. by apply/negP; rewrite inE/= => -[]. Qed.
+
+Lemma inr_in_set_inr A B (y : B) (Y : set B) :
+  inr y \in [set @inr A B y | y in Y] = (y \in Y).
+Proof. by apply/idP/idP => [/[!inE][/= [x ? [<-]]]|/[!inE]]//; exists y. Qed.
+
 Section bigop_lemmas.
 Context {T I : Type}.
 Implicit Types (A : set T) (i : I) (P : set I) (F G : I -> set T).
@@ -2219,6 +2239,9 @@ Proof. by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_seq. Qed.
 
 End bigcup_seq.
 
+Lemma in_set1 [T : finType] (x y : T) : (x \in [set y]) = (x \in [set y]%SET).
+Proof. by apply/idP/idP; rewrite !inE /= => /eqP. Qed.
+
 Lemma bigcup_pred [T : finType] [U : Type] (P : {pred T}) (f : T -> set U) :
   \bigcup_(t in [set` P]) f t = \big[setU/set0]_(t in P) f t.
 Proof.

classical/mathcomp_extra.v

@@ -464,3 +464,9 @@ End trunc_floor_ceil.
 
 Lemma natr_int {R : archiNumDomainType} n : n%:R \is a @Num.int R.
 Proof. by rewrite Num.Theory.intrEge0. Qed.
+
+Lemma inr_inj {A B} : injective (@inr A B).
+Proof. by move=>  ? ? []. Qed.
+
+Lemma inl_inj {A B} : injective (@inl A B).
+Proof. by move=>  ? ? []. Qed.

reals/constructive_ereal.v

@@ -2509,6 +2509,11 @@ by move=> [x| |] [y| |]//= _ _; apply/esym; have [ab|ba] := leP x y;
   [apply/max_idPr; rewrite lee_fin|apply/max_idPl; rewrite lee_fin ltW].
 Qed.
 
+Lemma EFin_bigmax  {I : Type} (s : seq I) (P : I -> bool) (F : I -> R) r :
+  \big[maxe/r%:E]_(i <- s | P i) (F i)%:E =
+  (\big[Num.max/r]_(i <- s | P i) F i)%:E.
+Proof. by rewrite (big_morph _ EFin_max erefl). Qed.
+
 Lemma fine_min :
   {in fin_num &, {mono @fine R : x y / mine x y >-> (Num.min x y)%:E}}.
 Proof.

theories/ftc.v

@@ -65,6 +65,24 @@ Notation mu := (@lebesgue_measure R).
 Local Open Scope ereal_scope.
 Implicit Types (f : R -> R) (a : itv_bound R).
 
+Lemma integrable_locally f (A : set R) : measurable A ->
+  mu.-integrable A (EFin \o f) -> locally_integrable [set: R] (f \_ A).
+Proof.
+move=> mA intf; split.
+- move/integrableP : intf => [mf _].
+  by apply/(measurable_restrictT _ _).1 => //; exact/EFin_measurable_fun.
+- exact: openT.
+- move=> K _ cK.
+  move/integrableP : intf => [mf].
+  rewrite integral_mkcond/=.
+  under eq_integral do rewrite restrict_EFin restrict_normr.
+  apply: le_lt_trans.
+  apply: ge0_subset_integral => //=; first exact: compact_measurable.
+  apply/EFin_measurable_fun/measurableT_comp/EFin_measurable_fun => //=.
+  move/(measurable_restrictT _ _).1 : mf => /=.
+  by rewrite restrict_EFin; exact.
+Qed.
+
 Let FTC0 f a : mu.-integrable setT (EFin \o f) ->
   let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in
   forall x, a < BRight x -> lebesgue_pt f x ->

theories/kernel.v

@@ -1577,14 +1577,14 @@ Definition mkproduct :=
 
 End kproduct_measure.
 
-(* [Theorem 14.22, Klenke 2014] (3/3): the composition of finite transition
-  kernels is sigma-finite *)
 HB.instance Definition _ d0 d1 d2 (T0 : measurableType d0)
     (T1 : measurableType d1) (T2 : measurableType d2) {R : realType}
     (k1 : R.-ftker T0 ~> T1) (k2 : R.-ftker (T0 * T1) ~> T2) :=
   @isKernel.Build _ _ T0 (T1 * T2)%type R
     (mkproduct k1 k2) (measurable_kproduct k1 k2).
 
+(* [Theorem 14.22, Klenke 2014] (3/3): the composition of finite transition
+  kernels is sigma-finite *)
 Section sigma_finite_kproduct.
 Context d0 d1 d2 (T0 : measurableType d0)
   (T1 : measurableType d1) (T2 : measurableType d2) {R : realType}

theories/measure.v

@@ -1516,6 +1516,12 @@ by move=> fg mf mD A mA; rewrite [X in measurable X](_ : _ = D `&` f @^-1` A);
   [exact: mf|exact/esym/eq_preimage].
 Qed.
 
+Lemma measurable_fun_eqP D (f g : T1 -> T2) :
+  {in D, f =1 g} -> measurable_fun D f <-> measurable_fun D g.
+Proof.
+by move=> eq_fg; split; apply/eq_measurable_fun => // ? ?; rewrite eq_fg.
+Qed.
+
 Lemma measurable_cst D (r : T2) : measurable_fun D (cst r : T1 -> _).
 Proof.
 by move=> mD /= Y mY; rewrite preimage_cst; case: ifPn; rewrite ?setIT ?setI0.
@@ -1582,6 +1588,7 @@ End measurable_fun.
 #[global] Hint Extern 0 (measurable_fun _ id) =>
   solve [apply: measurable_id] : core.
 Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}.
+Arguments measurable_fun_eqP {d1 d2 T1 T2 D} f {g}.
 #[deprecated(since="mathcomp-analysis 0.6.2", note="renamed `eq_measurable_fun`")]
 Notation measurable_fun_ext := eq_measurable_fun (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_id`")]
@@ -3647,6 +3654,13 @@ HB.instance Definition _ :=
 
 End mnormalize.
 
+Lemma mnormalize_id d (T : measurableType d) (R : realType)
+  (P P' : probability T R) : mnormalize P P' = P.
+Proof.
+apply/funext => x; rewrite /mnormalize/= probability_setT.
+by rewrite onee_eq0/= invr1 mule1.
+Qed.
+
 Section pdirac.
 Context d (T : measurableType d) (R : realType).
 

theories/probability.v

@@ -1047,6 +1047,23 @@ Qed.
 HB.instance Definition _ :=
   @Measure_isProbability.Build _ _ R bernoulli bernoulli_setT.
 
+Lemma eq_bernoulli (P : probability bool R) :
+  P [set true] = p%:E -> P =1 bernoulli.
+Proof.
+move=> Ptrue sb; rewrite /bernoulli /bernoulli_pmf.
+have Pfalse: P [set false] = (1 - p%:E)%E.
+  rewrite -Ptrue -(@probability_setT _ _ _ P) setT_bool measureU//; last first.
+    by rewrite disjoints_subset => -[]//.
+  by rewrite addeAC subee ?add0e//= Ptrue.
+have: (0 <= p%:E <= 1)%E by rewrite -Ptrue measure_ge0 probability_le1.
+rewrite !lee_fin => ->.
+have eq_sb := etrans (bigcup_imset1 (_ : set bool) id) (image_id _).
+rewrite -[in LHS](eq_sb sb)/= measure_fin_bigcup//; last 2 first.
+- exact: finite_finset.
+- by move=> [] [] _ _ [[]]//= [].
+- by apply: eq_fsbigr => /= -[].
+Qed.
+
 End bernoulli.
 
 Section bernoulli_measure.
@@ -1076,6 +1093,17 @@ Qed.
 End bernoulli_measure.
 Arguments bernoulli {R}.
 
+Lemma eq_bernoulliV2 {R : realType} (P : probability bool R) :
+  P [set true] = P [set false] -> P =1 bernoulli 2^-1.
+Proof.
+move=> Ptrue_eq_false; apply/eq_bernoulli.
+have : P [set: bool] = 1%E := probability_setT.
+rewrite setT_bool measureU//=; last first.
+  by rewrite disjoints_subset => -[]//.
+rewrite Ptrue_eq_false -mule2n; move/esym/eqP.
+by rewrite -mule_natl -eqe_pdivrMl// mule1 => /eqP<-.
+Qed.
+
 Section integral_bernoulli.
 Context {R : realType}.
 Variables (p : R) (p01 : (0 <= p <= 1)%R).