1.9. ForMathlib.Probability.Kernel.KernelSub
Kernel substraction
Module LeanMachineLearning.ForMathlib.Probability.Kernel.KernelSub contains 15 exposed declarations.
-
MeasureTheory.Measure.sub_apply_eq_rnDeriv_add_singularPart -
ProbabilityTheory.Kernel.instSubOfDecidableIsSFiniteKernel_leanMachineLearning -
ProbabilityTheory.Kernel.sub_def -
ProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_left -
ProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_right -
ProbabilityTheory.Kernel.sub_of_isSFiniteKernel -
ProbabilityTheory.Kernel.sub_apply_eq_rnDeriv_add_singularPart -
ProbabilityTheory.Kernel.sub_apply -
ProbabilityTheory.Kernel.le_iff -
ProbabilityTheory.Kernel.sub_le_self -
ProbabilityTheory.Kernel.instIsFiniteKernelHSub_leanMachineLearning -
ProbabilityTheory.Kernel.sub_apply_eq_zero_iff_le -
ProbabilityTheory.Kernel.sub_eq_zero_iff_le -
ProbabilityTheory.Kernel.measurableSet_eq_zero -
ProbabilityTheory.Kernel.measurableSet_eq