Structures · Analysis
MeasureTheory.Measure.IsNegInvariant
A measure is invariant under negation if - μ = μ. Equivalently, this means that for all
measurable A we have μ (- A) = μ A, where - A is the pointwise negation of A.
- Defined in
- Mathlib.MeasureTheory.Group.Measure
- Shape
- One type argument · adds neg_eq_self
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by45
- MeasureTheory.Measure.map_neg_eq_self
- MeasureTheory.convolution_flip
- MeasureTheory.Measure.measurePreserving_neg
- MeasureTheory.IntegrableOn.comp_neg
- MeasureTheory.integral_neg_eq_self
- MeasureTheory.convolution_eq_swap
- MeasureTheory.Measure.measurePreserving_sub_left
- MeasureTheory.convolutionExistsAt_flip
- MeasureTheory.Integrable.comp_sub_left
- MeasureTheory.Measure.IsNegInvariant.neg_eq_self
- MeasureTheory.contDiffOn_convolution_left_with_param
- MeasureTheory.lintegral_neg_eq_self
- HasCompactSupport.convolutionExists_left
- MeasureTheory.Integrable.comp_neg
- MeasureTheory.IntegrableOn.comp_neg_Iio
- MeasureTheory.Measure.measure_neg
- HasCompactSupport.contDiff_convolution_left
- MeasureTheory.integral_sub_left_eq_self
- MeasureTheory.IntegrableOn.comp_neg_Ici
- MeasureTheory.convolution_neg_of_neg_eq
- MeasureTheory.integrable_comp_sub_left
- MeasureTheory.Measure.neg_eq_self
- MeasureTheory.Measure.map_sub_left_eq_self
- MeasureTheory.Measure.measurePreserving_add_right_neg
- HasCompactSupport.continuous_convolution_left
- MeasureTheory.contDiffOn_convolution_left_with_param_comp
- MeasureTheory.Measure.pi.isNegInvariant
- BddAbove.continuous_convolution_left_of_integrable
- MeasureTheory.lintegral_sub_left_eq_self
- MeasureTheory.ConvolutionExistsAt.integrable_swap
- MeasureTheory.Pi.isNegInvariant_volume
- MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_isNegInvariant
- HasCompactSupport.convolutionExists_right_of_continuous_left
- MeasureTheory.Measure.map_sub_left_ae
- MeasureTheory.lconvolution_comm
- MeasureTheory.convolution_lsmul_swap
- MeasureTheory.IntegrableOn.comp_neg_Iic
- MeasureTheory.Measure.map_add_right_neg_eq_self
- HasCompactSupport.hasDerivAt_convolution_left
- MeasureTheory.Measure.measure_preimage_neg
- HasCompactSupport.hasFDerivAt_convolution_left
- MeasureTheory.Measure.instIsNegInvariantForallVolumeOfMeasurableNegOfSigmaFinite
- MeasureTheory.convolution_mul_swap
- MeasureTheory.convolutionExistsAt_iff_integrable_swap
- MeasureTheory.IntegrableOn.comp_neg_Ioi
Ancestors0
No ancestors.