Commit 2025-01-03 11:02 08ad1629

View on Github →

feat(Probability): proper kernels (#19434) Define proper kernels, which are self-kernels which can meaningfully be restricted to an event. From GibbsMeasure

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Kernel/Proper.lean

added theorem ProbabilityTheory.Kernel.IsProper.lintegral_mul

added theorem ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_bind

added theorem ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_indicator_mul_lintegral

added theorem ProbabilityTheory.Kernel.IsProper.setLIntegral_inter_eq_indicator_mul_setLIntegral

added structure ProbabilityTheory.Kernel.IsProper

added theorem ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul

added theorem ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul