TODO

Extra arguments to convolution_zero

theorem MeasureTheory.ConvolutionExists.of_finite {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] {f : G → E} {g : G → E'} {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : Measure G} [AddGroup G] [Finite G] [MeasurableSingletonClass G] [IsFiniteMeasure μ] : ConvolutionExists f g L μ

theorem MeasureTheory.convolution_assoc''' {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} {F' : Type u_6} {F'' : Type u_7} {E'' : Type u_8} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup E''] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 E''] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] {μ ν : Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [CompleteSpace F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedSpace 𝕜 F'] [CompleteSpace F'] [NormedAddCommGroup F''] [NormedSpace ℝ F''] [NormedSpace 𝕜 F''] [CompleteSpace F''] {k : G → E''} (L₂ : F →L[𝕜] E'' →L[𝕜] F') (L₃ : E →L[𝕜] F'' →L[𝕜] F') (L₄ : E' →L[𝕜] E'' →L[𝕜] F'') [AddGroup G] [SFinite μ] [SFinite ν] [μ.IsAddRightInvariant] {f : G → E} {g : G → E'} [MeasurableAdd₂ G] [ν.IsAddRightInvariant] [MeasurableNeg G] (hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)) (hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν) (hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ) (hi : ∀ (x₀ : G), Integrable (Function.uncurry fun (x y : G) => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)) : convolution (convolution f g L ν) k L₂ μ = convolution f (convolution g k L₄ μ) L₃ ν

Convolution is associative. This has a weak but inconvenient integrability condition. See also MeasureTheory.convolution_assoc.

theorem MeasureTheory.convolution_assoc'' {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} {F' : Type u_6} {F'' : Type u_7} {E'' : Type u_8} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup E''] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 E''] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] {μ ν : Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [CompleteSpace F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedSpace 𝕜 F'] [CompleteSpace F'] [NormedAddCommGroup F''] [NormedSpace ℝ F''] [NormedSpace 𝕜 F''] [CompleteSpace F''] {k : G → E''} (L₂ : F →L[𝕜] E'' →L[𝕜] F') (L₃ : E →L[𝕜] F'' →L[𝕜] F') (L₄ : E' →L[𝕜] E'' →L[𝕜] F'') [AddGroup G] [SFinite μ] [SFinite ν] [μ.IsAddRightInvariant] {f : G → E} {g : G → E'} [MeasurableAdd₂ G] [ν.IsAddRightInvariant] [MeasurableNeg G] (hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)) (hf : AEStronglyMeasurable f ν) (hg : AEStronglyMeasurable g μ) (hk : AEStronglyMeasurable k μ) (hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν) (hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun (x : G) => ‖g x‖) (fun (x : G) => ‖k x‖) x (ContinuousLinearMap.mul ℝ ℝ) μ) (hfgk : ConvolutionExists (fun (x : G) => ‖f x‖) (convolution (fun (x : G) => ‖g x‖) (fun (x : G) => ‖k x‖) (ContinuousLinearMap.mul ℝ ℝ) μ) (ContinuousLinearMap.mul ℝ ℝ) ν) : convolution (convolution f g L ν) k L₂ μ = convolution f (convolution g k L₄ μ) L₃ ν

Convolution is associative. This requires that

• all maps are a.e. strongly measurable w.r.t one of the measures
• f ⋆[L, ν] g exists almost everywhere
• ‖g‖ ⋆[μ] ‖k‖ exists almost everywhere
• ‖f‖ ⋆[ν] (‖g‖ ⋆[μ] ‖k‖) exists at x₀

@[simp]

theorem MeasureTheory.convolution_translate {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] {ν : Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [AddCommGroup G] (a : G) (f : G → E) (g : G → E') : convolution f (translate a g) L ν = translate a (convolution f g L ν)

@[simp]

theorem MeasureTheory.translate_convolution {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] {ν : Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [AddCommGroup G] [MeasurableAdd G] [ν.IsAddRightInvariant] (a : G) (f : G → E) (g : G → E') : convolution (translate a f) g L ν = translate a (convolution f g L ν)