Commit 2024-09-19 18:27 55437489

chore(Probability/Kernel): split Kernel.Basic (#16931) Kernel.Basic becomes 3 files:

• Kernel.Defs with definitions of kernels and classes of kernels
• Kernel.Basic with definitions of basic kernels (deterministic, const...)
• Kernel.Integral with lemmas about Bochner integrals against those basic kernels I also created a new file Independence.Integrable because the split revealed that Independence.Basic depended on the definition of Lp spaces and integrability only through two lemmas. I added one lemma, integral_restrict (in Kernel.Integral), because all kernels had lemmas about integral and setIntegral except that one for which the integral lemma was missing.