a hierarchy and a theory of kernels

Co-authored-by: Cyril Cohen <[email protected]>
Co-authored-by: @AyumuSaito

CHANGELOG_UNRELEASED.md

@@ -77,6 +77,24 @@
     `powere_posNyr`, `fine_powere_pos`, `powere_pos_ge0`,
     `powere_pos_gt0`, `powere_pos_eq0`, `powere_posM`, `powere12_sqrt`
 
+
+- in file `kernel.v`,
+  + new definitions `kseries`, `measure_fam_uub`, `kzero`, `kdirac`,
+    `prob_pointed`, `mset`, `pset`, `pprobability`, `kprobability`, `kadd`,
+    `mnormalize`, `knormalize`, `kcomp`, and `mkcomp`.
+  + new lemmas `eq_kernel`, `measurable_fun_kseries`, `integral_kseries`,
+    `measure_fam_uubP`, `eq_sfkernel`, `kzero_uub`, `sfinite_finite`,
+    `sfinite`, `sfinite_kernel_measure`, `finite_kernel_measure`,
+    `measurable_prod_subset_xsection_kernel`,
+    `measurable_fun_xsection_finite_kernel`,
+    `measurable_fun_xsection_integral`,
+    `measurable_fun_integral_finite_kernel`,
+    `measurable_fun_integral_sfinite_kernel`, `lt0_mset`, `gt1_mset`,
+    `kernel_measurable_eq_cst`, `kernel_measurable_neq_cst`, `kernel_measurable_fun_eq_cst`,
+    `measurable_fun_kcomp_finite`, `mkcomp_sfinite`,
+    `measurable_fun_mkcomp_sfinite`, `measurable_fun_preimage_integral`,
+    `measurable_fun_integral_kernel`, and `integral_kcomp`.
+
 ### Changed
 
 - in `mathcomp_extra.v`
@@ -89,6 +107,8 @@
     `power_pos_inv`, `power_pos_intmul`
 - in `lebesgue_measure.v`:
   + lemmas `measurable_fun_ln`, `measurable_fun_power_pos`
+- in `lebesgue_integral.v`:
+  + lemma `xsection_ndseq_closed` generalized from a measure to a family of measures
 
 ### Changed
 

_CoqProject

@@ -39,6 +39,7 @@ theories/lebesgue_integral.v
 theories/summability.v
 theories/signed.v
 theories/itv.v
+theories/kernel.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v