Structures · Analysis
MeasurableMul₂
We say that a type has MeasurableMul₂ if uncurry (· * ·) is a measurable function.
For a typeclass assuming measurability of (c * ·) and (· * c) see MeasurableMul.
- Defined in
- Mathlib.MeasureTheory.Group.Arithmetic
- Shape
- One type argument · adds measurable_mul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- ENNReal
- EReal
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by152
- Measurable.fun_mul
- Measurable.mul
- AEMeasurable.fun_mul
- AEMeasurable.mul
- Finset.measurable_prod
- MeasurableMul₂.measurable_mul
- MeasureTheory.quasiMeasurePreserving_inv
- ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀'
- ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem
- MeasureTheory.absolutelyContinuous_inv
- MeasureTheory.measure_mul_right_null
- MeasureTheory.inv_absolutelyContinuous
- MeasureTheory.measurePreserving_prod_mul
- MeasureTheory.Measure.mconv_absolutelyContinuous
- MeasureTheory.quasiMeasurePreserving_inv_mul
- Finset.measurable_fun_prod
- MeasureTheory.measure_mul_lintegral_eq
- MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv
- ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem₀
- MeasureTheory.quasiMeasurePreserving_mul_right
- MeasureTheory.aemeasurable_mlconvolution
- ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left
- Finset.aemeasurable_prod
- MeasureTheory.Measure.lintegral_mconv_eq_lintegral_prod
- Multiset.aemeasurable_prod
- List.aemeasurable_prod
- MeasureTheory.measurePreserving_prod_mul_right
- MeasureTheory.measurePreserving_prod_div_swap
- ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left₀
- MeasureTheory.measurePreserving_prod_mul_swap_right
- ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ
- MeasureTheory.Measure.lintegral_mconv
- MeasureTheory.Measure.mconv_dirac
- MeasureTheory.HaveLebesgueDecomposition.mconv
- MeasureTheory.measurable_measure_mul_right
- MeasureTheory.measurePreserving_prod_mul_swap
- ProbabilityTheory.iIndepFun.indepFun_finsetProd_of_notMem₀
- ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀
- MeasureTheory.measurePreserving_prod_inv_mul
- MeasureTheory.measure_eq_div_smul
- ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul
- List.measurable_prod
- ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right
- ProbabilityTheory.iIndepFun.indepFun_finsetProd_of_notMem
- MeasureTheory.measurePreserving_mul_prod_inv
- MeasureTheory.measurePreserving_prod_inv_mul_swap
- MeasureTheory.mlconvolution_assoc₀
- Multiset.measurable_prod
- MeasureTheory.measure_lintegral_div_measure
- MeasureTheory.measurePreserving_prod_div
Ancestors0
No ancestors.