Structures · Analysis
MeasurableAdd₂
We say that a type has MeasurableAdd₂ if uncurry (· + ·) is a measurable function.
For a typeclass assuming measurability of (c + ·) and (· + c) see MeasurableAdd.
- Defined in
- Mathlib.MeasureTheory.Group.Arithmetic
- Shape
- One type argument · adds measurable_add
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- EReal
- MeasureTheory.Measure
- AddOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by168
- Measurable.add
- Measurable.fun_add
- MeasurableAdd₂.measurable_add
- Measurable.tsum
- AEMeasurable.add
- MeasureTheory.quasiMeasurePreserving_neg
- Finset.measurable_sum
- MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant
- ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀'
- Finset.measurable_fun_sum
- MeasureTheory.Integrable.convolution_integrand
- ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetSum_of_notMem
- Finset.aemeasurable_fun_sum
- MeasureTheory.absolutelyContinuous_neg
- AEMeasurable.fun_add
- MeasureTheory.neg_absolutelyContinuous
- ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem₀
- MeasureTheory.measure_add_right_null
- ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀
- ProbabilityTheory.Kernel.iIndepFun.indepFun_add_left
- MeasureTheory.Measure.conv_absolutelyContinuous
- MeasureTheory.aemeasurable_lconvolution
- MeasureTheory.quasiMeasurePreserving_add_right
- MeasureTheory.integral_conv
- MeasureTheory.measure_add_lintegral_eq
- Finset.aemeasurable_sum
- MeasureTheory.conv_eq_withDensity_lconvolution_rnDeriv
- MeasureTheory.Measure.map_conv_addMonoidHom
- MeasureTheory.measurePreserving_prod_add
- MeasureTheory.quasiMeasurePreserving_neg_add
- ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetSum_of_notMem₀
- ProbabilityTheory.IndepFun.hasLaw_add
- MeasureTheory.HaveLebesgueDecomposition.conv
- MeasureTheory.measure_eq_sub_vadd
- MeasureTheory.measurePreserving_add_prod_neg
- MeasureTheory.measurePreserving_prod_neg_add
- MeasureTheory.measurePreserving_prod_neg_add_swap
- ProbabilityTheory.Kernel.iIndepFun.indepFun_add_left₀
- MeasureTheory.Measure.lintegral_conv
- MeasureTheory.measurePreserving_prod_add_right
- MeasureTheory.Measure.lintegral_conv_eq_lintegral_sum
- MeasureTheory.measure_neg_null
- List.aemeasurable_sum
- Measurable.tsum'
- MeasureTheory.measurePreserving_prod_sub_swap
- ProbabilityTheory.Kernel.iIndepFun.indepFun_sum_range_succ
- List.measurable_sum
- Finset.measurable_sum_apply
- MeasureTheory.Measure.conv_dirac
- MeasureTheory.measurable_measure_add_right
Ancestors0
No ancestors.