probability_fin can be avoided

math-comp · Dec 27, 2024 · df06613 · df06613
1 parent a0ae2cb
commit df06613
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 19 deletions.
diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v
@@ -118,7 +118,7 @@ apply/continuous_within_itvP => //; split.
   rewrite inE/=.
   apply: subset_itv_oo_cc.
   near: z.
-  exact: near_in_itv.
+  exact: near_in_itvoo.
 - rewrite (_:uni 0 = 1%R); last first.
     rewrite /uni indic_restrict patchE ifT//.
     by rewrite inE/= boundl_in_itv bnd_simp/=.
@@ -992,7 +992,7 @@ Proof. by rewrite -[LHS]fineK ?betafunEFin_fin_num. Qed.
 Lemma integrable_XMonemX01 a b : mu.-integrable setT (EFin \o XMonemX01 a b).
 Proof.
 apply/integrableP; split.
-  by apply/EFin_measurable_fun; exact: measurable_XMonemX01.
+  by apply/measurable_EFinP; exact: measurable_XMonemX01.
 under eq_integral.
   move=> /= x _.
   rewrite ger0_norm//; last by rewrite XMonemX01_ge0.
@@ -1035,7 +1035,7 @@ rewrite /beta_pdf.
 under eq_integral do rewrite EFinM.
 rewrite /=.
 rewrite ge0_integralZr//=; last 3 first.
-  apply: measurable_funTS => /=; apply/EFin_measurable_fun => //.
+  apply: measurable_funTS => /=; apply/measurable_EFinP => //.
   exact: measurable_XMonemX01.
   by move=> x _; rewrite lee_fin XMonemX01_ge0.
   by rewrite lee_fin invr_ge0// betafun_ge0.
@@ -1048,7 +1048,7 @@ Qed.
 Lemma integrable_beta_pdf : mu.-integrable setT (EFin \o beta_pdf).
 Proof.
 apply/integrableP; split.
-  by apply/EFin_measurable_fun; exact: measurable_beta_pdf.
+  by apply/measurable_EFinP; exact: measurable_beta_pdf.
 under eq_integral.
   move=> /= x _.
   rewrite ger0_norm//; last by rewrite beta_pdf_ge0.
@@ -1057,7 +1057,7 @@ rewrite -int_beta_pdf01.
 apply: (@le_lt_trans _ _ (\int[mu]_(x in `[0%R, 1%R]) (betafun a b)^-1%:E)%E).
   apply: ge0_le_integral => //=.
   - by move=> x _; rewrite lee_fin beta_pdf_ge0.
-  - by apply/measurable_funTS/EFin_measurable_fun => /=; exact: measurable_beta_pdf.
+  - by apply/measurable_funTS/measurable_EFinP => /=; exact: measurable_beta_pdf.
   - by move=> x _; rewrite lee_fin invr_ge0// betafun_ge0.
   - by move=> x _; rewrite lee_fin beta_pdf_le_betafunV.
 rewrite integral_cst//= lebesgue_measure_itv//=.
@@ -1163,7 +1163,7 @@ rewrite /beta_prob/= /mscale/= /beta_num lte_mul_pinfty//.
   by rewrite lee_fin// invr_ge0 betafun_ge0.
 apply: (@le_lt_trans _ _ (betafunEFin a b)).
   apply: ge0_subset_integral => //=.
-    by apply/EFin_measurable_fun; exact: measurable_XMonemX01.
+    by apply/measurable_EFinP; exact: measurable_XMonemX01.
   by move=> x _; rewrite lee_fin XMonemX01_ge0.
 by rewrite betafunEFin_lty.
 Qed.
@@ -1460,7 +1460,7 @@ congr (_ + _).
       \int[mu]_(x in `[0%R, 1%R]) (XMonemX01 (a + c) (b + d) x)%:E : \bar R)%E.
     rewrite -integralZl//=; last first.
       apply/integrableP; split.
-        apply/EFin_measurable_fun/measurable_funTS.
+        apply/measurable_EFinP/measurable_funTS.
         exact: measurable_XMonemX01.
       under eq_integral.
         move=> x x01.

diff --git a/theories/measure.v b/theories/measure.v
@@ -3518,12 +3518,6 @@ move=> mA; rewrite -(@probability_setT _ _ _ P).
 by apply: le_measure => //; rewrite ?in_setE.
 Qed.
 
-Lemma probability_fin (A : set T) : measurable A -> P A \is a fin_num.
-Proof.
-move=> Ameas; rewrite ge0_fin_numE//.
-by rewrite (@le_lt_trans _ _ 1)// ?measure_ge0 ?probability_le1// ?ltey.
-Qed.
-
 Lemma probability_setC (A : set T) : measurable A -> P (~` A) = 1 - P A.
 Proof.
 move=> mA.

diff --git a/theories/prob_lang.v b/theories/prob_lang.v
@@ -343,7 +343,7 @@ rewrite (_ : (fun x => _) = (fun x => x *
     (\1_(`[i%:R%:E, i.+1%:R%:E [%classic : set _) x)%:E)); last first.
   apply/funext => x; case: ifPn => ix; first by rewrite indicE/= mem_set ?mule1.
   by rewrite indicE/= memNset ?mule0// /= in_itv/=; exact/negP.
