Commit 2024-03-20 15:45 32531f6a

feat: density of a finite kernel wrt another kernel (#10948) Let κ : kernel α (γ × β) and ν : kernel α γ be two finite kernels with kernel.fst κ ≤ ν, where γ has a countably generated σ-algebra (true in particular for standard Borel spaces). We build a function f : α → γ → Set β → ℝ jointly measurable in the first two arguments such that for all a : α and all measurable sets s : Set β and A : Set γ, ∫ x in A, f a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal.