Commit 2024-08-17 05:53 c1cb845a

feat: absolute continuity of Measure.compProd (#11273) For μ ν : Measure α and κ η : Kernel α β,

• If μ ≪ ν and ∀ᵐ a ∂μ, κ a ≪ η a, then μ ⊗ₘ κ ≪ ν ⊗ₘ η
• If μ ⊗ₘ κ ≪ ν ⊗ₘ η, and κ is everywhere nonzero then μ ≪ ν Also remove a few s-finite assumptions in the Probability/Kernel/MeasureCompProd file.