Commit 2024-09-04 07:24 ee3c8402

View on Github →

feat: use junk value in Kernel.map, new class IsZeroOrMarkovKernel (#16403) Followup to #16130, doing this at the level of kernels instead of measures.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean

added theorem MeasureTheory.measurable_embeddingReal

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/Probability/Independence/Basic.lean

modified theorem ProbabilityTheory.IndepSets.indep'

modified theorem ProbabilityTheory.IndepSets.indep

modified theorem ProbabilityTheory.indepSet_empty_left

modified theorem ProbabilityTheory.indepSet_empty_right

modified theorem ProbabilityTheory.indep_bot_left

modified theorem ProbabilityTheory.indep_bot_right

modified theorem ProbabilityTheory.indep_iSup_of_antitone

modified theorem ProbabilityTheory.indep_iSup_of_monotone

Modified Mathlib/Probability/Independence/Kernel.lean

Modified Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.eq_zero_or_isMarkovKernel

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.Kernel.IsMarkovKernel.map

added theorem ProbabilityTheory.Kernel.fst_eq

modified theorem ProbabilityTheory.Kernel.fst_map_prod

added theorem ProbabilityTheory.Kernel.mapOfMeasurable_eq_map

modified theorem ProbabilityTheory.Kernel.map_apply

modified theorem ProbabilityTheory.Kernel.map_id'

modified theorem ProbabilityTheory.Kernel.map_id

added theorem ProbabilityTheory.Kernel.map_of_not_measurable

modified theorem ProbabilityTheory.Kernel.map_prodMkLeft

modified theorem ProbabilityTheory.Kernel.map_prodMkRight

modified theorem ProbabilityTheory.Kernel.map_zero

added theorem ProbabilityTheory.Kernel.snd_eq

modified theorem ProbabilityTheory.Kernel.snd_map_prod

modified theorem ProbabilityTheory.Kernel.sum_map_seq

added theorem ProbabilityTheory.Kernel.swapRight_eq

Modified Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean

Modified Mathlib/Probability/Kernel/Disintegration/Unique.lean

Modified Mathlib/Probability/Kernel/RadonNikodym.lean