Commit 2024-02-26 08:00 fc8f4175

feat: measurable parametric Stieltjes functions (#10952) We provide tools to build a measurable function α → StieltjesFunction with limits 0 at -∞ and 1 at +∞ for all a : α from a measurable function f : α → ℚ → ℝ. These measurable parametric Stieltjes functions are cumulative distribution functions (CDF) of Markov kernels. The reason for going through ℚ instead of defining directly a Stieltjes function is that since ℚ is countable, building a measurable function is easier and we can obtain properties of the form ∀ᵐ (a : α) ∂μ, ∀ (q : ℚ), ... (for some measure μ on α) by proving the weaker ∀ (q : ℚ), ∀ᵐ (a : α) ∂μ, .... TODO: I will later refactor the CondCdf file to use this file. This will also be used in another new file to build CDFs of kernels, towards proving disintegration of kernels.