Theorems · Theorem · abstract harmonic analysis

MeasureTheory.Measure.mconv_absolutelyContinuous

∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] {μ ν ρ : MeasureTheory.Measure M}
  [ρ.IsMulLeftInvariant] [MeasureTheory.SFinite ν], ν.AbsolutelyContinuous ρ → (μ.mconv ν).AbsolutelyContinuous ρ

Defined in

Mathlib.MeasureTheory.Group.Convolution

Cited by

3 results in Mathlib

Foundations

Depth 218 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidMeasurableSpaceMeasurableMul₂MeasureTheory.Measure.IsMulLeftInvariantMeasureTheory.SFinite