Commit 2024-11-23 11:01 0b15a0dc

View on Github →

feat: independence of functions under conditioning (#17915) From PFR

Estimated changes

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/Data/ENNReal/Inv.lean

added theorem ENNReal.prod_inv_distrib

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/Probability/ConditionalProbability.lean

Modified Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.cond_iInter

added theorem ProbabilityTheory.iIndepFun.cond

Modified Mathlib/Probability/Independence/Kernel.lean

added theorem ProbabilityTheory.Kernel.iIndepFun.cond_iInter