Commit 2023-06-16 17:18 88b137e2

View on Github →

feat: port Probability.Kernel.Invariance (#5142)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Kernel/Invariance.lean

added theorem ProbabilityTheory.kernel.Invariant.comp

added theorem ProbabilityTheory.kernel.Invariant.comp_const

added theorem ProbabilityTheory.kernel.Invariant.def

added def ProbabilityTheory.kernel.Invariant

added theorem ProbabilityTheory.kernel.bind_add

added theorem ProbabilityTheory.kernel.bind_smul

added theorem ProbabilityTheory.kernel.comp_const_apply_eq_bind

added theorem ProbabilityTheory.kernel.const_bind_eq_comp_const