Commit 2024-03-17 17:51 8a25f82b

feat(Probability/Kernel): build a kernel from a kernel CDF (#11209) Let κ : kernel α (β × ℝ) and ν : kernel α β be two finite kernels. A function f : α × β → StieltjesFunction is called a conditional kernel CDF of κ with respect to ν if it is measurable, tends to to 0 at -∞ and to 1 at +∞ for all p : α × β, if fun b ↦ f (a, b) x is (ν a)-integrable for all a : α and x : ℝ and for all measurable sets s : Set β, ∫ b in s, f (a, b) x ∂(ν a) = (κ a (s ×ˢ Iic x)).toReal. From such a function with property hf : IsCondKernelCDF f κ ν, we build a kernel (α × β) ℝ denoted by hf.toKernel f such that κ = ν ⊗ₖ hf.toKernel f. The new file has substantial overlap with the contents of Probability.Kernel.Disintegration and Probability.Kernel.CondCdf: these two files will later be refactored to use the code in this PR.