add a type for finite measures (#836)

* add a type for finite measures

- s-finite measures from branch kernels
- add subprobabilities
- dirac instance of probability
- rm finite_measure
- renaming
- minor fix

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -7,7 +7,6 @@
 - in `classical_sets.v`:
   + canonical `unit_pointedType`
 - in `measure.v`:
-  + definition `finite_measure`
   + mixin `isProbability`, structure `Probability`, type `probability`
   + lemma `probability_le1`
   + definition `discrete_measurable_unit`
@@ -36,7 +35,7 @@
   + lemmas `measurable_curry`, `measurable_fun_fst`, `measurable_fun_snd`,
     `measurable_fun_swap`, `measurable_fun_pair`, `measurable_fun_if_pair`
   + lemmas `dirac0`, `diracT`
-  + lemma `finite_measure_sigma_finite`
+  + lemma `fin_num_fun_sigma_finite`
 - in `lebesgue_measure.v`:
   + lemma `measurable_fun_opp`
 - in `lebesgue_integral.v`
@@ -88,6 +87,8 @@
   + new lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, 
     `join_product_continuous`, `join_product_open`, `join_product_inj`, and 
     `join_product_weak`. 
+- in `measure.v`:
+  + structure `FiniteMeasure`, notation `{finite_measure set _ -> \bar _}`
 
 - in file `topology.v`,
   + new definition `clopen`.
@@ -98,6 +99,24 @@
 - in file `topology.v`,
   + new lemmas `powerset_filter_fromP` and `compact_cluster_set1`.
 
+- in `measure.v`:
+  + definition `sfinite_measure_def`
+  + mixin `Measure_isSFinite_subdef`, structure `SFiniteMeasure`,
+    notation `{sfinite_measure set _ -> \bar _}`
+  + mixin `SigmaFinite_isFinite` with field `fin_num_measure`, structure `FiniteMeasure`,
+    notation `{finite_measure set _ -> \bar _}`
+  + lemmas `sfinite_measure_sigma_finite`, `sfinite_mzero`, `sigma_finite_mzero`
+  + factory `Measure_isFinite`, `Measure_isSFinite`
+  + defintion `sfinite_measure_seq`, lemma `sfinite_measure_seqP`
+  + mixin `FiniteMeasure_isSubProbability`, structure `SubProbability`,
+    notation `subprobability`
+  + factory `Measure_isSubProbability`
+  + factory `FiniteMeasure_isSubProbability`
+  + factory `Measure_isSigmaFinite`
+  + lemmas `fin_num_fun_lty`, `lty_fin_num_fun`
+  + definition `fin_num_fun`
+  + structure `FinNumFun`
+
 ### Changed
 
 - in `fsbigop.v`:
@@ -120,6 +139,10 @@
   + lemma `compact_near_coveringP`
 - in `functions.v`:
   + notation `mem_fun_`
+- in `measure.v`:
+  + order of arguments of `isContent`, `Content`, `measure0`, `isMeasure0`,
+    `Measure`, `isSigmaFinite`, `SigmaFiniteContent`, `SigmaFiniteMeasure`
+
 ### Renamed
 
 - in `measurable.v`:
@@ -171,6 +194,8 @@
 - in `lebesgue_integral.v`:
   + lemma `integrable_abse`
 
+  + `sigma_finite` generalized from `numFieldType` to `numDomainType`
+  + `fin_num_fun_sigma_finite` generalized from `measurableType` to `algebraOfSetsType`
 
 ### Deprecated
 

theories/lebesgue_integral.v

@@ -3732,9 +3732,10 @@ End integrable_fune.
 
 Section integral_counting.
 Local Open Scope ereal_scope.
-Variables (R : realType).
+Variable R : realType.
 
-Lemma counting_dirac (A : set nat) : counting R A = \sum_(n <oo) \d_ n A.
+Lemma counting_dirac (A : set nat) :
+  counting A = \sum_(n <oo) \d_ n A :> \bar R.
 Proof.
 have -> : \sum_(n <oo) \d_ n A = \esum_(i in A) \d_ i A :> \bar R.
   rewrite nneseries_esum// (_ : [set _ | _] = setT); last exact/seteqP.
@@ -3753,13 +3754,12 @@ apply: (@le_lt_trans _ _ (\sum_(i <oo) `|fine (a i)|%:E)).
   apply: lee_nneseries => // n _; rewrite integral_dirac//.
   move: (@summable_pinfty _ _ _ _ sa n Logic.I).
   by case: (a n) => //= r _; rewrite indicE/= mem_set// mul1r.
-move: (sa); rewrite /summable (_ : [set: nat] = (fun=> true))//; last exact/seteqP.
-rewrite -nneseries_esum//; apply: le_lt_trans.
-by apply: lee_nneseries => // n _ /=; case: (a n) => //; rewrite leey.
+move: (sa); rewrite /summable -fun_true -nneseries_esum//; apply: le_lt_trans.
+by apply lee_nneseries => // n _ /=; case: (a n) => //; rewrite leey.
 Qed.
 
 Lemma integral_count (a : nat -> \bar R) : summable setT a ->
-  \int[counting R]_t (a t) = \sum_(k <oo) (a k).
+  \int[counting]_t (a t) = \sum_(k <oo) (a k).
 Proof.
 move=> sa.
 transitivity (\int[mseries (fun n => [the measure _ _ of \d_ n]) O]_t a t).

theories/lebesgue_measure.v

@@ -331,7 +331,7 @@ apply/andP; split=> //; apply: contraTneq xbj => ->.
 by rewrite in_itv/= le_gtF// (itvP xabi).
 Qed.
 
-HB.instance Definition _ := isContent.Build _ R _
+HB.instance Definition _ := isContent.Build _ _ R
   (hlength : set ocitv_type -> _) (@hlength_ge0') hlength_semi_additive.
 
 Hint Extern 0 ((_ .-ocitv).-measurable _) => solve [apply: is_ocitv] : core.
@@ -378,7 +378,7 @@ do !case: ifPn => //= ?; do ?by rewrite ?adde_ge0 ?lee_fin// ?subr_ge0// ?ltW.
 by rewrite addrAC lee_fin ler_add// subr_le0 leNgt.
 Qed.
 
-Lemma hlength_sigma_finite : sigma_finite [set: ocitv_type] hlength.
+Lemma hlength_sigma_finite : sigma_finite setT (hlength : set ocitv_type -> _).
 Proof.
 exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic).
   apply/esym; rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=.