adapt to hierarchy with subprob

Author: affeldt-aist

theories/kernel.v

@@ -582,14 +582,6 @@ Arguments measurable_fun_xsection_integral {_ _ _ _ _} k l.
 Arguments measurable_fun_integral_finite_kernel {_ _ _ _ _} k l.
 Arguments measurable_fun_integral_sfinite_kernel {_ _ _ _ _} k l.
 
-Section pdirac.
-Context d (T : measurableType d) (R : realType).
-
-HB.instance Definition _ x :=
-  isProbability.Build _ _ _ (@dirac _ T x R) (diracT R x).
-
-End pdirac.
-
 Section kdirac.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable f : X -> Y.
@@ -825,7 +817,7 @@ by rewrite -{1}(@fineK _ (f x setT))// -EFinM divrr// ?unitfE fine_eq0.
 Qed.
 
 HB.instance Definition _ x :=
-  isProbability.Build _ _ _ (mnormalize x) (mnormalize1 x).
+  Measure_isProbability.Build _ _ _ (mnormalize x) (mnormalize1 x).
 
 End mnormalize.
 

theories/prob_lang.v

@@ -71,7 +71,7 @@ rewrite /bernoulli/= /measure_add/= /msum 2!big_ord_recr/= big_ord0 add0e/=.
 by rewrite /mscale/= !diracT !mule1 -EFinD onem1'.
 Qed.
 
-HB.instance Definition _ := @isProbability.Build _ _ R bernoulli bernoulli_setT.
+HB.instance Definition _ := @Measure_isProbability.Build _ _ R bernoulli bernoulli_setT.
 
 End bernoulli.
 

theories/wip.v

@@ -97,7 +97,7 @@ HB.instance Definition _ := isMeasure.Build _ _ _
 Let mgauss01_setT : mgauss01 [set: _] = 1%E.
 Proof. by rewrite /mgauss01 integral_gauss01_density. Qed.
 
-HB.instance Definition _ := @isProbability.Build _ _ R mgauss01 mgauss01_setT.
+HB.instance Definition _ := @Measure_isProbability.Build _ _ R mgauss01 mgauss01_setT.
 
 Definition gauss01 := [the probability _ _ of mgauss01].