ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ✝ : Type u_4<VAR>inst✝¹⁸ : CommRing Rₘ<VAR>inst✝¹⁷ : Algebra R Rₘ<VAR>inst✝¹⁶ : CommRing Sₘ✝<VAR>inst✝¹⁵ : Algebra S Sₘ✝<VAR>M : Submonoid R<VAR>inst✝¹⁴ : IsLocalization M Rₘ<VAR>inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝<VAR>inst✝¹² : Algebra Rₘ Sₘ✝<VAR>inst✝¹¹ : Algebra R Sₘ✝<VAR>inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝<VAR>inst✝⁹ : IsScalarTower R S Sₘ✝<VAR>Sₘ : Type u_5<VAR>inst✝⁸ : CommRing Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : Algebra R Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>ι : Type u_6<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<VAR>this : Module.Finite R S<GOAL>traceMatrix Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ✝ : Type u_4<VAR>inst✝¹⁸ : CommRing Rₘ<VAR>inst✝¹⁷ : Algebra R Rₘ<VAR>inst✝¹⁶ : CommRing Sₘ✝<VAR>inst✝¹⁵ : Algebra S Sₘ✝<VAR>M : Submonoid R<VAR>inst✝¹⁴ : IsLocalization M Rₘ<VAR>inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝<VAR>inst✝¹² : Algebra Rₘ Sₘ✝<VAR>inst✝¹¹ : Algebra R Sₘ✝<VAR>inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝<VAR>inst✝⁹ : IsScalarTower R S Sₘ✝<VAR>Sₘ : Type u_5<VAR>inst✝⁸ : CommRing Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : Algebra R Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>ι : Type u_6<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<VAR>this✝ : Module.Finite R S<VAR>this : Module.Free R S<GOAL>traceMatrix Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ✝ : Type u_4<VAR>inst✝¹⁸ : CommRing Rₘ<VAR>inst✝¹⁷ : Algebra R Rₘ<VAR>inst✝¹⁶ : CommRing Sₘ✝<VAR>inst✝¹⁵ : Algebra S Sₘ✝<VAR>M : Submonoid R<VAR>inst✝¹⁴ : IsLocalization M Rₘ<VAR>inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝<VAR>inst✝¹² : Algebra Rₘ Sₘ✝<VAR>inst✝¹¹ : Algebra R Sₘ✝<VAR>inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝<VAR>inst✝⁹ : IsScalarTower R S Sₘ✝<VAR>Sₘ : Type u_5<VAR>inst✝⁸ : CommRing Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : Algebra R Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>ι : Type u_6<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<VAR>this✝ : Module.Finite R S<VAR>this : Module.Free R S<VAR>i j : ι<GOAL>traceMatrix Rₘ (⇑(Basis.localizationLocalization Rₘ M Sₘ b)) i j = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b) i j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ✝ : Type u_4<VAR>inst✝¹⁸ : CommRing Rₘ<VAR>inst✝¹⁷ : Algebra R Rₘ<VAR>inst✝¹⁶ : CommRing Sₘ✝<VAR>inst✝¹⁵ : Algebra S Sₘ✝<VAR>M : Submonoid R<VAR>inst✝¹⁴ : IsLocalization M Rₘ<VAR>inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝<VAR>inst✝¹² : Algebra Rₘ Sₘ✝<VAR>inst✝¹¹ : Algebra R Sₘ✝<VAR>inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝<VAR>inst✝⁹ : IsScalarTower R S Sₘ✝<VAR>Sₘ : Type u_5<VAR>inst✝⁸ : CommRing Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : Algebra R Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>ι : Type u_6<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<VAR>this✝ : Module.Finite R S<VAR>this : Module.Free R S<VAR>i j : ι<GOAL>(trace Rₘ Sₘ) ((algebraMap S Sₘ) (b i * b j)) = (algebraMap R Rₘ) ((trace R S) (b i * b j))
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<GOAL>𝓤 (α × β) = map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : b⁻¹ * a = c<GOAL>a = b * c
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝² : HasLimitsOfShape J C<VAR>G : J ⥤ C<VAR>α : F ⟶ G<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasLimitsOfShape J D<VAR>H : C ⥤ D<VAR>j✝ : J<GOAL>(H.map (limMap α) ≫ post G H) ≫ π (G ⋙ H) j✝ = (post F H ≫ limMap (whiskerRight α H)) ≫ π (G ⋙ H) j✝
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>M' : Submodule R S<VAR>h : M' ≤ M<VAR>inst✝ : Module.Flat R ↥N<VAR>i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)<GOAL>M'.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>M' : Submodule R S<VAR>h : M' ≤ M<VAR>inst✝ : Module.Flat R ↥N<VAR>i : ↥M' ⊗[R] ↥N →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (inclusion h)<VAR>hi : Function.Injective ⇑i<GOAL>M'.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q✝ p q : MvPolynomial σ R<GOAL>(p * q).degrees ≤ p.degrees + q.degrees
<VAR>X : Scheme<VAR>U V : X.Opens<VAR>h : U = V<VAR>W : (Spec Γ(X, V)).Opens<GOAL>Hom.app (Spec.map (X.presheaf.map (eqToHom h).op)) W = eqToHom ⋯
<VAR>X : Scheme<VAR>U V : X.Opens<VAR>h : U = V<VAR>W : (Spec Γ(X, V)).Opens<VAR>this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))<GOAL>Hom.app (Spec.map (X.presheaf.map (eqToHom h).op)) W = eqToHom ⋯
<VAR>X : Scheme<VAR>U : X.Opens<VAR>this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))<VAR>W : (Spec Γ(X, U)).Opens<GOAL>Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) W = eqToHom ⋯
<VAR>X : Scheme<VAR>U : X.Opens<VAR>this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))<VAR>W : (Spec Γ(X, U)).Opens<GOAL>Hom.app (𝟙 (Scheme.Spec.obj (op Γ(X, U)))) W ≫ (Scheme.Spec.obj (op Γ(X, U))).presheaf.map (eqToHom ⋯).op = eqToHom ⋯
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>W.addX P Q / addZ P Q ^ 2 = W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b = b ↔ a = ⊥
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a✝ b✝ c a b : G<GOAL>a * (a⁻¹ * b) = b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>((∑ i ∈ s, f i) / ↑s.card) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑s.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>f : ι → α<GOAL>((∑ i ∈ ∅, f i) / ↑∅.card) ^ 2 ≤ (∑ i ∈ ∅, f i ^ 2) / ↑∅.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : s.Nonempty<GOAL>((∑ i ∈ s, f i) / ↑s.card) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑s.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : 0 < ↑s.card<GOAL>((∑ i ∈ s, f i) / ↑s.card) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑s.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : 0 < ↑s.card<GOAL>(∑ i ∈ s, f i) ^ 2 * ↑s.card ≤ (↑s.card * ∑ i ∈ s, f i ^ 2) * ↑s.card
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>s : Set (SimpleGraph V)<VAR>G : SimpleGraph V<VAR>hG : G ∈ s<GOAL>(∀ G ∈ s, G.Adj a b) → a ≠ b
<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>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : 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>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : 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 : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<GOAL>((f ⋆[L, ν] g) ⋆[L₂, μ] k) x₀ = (f ⋆[L₃, ν] g ⋆[L₄, μ] k) 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>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : 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>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : 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 : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<GOAL>Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
<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>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : 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>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : 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 : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<GOAL>Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
<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>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : 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>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : 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 : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν<GOAL>Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
<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>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : 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>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : 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 : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν<VAR>h3 : Measure.map (fun z => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν<GOAL>Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
<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>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : 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>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : 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 : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν<VAR>h3 : Measure.map (fun z => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν<GOAL>Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)
<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>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : 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>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : 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 : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν<VAR>h3 : Measure.map (fun z => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν<GOAL>(∀ᵐ (y : G) ∂ν, Integrable (fun x => uncurry (fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (x, y)) μ) ∧ Integrable (fun y => ∫ (x : G), ‖uncurry (fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (x, y)‖ ∂μ) ν
<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>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : 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>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : 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 : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν<VAR>h3 : Measure.map (fun z => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν<GOAL>Integrable (fun y => ∫ (x : G), ‖uncurry (fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (x, y)‖ ∂μ) ν