Commit 2023-10-31 15:03 95e9bc17

feat(Probability/Density): Random variables are independent iff joint density is product (#8026) This PR proves that two random variables are independent, iff their joint distribution is the product measure of marginal distributions, iff their joint density is a product of their marginal densities up to AE equality. It also uses lemmas stating that μ.withDensity is injective up to AE equality.