Commit 2025-02-27 10:04 90911138

View on Github →

feat: add lemmas about kernels (#22200)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Map.lean

modified theorem MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq

Modified Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.Kernel.deterministic_congr

added theorem ProbabilityTheory.Kernel.lintegral_id'

added theorem ProbabilityTheory.Kernel.lintegral_id

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

added theorem ProbabilityTheory.Kernel.comap_prod

added theorem ProbabilityTheory.Kernel.comp_map

added theorem ProbabilityTheory.Kernel.deterministic_map

added theorem ProbabilityTheory.Kernel.deterministic_prod_apply'

added theorem ProbabilityTheory.Kernel.id_comap

added theorem ProbabilityTheory.Kernel.id_map

added theorem ProbabilityTheory.Kernel.id_prod_apply'

added theorem ProbabilityTheory.Kernel.id_prod_eq

added theorem ProbabilityTheory.Kernel.lintegral_deterministic_prod

added theorem ProbabilityTheory.Kernel.lintegral_id_prod

added theorem ProbabilityTheory.Kernel.lintegral_prod_deterministic

added theorem ProbabilityTheory.Kernel.lintegral_prod_id

added theorem ProbabilityTheory.Kernel.lintegral_prod_symm

added theorem ProbabilityTheory.Kernel.map_apply_eq_iff_map_symm_apply_eq

added theorem ProbabilityTheory.Kernel.map_comp_right

added theorem ProbabilityTheory.Kernel.map_prod_eq

added theorem ProbabilityTheory.Kernel.map_prod_map

added theorem ProbabilityTheory.Kernel.prodAssoc_prod