ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f f' : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddGroup G<VAR>x : G<VAR>hfg : MeasureTheory.ConvolutionExistsAt f g x L μ<VAR>hfg' : MeasureTheory.ConvolutionExistsAt f' g x L μ<GOAL>MeasureTheory.convolution (f + f') g L μ x = MeasureTheory.convolution f g L μ x + MeasureTheory.convolution f' g L μ x
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f f' : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddGroup G<VAR>hfg : MeasureTheory.ConvolutionExists f g L μ<VAR>hfg' : MeasureTheory.ConvolutionExists f' g L μ<GOAL>MeasureTheory.convolution (f + f') g L μ = MeasureTheory.convolution f g L μ + MeasureTheory.convolution f' g L μ
<VAR>G : Type uG<VAR>x : G<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>f g g' : G → ℝ<VAR>hfg : MeasureTheory.ConvolutionExistsAt f g x (ContinuousLinearMap.lsmul ℝ ℝ) μ<VAR>hfg' : MeasureTheory.ConvolutionExistsAt f g' x (ContinuousLinearMap.lsmul ℝ ℝ) μ<VAR>hf : ∀ (x : G), 0 ≤ f x<VAR>hg : ∀ (x : G), g x ≤ g' x<GOAL>MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ x ≤ MeasureTheory.convolution f g' (ContinuousLinearMap.lsmul ℝ ℝ) μ x
<VAR>G : Type uG<VAR>x : G<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddGroup G<VAR>f g g' : G → ℝ<VAR>hfg' : MeasureTheory.ConvolutionExistsAt f g' x (ContinuousLinearMap.lsmul ℝ ℝ) μ<VAR>hf : ∀ (x : G), 0 ≤ f x<VAR>hg : ∀ (x : G), g x ≤ g' x<VAR>hg' : ∀ (x : G), 0 ≤ g' x<GOAL>MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ x ≤ MeasureTheory.convolution f g' (ContinuousLinearMap.lsmul ℝ ℝ) μ x
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddRightInvariant<VAR>h1 : f =ᵐ[μ] f'<VAR>h2 : g =ᵐ[μ] g'<GOAL>MeasureTheory.convolution f g L μ = MeasureTheory.convolution f' g' L μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddGroup G<GOAL>Function.support (MeasureTheory.convolution f g L μ) ⊆ Function.support g + Function.support f
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddRightInvariant<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.Integrable (MeasureTheory.convolution f g L μ) μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>T2Space G<VAR>hcf : HasCompactSupport f<VAR>hcg : HasCompactSupport g<GOAL>HasCompactSupport (MeasureTheory.convolution f g L μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>P : Type uP<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>TopologicalSpace P<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : ContinuousOn (↿g) (s ×ˢ Set.univ)<GOAL>ContinuousOn (fun q => MeasureTheory.convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>P : Type uP<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>TopologicalSpace P<VAR>s : Set P<VAR>v : P → G<VAR>hv : ContinuousOn v s<VAR>g : P → G → E'<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : ContinuousOn (↿g) (s ×ˢ Set.univ)<GOAL>ContinuousOn (fun x => MeasureTheory.convolution f (g x) L μ (v x)) s
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>hcg : HasCompactSupport g<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : Continuous g<GOAL>Continuous (MeasureTheory.convolution f g L μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>FirstCountableTopology G<VAR>SecondCountableTopologyEither G E'<VAR>hbg : BddAbove (Set.range fun x => ‖g x‖)<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : Continuous g<GOAL>Continuous (MeasureTheory.convolution f g L μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddCommGroup G<GOAL>Function.support (MeasureTheory.convolution f g L μ) ⊆ Function.support f + Function.support g
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddCommGroup G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>MeasurableNeg G<VAR>MeasurableAdd G<GOAL>MeasureTheory.convolution g f L.flip μ = MeasureTheory.convolution f g L μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>x : G<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddCommGroup G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>MeasurableNeg G<VAR>MeasurableAdd G<GOAL>MeasureTheory.convolution f g L μ x = ∫ (t : G), (L (f (x - t))) (g t) ∂μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>x : G<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddCommGroup G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>MeasurableNeg G<VAR>MeasurableAdd G<VAR>f : G → 𝕜<VAR>g : G → F<GOAL>MeasureTheory.convolution f g (ContinuousLinearMap.lsmul 𝕜 𝕜) μ x = ∫ (t : G), f (x - t) • g t ∂μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>x : G<VAR>NontriviallyNormedField 𝕜<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>AddCommGroup G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>MeasurableNeg G<VAR>MeasurableAdd G<VAR>NormedSpace ℝ 𝕜<VAR>f g : G → 𝕜<GOAL>MeasureTheory.convolution f g (ContinuousLinearMap.mul 𝕜 𝕜) μ x = ∫ (t : G), f (x - t) * g t ∂μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>x : G<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddCommGroup G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>MeasurableNeg G<VAR>MeasurableAdd G<VAR>h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x<VAR>h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x<GOAL>MeasureTheory.convolution f g L μ (-x) = MeasureTheory.convolution f g L μ x
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddCommGroup G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : Continuous f<VAR>hg : MeasureTheory.LocallyIntegrable g μ<GOAL>Continuous (MeasureTheory.convolution f g L μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>AddCommGroup G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>FirstCountableTopology G<VAR>SecondCountableTopologyEither G E<VAR>hbf : BddAbove (Set.range fun x => ‖f x‖)<VAR>hf : Continuous f<VAR>hg : MeasureTheory.Integrable g μ<GOAL>Continuous (MeasureTheory.convolution f g L μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>SeminormedAddCommGroup G<VAR>x₀ : G<VAR>R : ℝ<VAR>hf : Function.support f ⊆ Metric.ball 0 R<VAR>hg : ∀ x ∈ Metric.ball x₀ R, g x = g x₀<GOAL>MeasureTheory.convolution f g L μ x₀ = ∫ (t : G), (L (f t)) (g x₀) ∂μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedSpace ℝ F<VAR>SeminormedAddCommGroup G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>μ.IsAddLeftInvariant<VAR>MeasureTheory.SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : MeasureTheory.Integrable f μ<VAR>hf : Function.support f ⊆ Metric.ball 0 R<VAR>hmg : MeasureTheory.AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ Metric.ball x₀ R, dist (g x) z₀ ≤ ε<GOAL>dist (MeasureTheory.convolution f g L μ x₀) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>NormedAddCommGroup E'<VAR>g : G → E'<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>SeminormedAddCommGroup G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>μ.IsAddLeftInvariant<VAR>MeasureTheory.SFinite μ<VAR>NormedSpace ℝ E'<VAR>CompleteSpace E'<VAR>f : G → ℝ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hf : Function.support f ⊆ Metric.ball 0 R<VAR>hnf : ∀ (x : G), 0 ≤ f x<VAR>hintf : ∫ (x : G), f x ∂μ = 1<VAR>hmg : MeasureTheory.AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ Metric.ball x₀ R, dist (g x) z₀ ≤ ε<GOAL>dist (MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) z₀ ≤ ε
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>NormedAddCommGroup E'<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>SeminormedAddCommGroup G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>μ.IsAddLeftInvariant<VAR>MeasureTheory.SFinite μ<VAR>NormedSpace ℝ E'<VAR>CompleteSpace E'<VAR>ι : Type u_1<VAR>g : ι → G → E'<VAR>l : Filter ι<VAR>x₀ : G<VAR>z₀ : E'<VAR>φ : ι → G → ℝ<VAR>k : ι → G<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x<VAR>hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1<VAR>hφ : Filter.Tendsto (fun n => Function.support (φ n)) l (𝓝 0).smallSets<VAR>hmg : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (g i) μ<VAR>hcg : Filter.Tendsto (Function.uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀)<VAR>hk : Filter.Tendsto k l (𝓝 x₀)<GOAL>Filter.Tendsto (fun i => MeasureTheory.convolution (φ i) (g i) (ContinuousLinearMap.lsmul ℝ ℝ) μ (k i)) l (𝓝 z₀)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace G<VAR>μ ν : MeasureTheory.Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>AddGroup G<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>μ.IsAddRightInvariant<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ E'<VAR>CompleteSpace E<VAR>CompleteSpace E'<VAR>hf : MeasureTheory.Integrable f ν<VAR>hg : MeasureTheory.Integrable g μ<GOAL>∫ (x : G), MeasureTheory.convolution f g L ν x ∂μ = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 E''<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace G<VAR>μ ν : MeasureTheory.Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>NormedSpace 𝕜 F'<VAR>CompleteSpace F'<VAR>NormedAddCommGroup F''<VAR>NormedSpace ℝ F''<VAR>NormedSpace 𝕜 F''<VAR>CompleteSpace F''<VAR>k : G → E''<VAR>L₂ : F →L[𝕜] E'' →L[𝕜] F'<VAR>L₃ : E →L[𝕜] F'' →L[𝕜] F'<VAR>L₄ : E' →L[𝕜] E'' →L[𝕜] F''<VAR>AddGroup G<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>μ.IsAddRightInvariant<VAR>MeasurableAdd₂ G<VAR>ν.IsAddRightInvariant<VAR>MeasurableNeg G<VAR>hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)<VAR>x₀ : G<VAR>hfg : ∀ᵐ (y : G) ∂μ, MeasureTheory.ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, MeasureTheory.ConvolutionExistsAt g k x L₄ μ<VAR>hi : MeasureTheory.Integrable (Function.uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)<GOAL>MeasureTheory.convolution (MeasureTheory.convolution f g L ν) k L₂ μ x₀ = MeasureTheory.convolution f (MeasureTheory.convolution g k L₄ μ) L₃ ν x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 E''<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace G<VAR>μ ν : MeasureTheory.Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>NormedSpace 𝕜 F'<VAR>CompleteSpace F'<VAR>NormedAddCommGroup F''<VAR>NormedSpace ℝ F''<VAR>NormedSpace 𝕜 F''<VAR>CompleteSpace F''<VAR>k : G → E''<VAR>L₂ : F →L[𝕜] E'' →L[𝕜] F'<VAR>L₃ : E →L[𝕜] F'' →L[𝕜] F'<VAR>L₄ : E' →L[𝕜] E'' →L[𝕜] F''<VAR>AddGroup G<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>μ.IsAddRightInvariant<VAR>MeasurableAdd₂ G<VAR>ν.IsAddRightInvariant<VAR>MeasurableNeg G<VAR>hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)<VAR>x₀ : G<VAR>hf : MeasureTheory.AEStronglyMeasurable f ν<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>hk : MeasureTheory.AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, MeasureTheory.ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, MeasureTheory.ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (ContinuousLinearMap.mul ℝ ℝ) μ<VAR>hfgk : MeasureTheory.ConvolutionExistsAt (fun x => ‖f x‖) (MeasureTheory.convolution (fun x => ‖g x‖) (fun x => ‖k x‖) (ContinuousLinearMap.mul ℝ ℝ) μ) x₀ (ContinuousLinearMap.mul ℝ ℝ) ν<GOAL>MeasureTheory.convolution (MeasureTheory.convolution f g L ν) k L₂ μ x₀ = MeasureTheory.convolution f (MeasureTheory.convolution g k L₄ μ) L₃ ν x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 E''<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>g : G → E'' →L[𝕜] E'<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hcg : HasCompactSupport g<VAR>hg : Continuous g<VAR>x₀ : G<VAR>x : E''<GOAL>(MeasureTheory.convolution f g (ContinuousLinearMap.precompR E'' L) μ x₀) x = MeasureTheory.convolution f (fun a => (g a) x) L μ x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>NormedSpace 𝕜 G<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<GOAL>HasFDerivAt (MeasureTheory.convolution f g L μ) (MeasureTheory.convolution f (fderiv 𝕜 g) (ContinuousLinearMap.precompR G L) μ x₀) x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>g : G → E'<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>NormedSpace 𝕜 G<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>hcf : HasCompactSupport f<VAR>hf : ContDiff 𝕜 1 f<VAR>hg : MeasureTheory.LocallyIntegrable g μ<VAR>x₀ : G<GOAL>HasFDerivAt (MeasureTheory.convolution f g L μ) (MeasureTheory.convolution (fderiv 𝕜 f) g (ContinuousLinearMap.precompL G L) μ x₀) x₀
<VAR>𝕜 : Type u𝕜<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>f₀ : 𝕜 → E<VAR>g₀ : 𝕜 → E'<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>μ : MeasureTheory.Measure 𝕜<VAR>μ.IsAddLeftInvariant<VAR>MeasureTheory.SFinite μ<VAR>hf : MeasureTheory.LocallyIntegrable f₀ μ<VAR>hcg : HasCompactSupport g₀<VAR>hg : ContDiff 𝕜 1 g₀<VAR>x₀ : 𝕜<GOAL>HasDerivAt (MeasureTheory.convolution f₀ g₀ L μ) (MeasureTheory.convolution f₀ (deriv g₀) L μ x₀) x₀
<VAR>𝕜 : Type u𝕜<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>f₀ : 𝕜 → E<VAR>g₀ : 𝕜 → E'<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>μ : MeasureTheory.Measure 𝕜<VAR>μ.IsAddLeftInvariant<VAR>MeasureTheory.SFinite μ<VAR>μ.IsNegInvariant<VAR>hcf : HasCompactSupport f₀<VAR>hf : ContDiff 𝕜 1 f₀<VAR>hg : MeasureTheory.LocallyIntegrable g₀ μ<VAR>x₀ : 𝕜<GOAL>HasDerivAt (MeasureTheory.convolution f₀ g₀ L μ) (MeasureTheory.convolution (deriv f₀) g₀ L μ x₀) x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>P : Type uP<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>f : G → E<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace G<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup P<VAR>NormedSpace 𝕜 P<VAR>μ : MeasureTheory.Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ Set.univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<GOAL>HasFDerivAt (fun q => MeasureTheory.convolution f (g q.1) L μ q.2) (MeasureTheory.convolution f (fun x => fderiv 𝕜 (↿g) (q₀.1, x)) (ContinuousLinearMap.precompR (P × G) L) μ q₀.2) q₀
<VAR>𝕜 : Type u𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>G E' F P : Type uP<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup P<VAR>NormedSpace 𝕜 P<VAR>f : G → E<VAR>n : ℕ∞<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 n (↿g) (s ×ˢ Set.univ)<GOAL>ContDiffOn 𝕜 n (fun q => MeasureTheory.convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)