ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>E : Type u_2<VAR>PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<GOAL>HasUnitSpeedOn (naturalParameterization f s a) (variationOnFromTo f s a '' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>a x : 𝕜<VAR>𝕜' : Type u_2<VAR>NormedAddCommGroup 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>hh : HasDerivAt h h' (a + x)<GOAL>HasDerivAt (fun x => h (a + x)) h' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>x a : 𝕜<VAR>𝕜' : Type u_2<VAR>NormedAddCommGroup 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>hh : HasDerivAt h h' (x + a)<GOAL>HasDerivAt (fun x => h (x + a)) h' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>a : 𝕜<GOAL>deriv (fun x => f (-x)) a = -deriv f (-a)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>a x : 𝕜<VAR>𝕜' : Type u_2<VAR>NormedAddCommGroup 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>hh : DifferentiableAt 𝕜 h (a + x)<GOAL>deriv (fun x => h (a + x)) x = deriv h (a + x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>a x : 𝕜<VAR>𝕜' : Type u_2<VAR>NormedAddCommGroup 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>hh : DifferentiableAt 𝕜 h (x + a)<GOAL>deriv (fun x => h (x + a)) x = deriv h (x + a)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>x : 𝕜<GOAL>HasStrictDerivAt (⇑f) (f.linear 1) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>L : Filter 𝕜<VAR>x : 𝕜<GOAL>HasDerivAtFilter (⇑f) (f.linear 1) x L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>HasDerivWithinAt (⇑f) (f.linear 1) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>x : 𝕜<GOAL>HasDerivAt (⇑f) (f.linear 1) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>hs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (⇑f) s x = f.linear 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>x : 𝕜<GOAL>deriv (⇑f) x = f.linear 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>x : 𝕜<GOAL>DifferentiableAt 𝕜 (⇑f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<GOAL>Differentiable 𝕜 ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>DifferentiableWithinAt 𝕜 (⇑f) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>s : Set 𝕜<GOAL>DifferentiableOn 𝕜 (⇑f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>a b : E<VAR>x : 𝕜<GOAL>HasStrictDerivAt (⇑(AffineMap.lineMap a b)) (b - a) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>a b : E<VAR>x : 𝕜<GOAL>HasDerivAt (⇑(AffineMap.lineMap a b)) (b - a) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>a b : E<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>HasDerivWithinAt (⇑(AffineMap.lineMap a b)) (b - a) s 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>AddGroup G<VAR>TopologicalSpace G<VAR>C : ℝ<VAR>hC : ∀ (i : G), ‖g i‖ ≤ C<VAR>x t : G<VAR>s u : Set G<VAR>hx : x ∈ s<VAR>hu : -tsupport g + s ⊆ u<GOAL>‖(L (f t)) (g (x - t))‖ ≤ u.indicator (fun t => ‖L‖ * ‖f t‖ * C) 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>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>hcg : HasCompactSupport g<VAR>hg : Continuous g<VAR>x t : G<VAR>s u : Set G<VAR>hx : x ∈ s<VAR>hu : -tsupport g + s ⊆ u<GOAL>‖(L (f t)) (g (x - t))‖ ≤ u.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) 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>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>hcg : HasCompactSupport g<VAR>hg : Continuous g<VAR>x t : G<VAR>s : Set G<VAR>hx : x ∈ s<GOAL>‖(L (f t)) (g (x - t))‖ ≤ (-tsupport g + s).indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) 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>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ContinuousSub G<VAR>hg : Continuous g<VAR>t : G<GOAL>Continuous fun x => (L (f t)) (g (x - 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>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : Continuous f<VAR>x t : G<VAR>s : Set G<VAR>hx : x ∈ s<GOAL>‖(L (f (x - t))) (g t)‖ ≤ (-tsupport f + s).indicator (fun t => (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) 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>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>Sub G<VAR>x : G<VAR>h : MeasureTheory.ConvolutionExistsAt f g x L μ<GOAL>MeasureTheory.Integrable (fun t => (L (f t)) (g (x - 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>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>AddGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>MeasureTheory.SFinite ν<VAR>hf : MeasureTheory.AEStronglyMeasurable f ν<VAR>hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun p => p.1 - p.2) (μ.prod ν))<GOAL>MeasureTheory.AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
<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>AddGroup G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>x : G<VAR>hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun t => x - t) μ)<GOAL>MeasureTheory.AEStronglyMeasurable (fun t => (L (f t)) (g (x - 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>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>AddGroup G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>x : G<VAR>hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun t => x - t) μ)<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun t => (L (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>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>AddGroup G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>x₀ : G<VAR>s : Set G<VAR>hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => -t + x₀) ⁻¹' s))<VAR>hs : MeasurableSet s<VAR>h2s : (Function.support fun t => (L (f t)) (g (x₀ - t))) ⊆ s<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>hmg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun t => x₀ - t) (μ.restrict s))<GOAL>MeasureTheory.ConvolutionExistsAt f g x₀ 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>AddGroup G<VAR>MeasurableAdd G<VAR>MeasurableNeg G<VAR>x₀ : G<VAR>h : MeasureTheory.ConvolutionExistsAt (fun x => ‖f x‖) (fun x => ‖g x‖) x₀ (ContinuousLinearMap.mul ℝ ℝ) μ<VAR>hmf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hmg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun t => x₀ - t) μ)<GOAL>MeasureTheory.ConvolutionExistsAt f g x₀ 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>AddGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddRightInvariant<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>x : G<GOAL>MeasureTheory.AEStronglyMeasurable (fun t => (L (f t)) (g (x - 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>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>AddGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddRightInvariant<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>x : G<GOAL>MeasureTheory.AEStronglyMeasurable (fun t => (L (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>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>AddGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddRightInvariant<VAR>x₀ : G<VAR>h : MeasureTheory.ConvolutionExistsAt (fun x => ‖f x‖) (fun x => ‖g x‖) x₀ (ContinuousLinearMap.mul ℝ ℝ) μ<VAR>hmf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hmg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.ConvolutionExistsAt f g x₀ 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>AddGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddRightInvariant<VAR>MeasureTheory.SFinite ν<VAR>hf : MeasureTheory.AEStronglyMeasurable f ν<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
<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>AddGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddRightInvariant<VAR>MeasureTheory.SFinite ν<VAR>hf : MeasureTheory.Integrable f ν<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.Integrable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
<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>AddGroup G<VAR>MeasurableAdd₂ G<VAR>MeasurableNeg G<VAR>MeasureTheory.SFinite μ<VAR>μ.IsAddRightInvariant<VAR>MeasureTheory.SFinite ν<VAR>hf : MeasureTheory.Integrable f ν<VAR>hg : MeasureTheory.Integrable g μ<GOAL>∀ᵐ (x : G) ∂μ, MeasureTheory.ConvolutionExistsAt f g x 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>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>x₀ : G<VAR>h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : Continuous g<GOAL>MeasureTheory.ConvolutionExistsAt f g x₀ 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>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>MeasureTheory.ConvolutionExists 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>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : Continuous g<GOAL>MeasureTheory.ConvolutionExists 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>AddCommGroup G<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>MeasurableAdd₂ G<VAR>MeasureTheory.SFinite μ<VAR>x₀ : G<VAR>s : Set G<VAR>hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => x₀ - t) ⁻¹' s))<VAR>hs : MeasurableSet s<VAR>h2s : (Function.support fun t => (L (f t)) (g (x₀ - t))) ⊆ s<VAR>hf : MeasureTheory.IntegrableOn f s μ<VAR>hmg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.ConvolutionExistsAt f g x₀ 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>AddCommGroup G<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>MeasurableAdd G<VAR>μ.IsNegInvariant<GOAL>MeasureTheory.ConvolutionExistsAt g f x L.flip μ ↔ MeasureTheory.ConvolutionExistsAt f g x 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>AddCommGroup G<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>MeasurableAdd G<VAR>μ.IsNegInvariant<VAR>h : MeasureTheory.ConvolutionExistsAt f g x L μ<GOAL>MeasureTheory.Integrable (fun t => (L (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>AddCommGroup G<VAR>MeasurableNeg G<VAR>μ.IsAddLeftInvariant<VAR>MeasurableAdd G<VAR>μ.IsNegInvariant<GOAL>MeasureTheory.ConvolutionExistsAt f g x L μ ↔ MeasureTheory.Integrable (fun t => (L (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>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>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>hcf : HasCompactSupport f<VAR>hf : Continuous f<VAR>hg : MeasureTheory.LocallyIntegrable g μ<GOAL>MeasureTheory.ConvolutionExists 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>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>BorelSpace G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : Continuous f<VAR>hg : MeasureTheory.LocallyIntegrable g μ<GOAL>MeasureTheory.ConvolutionExists 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>Sub G<GOAL>MeasureTheory.convolution f g L μ x = ∫ (t : G), (L (f t)) (g (x - 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>Sub G<VAR>f : G → 𝕜<VAR>g : G → F<GOAL>MeasureTheory.convolution f g (ContinuousLinearMap.lsmul 𝕜 𝕜) μ x = ∫ (t : G), f t • g (x - t) ∂μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>x : G<VAR>NontriviallyNormedField 𝕜<VAR>MeasurableSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Sub G<VAR>NormedSpace ℝ 𝕜<VAR>f g : G → 𝕜<GOAL>MeasureTheory.convolution f g (ContinuousLinearMap.mul 𝕜 𝕜) μ x = ∫ (t : G), f t * g (x - 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>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>SMulCommClass ℝ 𝕜 F<VAR>y : 𝕜<GOAL>MeasureTheory.convolution (y • f) g L μ = y • 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>SMulCommClass ℝ 𝕜 F<VAR>y : 𝕜<GOAL>MeasureTheory.convolution f (y • g) L μ = y • 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>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>MeasureTheory.convolution 0 g L μ = 0
<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>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>MeasureTheory.convolution f 0 L μ = 0
<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' : 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 (g + 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 : 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>hfg : MeasureTheory.ConvolutionExists f g L μ<VAR>hfg' : MeasureTheory.ConvolutionExists f g' L μ<GOAL>MeasureTheory.convolution f (g + g') L μ = MeasureTheory.convolution f g L μ + MeasureTheory.convolution f g' L μ