Commit 2026-05-04 16:33 b44e5279

View on Github →

feat(Probability/Kernel): define IsDeterministic (#38211) Defines the IsDeterministic typeclass which state that a kernel is deterministic in a categorical sense, i.e., it "commutes" with Kernel.copy. For some additional context, please see #37851.

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Typeclasses/ZeroOne.lean

added theorem MeasureTheory.IsZeroOneMeasure.exists_eq_dirac

added theorem MeasureTheory.IsZeroOneMeasure.exists_measure_eq_one_iff_measure_univ_eq_one

added theorem MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one

added theorem MeasureTheory.IsZeroOneMeasure.measure_inter_eq_prod

added theorem MeasureTheory.IsZeroOneMeasure.measure_univ

added theorem MeasureTheory.Measure.zero_one

Modified Mathlib/Probability/Kernel/Composition/Comp.lean

added theorem ProbabilityTheory.Kernel.copy_comp_apply_prod

Modified Mathlib/Probability/Kernel/Composition/KernelLemmas.lean

deleted theorem ProbabilityTheory.Kernel.deterministic_comp_copy

Created Mathlib/Probability/Kernel/Deterministic.lean

added theorem ProbabilityTheory.Kernel.IsDeterministic.exists_eq_deterministic

added theorem ProbabilityTheory.Kernel.comp_parallelComp_comp_copy

added theorem ProbabilityTheory.Kernel.isDeterministic_iff_isZeroOneMeasure

Modified Mathlib/Probability/Kernel/Posterior.lean