Generalize mfun (#1256)

---------

Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -84,15 +84,45 @@
   + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`,
     `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`,
     `disj_itv_Rhull`
+- in `topology.v`:
+  + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
+    `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
+	into local `Let`'s
+
+- in `lebesgue_integral.v`:
+  + structure `SimpleFun` now inside a module `HBSimple`
+  + structure `NonNegSimpleFun` now inside a module `HBNNSimple`
+  + lemma `cst_nnfun_subproof` has now a different statement
+  + lemma `indic_nnfun_subproof` has now a different statement
+
 
 ### Renamed
 
 ### Generalized
 
+- in `lebesgue_integral.v`:
+  + generalized from `sigmaRingType`/`realType` to `sigmaRingType`/`sigmaRingType`
+    * mixin `isMeasurableFun`
+    * structure `MeasurableFun`
+	* definition `mfun`
+    * lemmas `mfun_rect`, `mfun_valP`, `mfuneqP`
+
 ### Deprecated
 
 ### Removed
 
+- in `lebesgue_integral.v`:
+  + definition `cst_mfun`
+  + lemma `mfun_cst`
+
+- in `cardinality.v`:
+  + lemma `cst_fimfun_subproof`
+
+- in `lebesgue_integral.v`:
+  + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
+  + lemma `cst_nnfun_subproof` (turned into a `Let`)
+  + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead)
+
 ### Infrastructure
 
 ### Misc

classical/cardinality.v

@@ -1324,9 +1324,9 @@ suff -> : cst x @` [set: aT] = [set x] by apply: finite_set1.
 by apply/predeqP => y; split=> [[t' _ <-]//|->//] /=; exists point.
 Qed.
 
-Lemma cst_fimfun_subproof aT rT x : @FiniteImage aT rT (cst x).
-Proof. by split; exact: finite_image_cst. Qed.
-HB.instance Definition _ aT rT x := @cst_fimfun_subproof aT rT x.
+HB.instance Definition _ aT rT x :=
+  FiniteImage.Build aT rT (cst x) (@finite_image_cst aT rT x).
+
 Definition cst_fimfun {aT rT} x := [the {fimfun aT >-> rT} of cst x].
 
 Lemma fimfun_cst aT rT x : @cst_fimfun aT rT x =1 cst x. Proof. by []. Qed.

theories/charge.v

@@ -1914,6 +1914,8 @@ Implicit Types f : T -> \bar R.
 
 Local Notation "'d nu '/d mu" := (f nu mu).
 
+Import HBNNSimple.
+
 Lemma change_of_variables f E : (forall x, 0 <= f x) ->
     measurable E -> measurable_fun E f ->
   \int[mu]_(x in E) (f x * ('d nu '/d mu) x) = \int[nu]_(x in E) f x.

theories/kernel.v

@@ -504,6 +504,8 @@ Section measurable_fun_integral_finite_sfinite.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable k : X * Y -> \bar R.
 
+Import HBNNSimple.
+
 Lemma measurable_fun_xsection_integral
     (l : X -> {measure set Y -> \bar R})
     (k_ : {nnsfun (X * Y) >-> R}^nat)
@@ -949,6 +951,7 @@ HB.export KCOMP_SFINITE_KERNEL.
 
 Section measurable_fun_preimage_integral.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Import HBNNSimple.
 Variables (k : Y -> \bar R)
   (k_ : ({nnsfun Y >-> R}) ^nat)
   (ndk_ : nondecreasing_seq (k_ : (Y -> R)^nat))
@@ -963,7 +966,7 @@ HB.instance Definition _ n := @isNonNegFun.Build _ _ _ (k_2_ge0 n).
 Let mk_2 n : measurable_fun [set: X * Y] (k_2 n).
 Proof. by apply: measurableT_comp => //; exact: measurable_snd. Qed.
 
-HB.instance Definition _ n := @isMeasurableFun.Build _ _ _ _ (mk_2 n).
+HB.instance Definition _ n := @isMeasurableFun.Build _ _ _ _ _ (mk_2 n).
 
 Let fk_2 n : finite_set (range (k_2 n)).
 Proof.
@@ -992,6 +995,10 @@ Qed.
 
 End measurable_fun_preimage_integral.
 
+Section measurable_fun_integral_kernel.
+
+Import HBNNSimple.
+
 Lemma measurable_fun_integral_kernel
     d d' (X : measurableType d) (Y : measurableType d') (R : realType)
     (l : X -> {measure set Y -> \bar R})
@@ -1004,6 +1011,8 @@ have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x).
 by apply: (measurable_fun_preimage_integral ndk_ k_k) => n r; exact/ml.
 Qed.
 
+End measurable_fun_integral_kernel.
+
 Section integral_kcomp.
 Context d d2 d3 (X : measurableType d) (Y : measurableType d2)
   (Z : measurableType d3) (R : realType).
@@ -1017,6 +1026,8 @@ rewrite integral_indic//= /kcomp.
 by apply: eq_integral => y _; rewrite integral_indic.
 Qed.
 
+Import HBNNSimple.
+
 Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) :
   \int[kcomp l k x]_z (f z)%:E = \int[l x]_y (\int[k (x, y)]_z (f z)%:E).
 Proof.