Commit 2025-10-01 13:25 caee90cf

View on Github →

feat(Probability/Independence): relate conditional independence and factorization of a kernel (#29884)

CondIndepFun m' hm' f g μ
  ↔ (condExpKernel μ m').map (fun ω ↦ (f ω, g ω))
    =ᵐ[μ.trim hm'] (condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g

From the LeanBandits project.

Estimated changes