-apply: emeasurable_funM => //=; apply/EFin_measurable_fun.
+apply: emeasurable_funM => //=; apply/measurable_EFinP.
 by rewrite (_ : \1__ = mindic R (emeasurable_itv `[i%:R%:E, i.+1%:R%:E[)).
 Qed.
 
@@ -1425,14 +1425,14 @@ Let q : R := p * (1 - p).
 Let r : R := p ^+ 2 + (1 - p) ^+ 2.
 
 Let Dtrue : D [set true] = p%:E.
-Proof. by rewrite fineK//= probability_fin. Qed.
+Proof. by rewrite fineK//= fin_num_measure. Qed.
 
 Let Dfalse : D [set false] = 1 - (p%:E).
 Proof.
 rewrite -Dtrue; have <- : D [set: bool] = 1 := probability_setT.
 rewrite setT_bool measureU//=; last first.
   by rewrite disjoints_subset => -[]//.
-by rewrite addeAC subee ?probability_fin ?add0e.
+by rewrite addeAC subee ?fin_num_measure ?add0e.
 Qed.
 
 Let p_ge0 : (0 <= p)%R.
@@ -1540,7 +1540,7 @@ by rewrite sumgE ltey.
 Unshelve. all: end_near. Qed.
 
 Lemma von_neumann_trick_prob_kernelT gamma :
-   von_neumann_trick gamma [set: bool] = 1.
+  von_neumann_trick gamma [set: bool] = 1.
 Proof.
 rewrite setT_bool measureU//=; last first.
   by rewrite disjoints_subset => -[].
@@ -1712,7 +1712,7 @@ rewrite (sfinite_Fubini
   [the {sfinite_measure set X -> \bar R} of T z]
   [the {sfinite_measure set Y -> \bar R} of U z]
   (fun x => \d_(x.1, x.2) A ))//; last first.
-  apply/EFin_measurable_fun => /=; rewrite (_ : (fun x => _) = mindic R mA)//.
+  apply/measurable_EFinP => /=; rewrite (_ : (fun x => _) = mindic R mA)//.
   by apply/funext => -[].
 rewrite /=.
 apply: eq_integral => y _.
@@ -2067,7 +2067,7 @@ under eq_integral.
   under eq_integral do rewrite retE /=.
   over.
 rewrite (sfinite_Fubini (T' z) (U' z) (fun x => \d_(x.1, x.2) A ))//; last first.
-  apply/EFin_measurable_fun => /=; rewrite (_ : (fun x => _) = mindic R mA)//.
+  apply/measurable_EFinP => /=; rewrite (_ : (fun x => _) = mindic R mA)//.
   by apply/funext => -[].
 rewrite /=.
 apply: eq_integral => y _.