Mathlib Changelog
Changelog
About
Github
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