Commit 2023-03-16 06:43 97d1aa95

View on Github →

feat(probability/kernel/invariance): Define pushforward of measure along a kernel (#18244)

Estimated changes

Modified src/measure_theory/measure/measure_space.lean

Modified src/probability/kernel/basic.lean

added theorem probability_theory.kernel.const_apply

Modified src/probability/kernel/composition.lean

Created src/probability/kernel/invariance.lean

added theorem probability_theory.kernel.comp_apply_eq_map_measure

added theorem probability_theory.kernel.comp_const_apply_eq_map_measure

added theorem probability_theory.kernel.const_map_measure_eq_comp_const

added theorem probability_theory.kernel.invariant.comp

added theorem probability_theory.kernel.invariant.comp_const

added theorem probability_theory.kernel.invariant.def

added def probability_theory.kernel.invariant

added theorem probability_theory.kernel.lintegral_map_measure

added def probability_theory.kernel.map_measure

added theorem probability_theory.kernel.map_measure_add

added theorem probability_theory.kernel.map_measure_apply

added theorem probability_theory.kernel.map_measure_smul

added theorem probability_theory.kernel.map_measure_zero