Structures · Analysis
MeasurableAdd
We say that a type has MeasurableAdd if (c + ·) and (· + c) are measurable functions.
For a typeclass assuming measurability of uncurry (· + ·) see MeasurableAdd₂.
- Defined in
- Mathlib.MeasureTheory.Group.Arithmetic
- Shape
- One type argument · adds measurable_const_add, measurable_add_const
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- AddOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by103
- MeasureTheory.measure_preimage_add
- MeasurableAdd.measurable_add_const
- MeasurableAdd.measurable_const_add
- MeasurableEquiv.addLeft
- Measurable.const_add
- Measurable.add_const
- MeasurableEquiv.addRight
- MeasureTheory.integral_add_right_eq_self
- AEMeasurable.add_const
- MeasureTheory.integral_sub_right_eq_self
- MeasureTheory.convolution_flip
- MeasureTheory.integral_add_left_eq_self
- MeasureTheory.measurePreserving_add_left
- MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd'
- MeasureTheory.Integrable.comp_sub_right
- MeasureTheory.lintegral_add_left_eq_self
- MeasureTheory.measure_preimage_add_right
- MeasureTheory.convolution_eq_swap
- AEMeasurable.const_add
- MeasureTheory.Measure.measurePreserving_sub_left
- measurableEmbedding_subRight
- MeasureTheory.convolutionExistsAt_flip
- MeasureTheory.Integrable.comp_add_left
- MeasureTheory.measurePreserving_add_right
- MeasureTheory.Integrable.comp_sub_left
- MeasureTheory.Integrable.comp_add_right
- MeasurableEquiv.subLeft
- MeasureTheory.isAddLeftInvariant_map
- MeasureTheory.lintegral_add_right_eq_self
- MeasurableEquiv.subRight
- BddAbove.convolutionExistsAt'
- MeasureTheory.forall_measure_preimage_add_right_iff
- MeasureTheory.map_add_right_ae
- measurableEmbedding_addLeft
- MeasureTheory.map_add_left_ae
- MeasurableEquiv.symm_addLeft
- MeasureTheory.eventually_add_left_iff
- MeasureTheory.map_sub_right_ae
- MeasureTheory.integral_sub_left_eq_self
- MeasureTheory.convolution_neg_of_neg_eq
- MeasureTheory.integral_eq_zero_of_add_right_eq_neg
- MeasureTheory.integrable_comp_sub_left
- MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd'
- VectorFourier.fourierIntegral_comp_add_right
- MeasureTheory.forall_measure_preimage_add_iff
- Measurable.add_simpleFunc
- Measurable.simpleFunc_add
- MeasureTheory.Measure.map_sub_left_eq_self
- MeasureTheory.measurePreserving_sub_right
- MeasureTheory.Measure.measurePreserving_add_right_neg
Ancestors0
No ancestors.