Radon nikodym

CHANGELOG_UNRELEASED.md

@@ -88,6 +88,28 @@
   + 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 `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`, `finite_mzero`
+  + factory `Measure_isFinite`, `Measure_isSFinite`
+  + lemma `sfinite_measure`
+  + mixin `FiniteMeasure_isSubProbability`, structure `SubProbability`,
+    notation `subprobability`
+  + factory `Measure_isSubProbability`
+  + factory `FiniteMeasure_isSubProbability`
+  + factory `Measure_isSigmaFinite`
+  + lemmas `fin_num_fun_finite_measure`, `finite_measure_fin_num_fun`
+  + definition `fin_num_fun`
+  + structure `FinNumFun`
+  + definition `finite_measure2`
+  + lemmas `finite_measure2_finite_measure`, `finite_measure_finite_measure2`
 
 ### Changed
 
@@ -107,6 +129,11 @@
   + lemma `max_fimfun_subproof`
   + mixin `IsNonNegFun`, structure `NonNegFun`, notation `{nnfun _ >-> _}`
 
+- in `measure.v`:
+  + `finite_measure` is now a lemma that applies to a finite measure
+  + order of arguments of `isContent`, `Content`, `measure0`, `isMeasure0`,
+    `Measure`, `isSigmaFinite`, `SigmaFiniteContent`, `SigmaFiniteMeasure`
+
 ### Renamed
 
 - in `measurable.v`:
@@ -148,6 +175,9 @@
   + `xsection_preimage_snd`, `ysection_preimage_fst`
 - in `constructive_ereal.v`:
   + `oppeD`, `oppeB`
+- in `measure.v`:
+  + `sigma_finite` generalized from `numFieldType` to `numDomainType`
+  + `finite_measure_sigma_finite` generalized from `measurableType` to `algebraOfSetsType`
 
 ### Deprecated
 

_CoqProject

@@ -38,6 +38,8 @@ theories/numfun.v
 theories/lebesgue_integral.v
 theories/summability.v
 theories/signed.v
+theories/charge.v
+theories/radon_nikodym.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v