a hierarchy and a theory of kernels

[affeldt-aist]

Motivation for this change

This is the "mathematical part" of PR #749 : the hierarchy of kernels and their theory (stability of s-finite kernels by composition, etc.). This is documented in https://hal.inria.fr/hal-03917948/ (which is a reviewed paper, that might
simplify the review work for this PR).

The "programming language part" of PR #749 is now in the draft PR #912 because it is still the topic of
discussion. Some parts of it might integrate master later though (e.g., kernel for scoring or for conditional branching).

(PR #749 is therefore scheduled for closing.)

@CohenCyril @AyumuSaito

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[zstone1]

Looks pretty good. The comment about an existential vs. 3 fields is the most interesting. Otherwise I don't anything too bad. I find the identical mixin + factory idiom to be a bit strange, but it's fairly common, and I can live with it.

In some sense, an empty factory with an extra condition is what you is maybe what you mean? I tried to do that with

HB.factory Record Kernel_isFinite d d' (X : measurableType d)
    (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R})
    of isKernel _ _ _ _ _ k & SFiniteKernel_isFinite _ _ _ _ _ k := {
  measure_uub : measure_fam_uub k }.

However, I get

Error: I could not find classes covering exactly mixins:
[indt «SFiniteKernel_isFinite.axioms_», indt «isKernel.axioms_»]
In particular the covering [indt «FiniteKernel.axioms_»] also includes mixins:
[indt «Kernel_isSFinite_subdef.axioms_»]
This should never happen, please report a bug.

so that maybe doesn't work quite right.

[zstone1]

I'm fine with things as they are now. Most of my issues are longer term ones about factory and mixin duplication, and R vs \bar R. They're not really complaints about this PR in particular, and I'll be happy to have this kernel stuff in master.