English
Let ρ be a left-invariant measure on M, ν a finite measure with ν ≪ ρ. Then for any μ, the convolution μ ∗ₘ ν is absolutely continuous with respect to ρ: (μ ∗ₘ ν) ≪ ρ.
Русский
Пусть ρ — левосторонне инвариантная мера на M, ν — конечная мера с ν ≪ ρ. Тогда для любого μ свёртка μ ∗ₘ ν была бы абсолютно непрерывна по отношению к ρ: (μ ∗ₘ ν) ≪ ρ.
LaTeX
$$$(\\mu \\ast_{m} \\nu) \\ll ρ$$
Lean4
@[to_additive]
theorem mconv_absolutelyContinuous [MeasurableMul₂ M] {μ ν ρ : Measure M} [IsMulLeftInvariant ρ] [SFinite ν]
(hν : ν ≪ ρ) : μ ∗ₘ ν ≪ ρ := by
refine AbsolutelyContinuous.mk (fun s hs h ↦ ?_)
rw [← lintegral_indicator_one hs, lintegral_mconv (by measurability)]
conv in s.indicator 1 (_ * _) => change s.indicator 1 ((fun y ↦ x * y) y)
simp only [← Set.indicator_comp_right, Pi.one_comp]
conv in ∫⁻ _, _ ∂ν => rw [lintegral_indicator_one (by apply MeasurableSet.preimage hs (by fun_prop))]
have h0 (x : M) : ν (HMul.hMul x ⁻¹' s) = 0 := by
apply hν
rw [← map_apply (by fun_prop) hs, IsMulLeftInvariant.map_mul_left_eq_self, h]
simp [h0]
