1.15. ForMathlib.Probability.Kernel.Composition.IntegralCompProd🔗

Lp functions with respect to a composition of kernels and measures

Module LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.IntegralCompProd contains 2 exposed declarations.

• MeasureTheory.Measure.memLp_comp_iffLemma · 0 deps
• MeasureTheory.norm_integral_rpow_le_integral_norm_rpowLemma · 0 deps