move pprobability to measure.v (#1171)

CHANGELOG_UNRELEASED.md

@@ -6,6 +6,10 @@
 
 ### Changed
 
+- move from `kernel.v` to `measure.v`
+  + definition `mset`, `pset`, `pprobability`
+  + lemmas `lt0_mset`, `gt1_mset`
+
 ### Renamed
 
 - in `constructive_ereal.v`:

theories/charge.v

@@ -704,7 +704,7 @@ have g_cvg_0 : (g_ \o v) n @[n --> \oo] --> 0 by apply: mine2_cvg_0_cvg_0 => //=
 have nuDAoo : nu D >= nu (D `\` Aoo).
   rewrite -[in leRHS](@setDUK _ Aoo D); last first.
     by apply: bigcup_sub => i _; exact: A_D.
-  by rewrite chargeU// ?lee_addr// ?setDIK//; exact: measurableD.
+  by rewrite chargeU// ?leeDr// ?setDIK//; exact: measurableD.
 split; [by []| |by []]; split; [exact: measurableD | move=> E mE EDAoo].
 pose H n := subDD (\big[setU/set0]_(i < n) A_ (v i)).
 have EH n : [set nu E] `<=` H n.
@@ -940,7 +940,7 @@ Proof. by rewrite /= /cscale/= EFinN mulN1e. Qed.
 Let positive_set_cjordan_neg E : 0 <= cjordan_neg E.
 Proof.
 rewrite cjordan_negE /crestr0/=; case: ifPn; rewrite ?oppe0//.
-move=> /[!inE] mE; rewrite /crestr lee_oppr oppe0.
+move=> /[!inE] mE; rewrite /crestr leeNr oppe0.
 by move: nuPN => [_ [_ +] _ _] => -> //; exact: measurableI.
 Qed.
 
@@ -1496,7 +1496,7 @@ have hnu S : measurable S -> \int[mu]_(x in S) h x <= nu S.
   have mSDAP : measurable (S `\` AP) by exact: measurableD.
   rewrite integral_setU //.
   - rewrite measureU//.
-      by apply: lee_add; [exact: hnuN|exact: hnuP].
+      by apply: leeD; [exact: hnuN|exact: hnuP].
     by rewrite setDE setIACA setICl setI0.
   - exact: measurable_funTS.
   - by rewrite disj_set2E setDE setIACA setICl setI0.

theories/kernel.v

@@ -36,10 +36,6 @@ Require Import numfun lebesgue_measure lebesgue_integral.
 (*                        SFiniteKernel if the sum is over s-finite kernels.  *)
 (*               kzero == kernel defined using the mzero measure              *)
 (*           kdirac mf == kernel defined by a measurable function             *)
-(*            mset U r == the set of probability measures mu such that        *)
-(*                        mu U < r                                            *)
-(*                pset == the sets mset U r with U measurable and r \in [0,1] *)
-(*        pprobability == the measurable type generated by pset               *)
 (*      kprobability m == kernel defined by a probability measure             *)
 (*          kadd k1 k2 == lifting of the addition of measures to kernels      *)
 (*              l \; k == composition of kernels                              *)
@@ -627,38 +623,6 @@ HB.instance Definition _ := Kernel_isProbability.Build _ _ _ _ _
 End kdirac.
 Arguments kdirac {d d' X Y R f}.
 
-Section dist_salgebra_instance.
-Context d (T : measurableType d) (R : realType).
-
-Let p0 : probability T R := [the probability _ _ of dirac point].
-
-HB.instance Definition _ := gen_eqMixin (probability T R).
-HB.instance Definition _ := gen_choiceMixin (probability T R).
-HB.instance Definition _ := isPointed.Build (probability T R) p0.
-
-Definition mset (U : set T) (r : R) := [set mu : probability T R | mu U < r%:E].
-
-Lemma lt0_mset (U : set T) (r : R) : (r < 0)%R -> mset U r = set0.
-Proof.
-move=> r0; apply/seteqP; split => // x/=.
-by apply/negP; rewrite -leNgt (@le_trans _ _ 0)// lee_fin ltW.
-Qed.
-
-Lemma gt1_mset (U : set T) (r : R) :
-  measurable U -> (1 < r)%R -> mset U r = [set: probability T R].
-Proof.
-move=> mU r1; apply/seteqP; split => // x/= _.
-by rewrite /mset/= (le_lt_trans (probability_le1 _ _)).
-Qed.
-
-Definition pset : set (set (probability T R)) :=
-  [set mset U r | r in `[0%R,1%R] & U in measurable].
-
-Definition pprobability : measurableType pset.-sigma :=
-  [the measurableType _ of salgebraType pset].
-
-End dist_salgebra_instance.
-
 Section kprobability.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable P : X -> pprobability Y R.
@@ -726,7 +690,7 @@ exists (fun n => [the _.-ker _ ~> _ of kadd (f1 n) (f2 n)]).
   have [r1 f1r1] := measure_uub (f1 n).
   have [r2 f2r2] := measure_uub (f2 n).
   exists (r1 + r2)%R => x/=.
-  by rewrite /msum !big_ord_recr/= big_ord0 add0e EFinD lte_add.
+  by rewrite /msum !big_ord_recr/= big_ord0 add0e EFinD lteD.
 move=> x U mU.
 rewrite /kadd/= -/(measure_add (k1 x) (k2 x)) measure_addE hk1//= hk2//=.
 rewrite /mseries -nneseriesD//; apply: eq_eseriesr => n _ /=.
@@ -746,7 +710,7 @@ Proof.
 have [f1 hk1] := measure_uub k1; have [f2 hk2] := measure_uub k2.
 exists (f1 + f2)%R => x; rewrite /kadd /=.
 rewrite -/(measure_add (k1 x) (k2 x)).
-by rewrite measure_addE EFinD; exact: lte_add.
+by rewrite measure_addE EFinD; exact: lteD.
 Qed.
 
 HB.instance Definition _ t :=

theories/measure.v

@@ -81,46 +81,51 @@ From HB Require Import structures.
 (*                            T is expected to be a semiring of sets and R a  *)
 (*                            numFieldType.                                   *)
 (*                            The HB class is Measure.                        *)
-(* Content_SubSigmaAdditive_isMeasure ==                                      *)
-(*                      mixin that extends a content to a measure with the    *)
-(*                      proof that it is semi_sigma_additive                  *)
-(* Content_isMeasure == factory that extends a content to a measure with      *)
-(*                      the proof that it is sub_sigma_additive               *)
-(*                 isMeasure == factory corresponding to the "textbook        *)
+(* Content_SubSigmaAdditive_isMeasure == mixin that extends a content to a    *)
+(*                            measure with the proof that it is               *)
+(*                            semi_sigma_additive                             *)
+(*       Content_isMeasure == factory that extends a content to a measure     *)
+(*                            with the proof that it is sub_sigma_additive    *)
+(*               isMeasure == factory corresponding to the "textbook          *)
 (*                            definition" of measures                         *)
-(*           sfinite_measure == predicate for s-finite measure functions      *)
+(*         sfinite_measure == predicate for s-finite measure functions        *)
 (* {sfinite_measure set T -> \bar R} == type of s-finite measures             *)
 (*                            The HB class is SFiniteMeasure.                 *)
-(*    sfinite_measure_seq mu == the sequence of finite measures of the        *)
+(*  sfinite_measure_seq mu == the sequence of finite measures of the          *)
 (*                            s-finite measure mu                             *)
-(*  Measure_isSFinite_subdef == mixin for s-finite measures                   *)
-(*         Measure_isSFinite == factory for s-finite measures                 *)
+(* Measure_isSFinite_subdef == mixin for s-finite measures                    *)
+(*       Measure_isSFinite == factory for s-finite measures                   *)
 (* {sigma_finite_content set T -> \bar R} == contents that are also sigma     *)
 (*                            finite                                          *)
 (*                            The HB class is SigmaFiniteContent.             *)
 (* {sigma_finite_measure set T -> \bar R} == measures that are also sigma     *)
 (*                            finite                                          *)
 (*                            The HB class is SigmaFiniteMeasure.             *)
-(*          sigma_finite A f == the measure function f is sigma-finite on the *)
+(*        sigma_finite A f == the measure function f is sigma-finite on the   *)
 (*                            A : set T with T a semiring of sets             *)
-(*               fin_num_fun == predicate for finite function over measurable *)
+(*             fin_num_fun == predicate for finite function over measurable   *)
 (*                            sets                                            *)
-(*            FinNumFun.type == type of functions over semiring of sets       *)
+(*          FinNumFun.type == type of functions over semiring of sets         *)
 (*                            returning a fin_num                             *)
 (*                            The HB class is FinNumFun.                      *)
 (* {finite_measure set T -> \bar R} == finite measures                        *)
 (*                            The HB class is FiniteMeasure.                  *)
-(*      SigmaFinite_isFinite == mixin for finite measures                     *)
-(*          Measure_isFinite == factory for finite measures                   *)
-(*       subprobability T R == subprobability measure over the measurableType *)
+(*    SigmaFinite_isFinite == mixin for finite measures                       *)
+(*        Measure_isFinite == factory for finite measures                     *)
+(*      subprobability T R == subprobability measure over the measurableType  *)
 (*                            T with values in \bar R with R : realType       *)
 (*                            The HB class is SubProbability.                 *)
 (*         probability T R == probability measure over the measurableType T   *)
 (*                            with values in \bar with R : realType           *)
-(*               probability == type of probability measures                  *)
+(*             probability == type of probability measures                    *)
 (*                            The HB class is Probability.                    *)
-(*     Measure_isProbability == factor for probability measures               *)
-(*              mnormalize mu == normalization of a measure to a probability  *)
+(*   Measure_isProbability == factor for probability measures                 *)
+(*           mnormalize mu == normalization of a measure to a probability     *)
+(*                mset U r == the set of probability measures mu such that    *)
+(*                            mu U < r                                        *)
+(*                    pset == the sets mset U r with U measurable and         *)
+(*                            r \in [0,1]                                     *)
+(*            pprobability == the measurable type generated by pset           *)
 (* {outer_measure set T -> \bar R} == type of an outer measure over sets      *)
 (*                            of elements of type T : Type where R is         *)
 (*                            expected to be a numFieldType                   *)
@@ -2950,6 +2955,11 @@ HB.mixin Record isProbability d (T : measurableType d) (R : realType)
 HB.structure Definition Probability d (T : measurableType d) (R : realType) :=
   {P of @SubProbability d T R P & isProbability d T R P }.
 
+HB.instance Definition _ d (T : measurableType d) (R : realType) :=
+  gen_eqMixin (probability T R).
+HB.instance Definition _ d (T : measurableType d) (R : realType) :=
+  gen_choiceMixin (probability T R).
+
 Section probability_lemmas.
 Context d (T : measurableType d) (R : realType) (P : probability T R).
 
@@ -3036,6 +3046,35 @@ HB.instance Definition _ x :=
 
 End pdirac.
 
+HB.instance Definition _ d (T : measurableType d) (R : realType) :=
+  isPointed.Build (probability T R) [the probability _ _ of dirac point].
+
+Section dist_salgebra_instance.
+Context d (T : measurableType d) (R : realType).
+
+Definition mset (U : set T) (r : R) := [set mu : probability T R | mu U < r%:E].
+
+Lemma lt0_mset (U : set T) (r : R) : (r < 0)%R -> mset U r = set0.
+Proof.
+move=> r0; apply/seteqP; split => // x/=.
+by apply/negP; rewrite -leNgt (@le_trans _ _ 0)// lee_fin ltW.
+Qed.
+
+Lemma gt1_mset (U : set T) (r : R) :
+  measurable U -> (1 < r)%R -> mset U r = [set: probability T R].
+Proof.
+move=> mU r1; apply/seteqP; split => // x/= _.
+by rewrite /mset/= (le_lt_trans (probability_le1 _ _)).
+Qed.
+
+Definition pset : set (set (probability T R)) :=
+  [set mset U r | r in `[0%R,1%R] & U in measurable].
+
+Definition pprobability : measurableType pset.-sigma :=
+  [the measurableType _ of salgebraType pset].
+
+End dist_salgebra_instance.
+
 Lemma sigma_finite_counting (R : realType) :
   sigma_finite [set: nat] (@counting _ R).
 Proof.