Structures · Analysis
MeasureTheory.Measure.Regular
A measure μ is regular if
- it is finite on all compact sets;
- it is outer regular: μ(A) = inf {μ(U) | A ⊆ U open} for A measurable;
- it is inner regular for open sets, using compact sets:
μ(U) = sup {μ(K) | K ⊆ U compact} for U open.
- Defined in
- Mathlib.MeasureTheory.Measure.Regular
- Shape
- One type argument · adds innerRegular
Extends2
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 by64
- MeasureTheory.Measure.Regular.innerRegular
- MeasureTheory.Measure.Regular.map
- MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_regular
- MeasureTheory.addEquivAddHaarChar_smul_map
- IsOpen.measure_eq_iSup_isCompact
- MeasureTheory.mulEquivHaarChar_smul_map
- MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported
- MeasureTheory.addEquivAddHaarChar_eq
- MeasureTheory.mulEquivHaarChar_eq
- MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le
- MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular
- MeasureTheory.Measure.Regular.smul
- MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported_nnreal
- MeasureTheory.Measure.Regular.exists_isCompact_not_null
- MeasureTheory.Measure.support_mem_ae_of_regular
- MeasureTheory.null_iff_of_isAddLeftInvariant
- MeasureTheory.addEquivAddHaarChar_smul_integral_map
- MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariant
- MeasureTheory.MemLp.exists_hasCompactSupport_integral_rpow_sub_le
- MeasureTheory.mulEquivHaarChar_smul_integral_map
- MeasureTheory.measure_ne_zero_iff_nonempty_of_isAddLeftInvariant
- MeasureTheory.distribHaarChar_mul
- MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero
- MeasureTheory.measure_pos_iff_nonempty_of_vaddInvariant
- MeasureTheory.Measure.Regular.comap'
- MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero
- MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant
- MeasureTheory.distribHaarChar_eq_div
- MeasureTheory.null_iff_of_isMulLeftInvariant
- MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le
- MeasureTheory.measure_eq_zero_iff_eq_empty_of_smulInvariant
- NNRealRMK.integralLinearMap_inj
- MeasureTheory.Measure.IsHaarMeasure.isInvInvariant_of_regular
- MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul
- MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le
- MeasureTheory.measure_pos_iff_nonempty_of_isAddLeftInvariant
- RealRMK.integralPositiveLinearMap_inj
- MeasureTheory.mulEquivHaarChar_smul_eq_comap
- MeasureTheory.Measure.Regular.instInnerRegularCompactLTTop
- MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_regular
- MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_regular
- MeasureTheory.Measure.Regular.weaklyRegular
- NNRealRMK.rieszMeasure_integralLinearMap
- MeasureTheory.addEquivAddHaarChar_smul_preimage
- MeasureTheory.measure_eq_zero_iff_eq_empty_of_vaddInvariant
- MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts
- MeasureTheory.Measure.Regular.comap
- MeasureTheory.Measure.Regular.smul_nnreal
- MeasureTheory.Measure.Regular.domSMul
- MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular