1.20. ForMathlib.Probability.WithDensity
Lemmas about kernels and measures with density
Module LeanMachineLearning.ForMathlib.Probability.WithDensity contains 9 exposed declarations.
-
MeasureTheory.map_withDensity_comp -
MeasureTheory.map_equiv_withDensity -
MeasureTheory.map_swap_withDensity_comp_snd -
MeasureTheory.Measure.compProd_withDensity_left -
MeasureTheory.Measure.compProd_withDensity_withDensity -
MeasureTheory.Measure.compProd_eq_compProd_withDensity_comp_snd -
ProbabilityTheory.Kernel.comp_withDensity_eq_withDensity_comp -
ProbabilityTheory.Kernel.compProd_withDensity_left -
ProbabilityTheory.Kernel.withDensity_rnDeriv_eq'