Commit 2025-10-01 13:25 11f59c52

View on Github →

feat(Probability): condDistrib lemmas (#29555) From the LeanBandits project.

Estimated changes

Modified Mathlib/Probability/Kernel/CondDistrib.lean

added theorem ProbabilityTheory.condDistrib_ae_eq_iff_measure_eq_compProd

modified theorem ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd

added theorem ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable

added theorem ProbabilityTheory.condDistrib_comp

added theorem ProbabilityTheory.condDistrib_comp_map

added theorem ProbabilityTheory.condDistrib_comp_self

added theorem ProbabilityTheory.condDistrib_congr

added theorem ProbabilityTheory.condDistrib_congr_left

added theorem ProbabilityTheory.condDistrib_congr_right

added theorem ProbabilityTheory.condDistrib_const

added theorem ProbabilityTheory.condDistrib_fst_prod

added theorem ProbabilityTheory.condDistrib_map

added theorem ProbabilityTheory.condDistrib_self

added theorem ProbabilityTheory.condDistrib_snd_prod

Modified Mathlib/Probability/Kernel/Condexp.lean

added theorem ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map