English
Let μ, ν be measures on a monoid M with convolution mconv, and f: M → F be AEStronglyMeasurable with respect to μ ∗ₘ ν. Then f is integrable w.r.t. μ ∗ₘ ν if and only if (i) for almost every x with respect to μ, the function y ↦ f(xy) is integrable with respect to ν, and (ii) the function x ↦ ∫ ‖f(xy)‖ dν(y) is integrable with respect to μ.
Русский
Пусть μ, ν — меры на полугруппе M; функция f: M → F AEStronglyMeasurable относительно μ ∗ₘ ν. Тогда f интегрируема по μ ∗ₘ ν тогда и только тогда, когда (i) для почти всех x по μ функция y ↦ f(xy) интегрируема по ν, и (ii) функция x ↦ ∫ ‖f(xy)‖ dν(y) интегрируема по μ.
LaTeX
$$$$ \\mathrm{Integrable}(f, \\mu \\ast_m \\nu) \\iff \\left( \\forall^{\\mathrm{ae}} x \\partial \\mu,\; \\mathrm{Integrable}(y \\mapsto f(xy), \\nu) \\right) \\land \\mathrm{Integrable}\\left(x \\mapsto \\int_G \\|f(xy)\\| \\, d\\nu(y), \\mu\\right). $$$$
Lean4
@[to_additive]
theorem integrable_mconv_iff [SFinite ν] (hf : AEStronglyMeasurable f (μ ∗ₘ ν)) :
Integrable f (μ ∗ₘ ν) ↔ (∀ᵐ x ∂μ, Integrable (fun y ↦ f (x * y)) ν) ∧ Integrable (fun x ↦ ∫ y, ‖f (x * y)‖ ∂ν) μ :=
by
simp [Measure.mconv, integrable_map_measure hf (by fun_prop), integrable_prod_iff (hf.comp_measurable (by fun_prop))]
