Commit 2025-09-26 12:24 12335910

View on Github →

feat(Probability): CondIndepFun lemmas (#29554) Lemmas about conditional independence of constant random variables and of random variables that are measurable with respect to the sigma-algebra that we are conditioning on. From the LeanBandits project.

Estimated changes

Modified Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.indepFun_const_left

added theorem ProbabilityTheory.indepFun_const_right

Modified Mathlib/Probability/Independence/Conditional.lean

added theorem ProbabilityTheory.condIndepFun_const_left

added theorem ProbabilityTheory.condIndepFun_const_right

added theorem ProbabilityTheory.condIndepFun_of_measurable_left

added theorem ProbabilityTheory.condIndepFun_of_measurable_right

added theorem ProbabilityTheory.condIndepFun_self_left

added theorem ProbabilityTheory.condIndepFun_self_right

Modified Mathlib/Probability/Independence/Kernel.lean

added theorem ProbabilityTheory.Kernel.indepFun_const_left

added theorem ProbabilityTheory.Kernel.indepFun_const_right