Bochner integrals of convolutions

This file contains results about the Bochner integrals of convolutions of measures.

These results are not placed in the main convolution file because we don't want to import Bochner integrals over there.

Main statements

• integrable_conv_iff: A function is integrable with respect to the convolution μ ∗ ν iff the function y ↦ f (x + y) is integrable with respect to ν for μ-almost every x and the function x ↦ ∫ y, ‖f (x + y)‖ ∂ν is integrable with respect to μ.
• integral_conv: if f is integrable with respect to the convolution μ ∗ ν, then ∫ x, f x ∂(μ ∗ₘ ν) = ∫ x, ∫ y, f (x + y) ∂ν ∂μ.

theorem MeasureTheory.integrable_mconv_iff {M : Type u_1} {F : Type u_2} [Monoid M] {mM : MeasurableSpace M} [MeasurableMul₂ M] [NormedAddCommGroup F] {μ ν : Measure M} {f : M → F} [SFinite ν] (hf : AEStronglyMeasurable f (μ.mconv ν)) : Integrable f (μ.mconv ν) ↔ (∀ᵐ (x : M) ∂μ, Integrable (fun (y : M) => f (x * y)) ν) ∧ Integrable (fun (x : M) => ∫ (y : M), ‖f (x * y)‖ ∂ν) μ

theorem MeasureTheory.integrable_conv_iff {M : Type u_1} {F : Type u_2} [AddMonoid M] {mM : MeasurableSpace M} [MeasurableAdd₂ M] [NormedAddCommGroup F] {μ ν : Measure M} {f : M → F} [SFinite ν] (hf : AEStronglyMeasurable f (μ.conv ν)) : Integrable f (μ.conv ν) ↔ (∀ᵐ (x : M) ∂μ, Integrable (fun (y : M) => f (x + y)) ν) ∧ Integrable (fun (x : M) => ∫ (y : M), ‖f (x + y)‖ ∂ν) μ

theorem MeasureTheory.integral_mconv {M : Type u_1} {F : Type u_2} [Monoid M] {mM : MeasurableSpace M} [MeasurableMul₂ M] [NormedAddCommGroup F] {μ ν : Measure M} {f : M → F} [NormedSpace ℝ F] [SFinite μ] [SFinite ν] (hf : Integrable f (μ.mconv ν)) : ∫ (x : M), f x ∂μ.mconv ν = ∫ (x : M), ∫ (y : M), f (x * y) ∂ν ∂μ

theorem MeasureTheory.integral_conv {M : Type u_1} {F : Type u_2} [AddMonoid M] {mM : MeasurableSpace M} [MeasurableAdd₂ M] [NormedAddCommGroup F] {μ ν : Measure M} {f : M → F} [NormedSpace ℝ F] [SFinite μ] [SFinite ν] (hf : Integrable f (μ.conv ν)) : ∫ (x : M), f x ∂μ.conv ν = ∫ (x : M), ∫ (y : M), f (x + y) ∂ν ∂μ