Commit 2025-10-02 14:28 e4f93e72

feat(Probability): characterize conditional independence with conditional distributions (#30024) Two random variables f, g are conditionally independent given a third k iff the conditional distribution of f given k and g is equal to the conditional distribution of f given k.

CondIndepFun (mγ.comap k) hk.comap_le g f μ ↔
  condDistrib f (fun ω ↦ (k ω, g ω)) μ =ᵐ[μ.map (fun ω ↦ (k ω, g ω))]
    (condDistrib f k μ).prodMkRight _ 

From the LeanBandits project.