theorem MeasureTheory.convolution_symm {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [MeasurableSpace G] {f g : G → E} (L : E →L[𝕜] E →L[𝕜] F) (hL : ∀ (x y : E), (L x) y = (L y) x) [NormedSpace ℝ F] [AddCommGroup G] {μ : Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] : convolution f g L μ = convolution g f L μ

Special case of convolution_flip when L is symmetric.

theorem MeasureTheory.AEStronglyMeasurable.convolution {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] [NormedSpace ℝ F] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SigmaFinite μ] [μ.IsAddRightInvariant] (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : AEStronglyMeasurable (convolution f g L μ) μ

The convolution of two a.e. strongly measurable functions is a.e. strongly measurable.

theorem MeasureTheory.lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] [NormedSpace ℝ F] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsNegInvariant] [μ.IsAddLeftInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q) (hL : ∀ (x y : G), ‖(L (f x)) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) : ∫⁻ (a : G), ‖(L (f a)) (g (x₀ - a))‖ₑ ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ

This implies both of the following theorems convolutionExists_of_memLp_memLp and enorm_convolution_le_eLpNorm_mul_eLpNorm.

theorem MeasureTheory.ConvolutionExists.of_memLp_memLp {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] [NormedSpace ℝ F] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : Measure G) [SFinite μ] [μ.IsNegInvariant] [μ.IsAddLeftInvariant] [μ.IsAddRightInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q) (hL : ∀ (x y : G), ‖(L (f x)) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (hfp : MemLp f p μ) (hgq : MemLp g q μ) : ConvolutionExists f g L μ

If MemLp f p μ and MemLp g q μ, where p and q are Hölder conjugates, then the convolution of f and g exists everywhere.

theorem MeasureTheory.enorm_convolution_le_eLpNorm_mul_eLpNorm {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] [NormedSpace ℝ F] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : Measure G) [SFinite μ] [μ.IsNegInvariant] [μ.IsAddLeftInvariant] [μ.IsAddRightInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q) (hL : ∀ (x y : G), ‖(L (f x)) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) : ‖convolution f g L μ x₀‖ₑ ≤ eLpNorm f p μ * eLpNorm g q μ

If p and q are Hölder conjugates, then the convolution of f and g is bounded everywhere by eLpNorm f p μ * eLpNorm g q μ.