fixes #1943 (#1944)

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -109,6 +109,8 @@
   + `Rintegral_itv_bndo_bndc` -> `Rintegral_itvbo_itvbc`
   + `Rintegral_itv_obnd_cbnd` -> `Rintegral_itvob_itvcb`
 
+- in `measure_function.v`:
+  + `isFinite` -> `isFinNumFun`
 
 ### Generalized
 

theories/charge.v

@@ -138,7 +138,7 @@ HB.builders Context d (T : semiRingOfSetsType d) (R : realFieldType)
 
 Let finite : fin_num_fun mu. Proof. exact: charge_finite. Qed.
 
-HB.instance Definition _ := isFinite.Build d T R mu finite.
+HB.instance Definition _ := isFinNumFun.Build d T R mu finite.
 
 Let semi_additive : measure_function.semi_additive mu.
 Proof.
@@ -298,7 +298,7 @@ move=> mU.
 by have /(fin_num_measure nu) : measurable (U `&` D) by exact: measurableI.
 Qed.
 
-HB.instance Definition _ := isFinite.Build _ _ _
+HB.instance Definition _ := isFinNumFun.Build _ _ _
   restr crestr_finite_measure_function.
 
 Let crestr_semi_additive : measure_function.semi_additive restr.
@@ -402,7 +402,7 @@ Let cscale0 : cscale set0 = 0. Proof. by rewrite /cscale charge0 mule0. Qed.
 Let cscale_finite_measure_function U : measurable U -> cscale U \is a fin_num.
 Proof. by move=> mU; apply: fin_numM => //; exact: fin_num_measure. Qed.
 
-HB.instance Definition _ := isFinite.Build _ _ _
+HB.instance Definition _ := isFinNumFun.Build _ _ _
   cscale cscale_finite_measure_function.
 
 Let cscale_semi_additive : measure_function.semi_additive cscale.

theories/kernel.v

@@ -1332,7 +1332,7 @@ suff KE : kfcomp k (EFin \o \1_(B `\` A)) =
   by split; [exact: measurableD|rewrite KE; exact: emeasurable_funB].
 apply/funext => x/=.
 pose kx : {measure set T2 -> \bar R} := k x.
-pose H1 := isFinite.Build _ _ _ _ (@kernel_finite_transition _ _ _ _ R k x).
+pose H1 := isFinNumFun.Build _ _ _ _ (@kernel_finite_transition _ _ _ _ R k x).
 pose H2 := isSFinite.Build _ _ _ _ (finite_measure_sfinite
   (@kernel_finite_transition _ _ _ _ R k x)).
 pose H3 := isSigmaFinite.Build _ _ _ _ (finite_measure_sigma_finite
@@ -1416,7 +1416,7 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x =>
   under eq_integral do rewrite EFinM.
   rewrite integralZl//.
   pose kx : {measure set T2 -> \bar R} := k x.
-  pose H1 := isFinite.Build _ _ _ _ (@kernel_finite_transition _ _ _ _ R k x).
+  pose H1 := isFinNumFun.Build _ _ _ _ (@kernel_finite_transition _ _ _ _ R k x).
   pose H2 := isSFinite.Build _ _ _ _ (finite_measure_sfinite
     (@kernel_finite_transition _ _ _ _ R k x)).
   pose H3 := isSigmaFinite.Build _ _ _ _ (finite_measure_sigma_finite

theories/measure_theory/measure_function.v

@@ -76,7 +76,7 @@ From mathcomp Require Import measurable_structure measurable_function.
 (*         Measure_isSFinite == interface that extends a measure to an        *)
 (*                              s-finite measure using a sequence of finite   *)
 (*                              measures                                      *)
-(*                  isFinite == interface for functions that satisfy the      *)
+(*               isFinNumFun == interface for functions that satisfy the      *)
 (*                              fin_num_fun predicate                         *)
 (*            FinNumFun.type == type of functions over semiring of sets       *)
 (*                              returning a fin_num                           *)
@@ -1400,14 +1400,22 @@ Proof. exact/sfinite_measure_sigma_finite/sigma_finite_mzero. Qed.
 HB.instance Definition _ d (T : measurableType d) (R : realType) :=
   @isSFinite.Build d T R mzero (@sfinite_mzero d T R).
 
-HB.mixin Record isFinite d (T : semiRingOfSetsType d) (R : numDomainType)
+HB.mixin Record isFinNumFun d (T : semiRingOfSetsType d) (R : numDomainType)
   (k : set T -> \bar R) := { fin_num_measure : fin_num_fun k }.
 
+#[deprecated(since="mathcomp-analysis 1.17.0", use=isFinNumFun)]
+Notation isFinite x1 x2 x3 x4 := (isFinNumFun x1 x2 x3 x4).
+
+Module isFinite.
+#[deprecated(since="mathcomp-analysis 1.117.0", use=isFinNumFun)]
+Notation Build x1 x2 x3 x4 := (isFinNumFun.Build x1 x2 x3 x4) (only parsing).
+End isFinite.
+
 HB.structure Definition FinNumFun d (T : semiRingOfSetsType d)
-  (R : numFieldType) := { k of isFinite _ T R k }.
+  (R : numFieldType) := { k of isFinNumFun _ T R k }.
 
 HB.structure Definition FiniteMeasure d (T : sigmaRingType d) (R : realType) :=
-  { k of @SigmaFiniteMeasure _ _ _ k & isFinite _ T R k }.
+  { k of @SigmaFiniteMeasure _ _ _ k & isFinNumFun _ T R k }.
 Arguments fin_num_measure {d T R} _.
 
 Notation "{ 'finite_measure' 'set' T '->' '\bar' R }" :=
@@ -1437,7 +1445,7 @@ HB.instance Definition _ := @isSigmaFinite.Build d T R k sigma_finite.
 
 Let finite : fin_num_fun k. Proof. exact: fin_num_measure. Qed.
 
-HB.instance Definition _ := @isFinite.Build d T R k finite.
+HB.instance Definition _ := @isFinNumFun.Build d T R k finite.
 
 HB.end.
 

theories/probability_theory/random_variable.v

@@ -679,7 +679,7 @@ transitivity (- \int[mu]_(s in `]-oo, 0%R]) P (Y @^-1` `[(- s)%R, +oo[)).
   move/measurable_EFinP : mfPleY; apply: eq_measurable_fun => r /= _.
   by rewrite fineK// fin_num_measure.
 transitivity (- \int[mu]_(s in `]-oo, 0%R] `\ 0%R) P (Y @^-1` `[(- s)%R, +oo[)).
-  congr -%E; rewrite setDitv1r integral_itv_bndo_bndc//=.
+  congr -%E; rewrite setDitv1r integral_itvbo_itvbc//=.
   apply/measurable_funTS => /=.
   under eq_fun => s
     do rewrite -(@fineK _ (P (Y @^-1` `[(- s)%R, +oo[))) ?fin_num_measure//.