ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<GOAL>HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[precompR G L, μ] fderiv 𝕜 g) x₀) 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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<GOAL>HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[precompR G L, μ] fderiv 𝕜 g) x₀) 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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<GOAL>HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L', μ] fderiv 𝕜 g) x₀) 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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<VAR>h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ<GOAL>HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L', μ] fderiv 𝕜 g) x₀) 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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<VAR>h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ<VAR>h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ<GOAL>HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L', μ] fderiv 𝕜 g) x₀) 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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<VAR>h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ<VAR>h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ<VAR>h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x<GOAL>HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L', μ] fderiv 𝕜 g) x₀) 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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<VAR>h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ<VAR>h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ<VAR>h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x<VAR>K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1<GOAL>HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L', μ] fderiv 𝕜 g) x₀) 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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<VAR>h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ<VAR>h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ<VAR>h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x<VAR>K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1<VAR>hK' : IsCompact K'<GOAL>HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L', μ] fderiv 𝕜 g) x₀) 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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<VAR>h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ<VAR>h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ<VAR>h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x<VAR>K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1<VAR>hK' : IsCompact K'<GOAL>∀ᵐ (a : G) ∂μ, ∀ x ∈ ball x₀ 1, ‖(L' (f a)) (fderiv 𝕜 g (x - a))‖ ≤ ?m.1390320 a
<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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<VAR>h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ<VAR>h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ<VAR>h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x<VAR>K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1<VAR>hK' : IsCompact K'<GOAL>Integrable ?m.1390320 μ
<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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<VAR>h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ<VAR>h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ<VAR>h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x<VAR>K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1<VAR>hK' : IsCompact K'<GOAL>∀ᵐ (a : G) ∂μ, ∀ x ∈ ball x₀ 1, HasFDerivAt (fun x => (L (f a)) (g (x - a))) ((L' (f a)) (fderiv 𝕜 g (x - a))) 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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<VAR>h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ<VAR>h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ<VAR>h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x<VAR>K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1<VAR>hK' : IsCompact K'<GOAL>G → ℝ
<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 G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<VAR>fin_dim : FiniteDimensional 𝕜 G<VAR>this : ProperSpace G<VAR>L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L<VAR>h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ<VAR>h2 : ∀ (x : G), AEStronglyMeasurable (fun t => (L' (f t)) (fderiv 𝕜 g (x - t))) μ<VAR>h3 : ∀ (x t : G), HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x<VAR>K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1<VAR>hK' : IsCompact K'<GOAL>Integrable (fun t => (L (f t)) (g (x₀ - t))) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L✝ : CompleteSublattice α<VAR>L : CompleteSublattice β<VAR>s : Set α<VAR>hs : s ⊆ { carrier := ⇑f ⁻¹' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier<GOAL>sSup s ∈ { carrier := ⇑f ⁻¹' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L✝ : CompleteSublattice α<VAR>L : CompleteSublattice β<VAR>s : Set α<VAR>hs : s ⊆ { carrier := ⇑f ⁻¹' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier<GOAL>sInf s ∈ { carrier := ⇑f ⁻¹' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>f : ↥(lp (fun i => 𝕜) 2)<GOAL>HasSum (fun i => ↑f i • (fun i => b.repr.symm (lp.single 2 i 1)) i) (b.repr.symm f)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>f : ↥(lp (fun i => 𝕜) 2)<GOAL>(fun i => ↑f i • (fun i => b.repr.symm (lp.single 2 i 1)) i) = fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>f : ↥(lp (fun i => 𝕜) 2)<VAR>i : ι<GOAL>↑f i • (fun i => b.repr.symm (lp.single 2 i 1)) i = b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>f : ↥(lp (fun i => 𝕜) 2)<VAR>i : ι<GOAL>b.repr (↑f i • (fun i => b.repr.symm (lp.single 2 i 1)) i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>f : ↥(lp (fun i => 𝕜) 2)<VAR>i : ι<VAR>this : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance<GOAL>b.repr (↑f i • (fun i => b.repr.symm (lp.single 2 i 1)) i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>f : ↥(lp (fun i => 𝕜) 2)<VAR>i : ι<VAR>this✝ : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance<VAR>this : lp.single 2 i (↑f i * 1) = ↑f i • lp.single 2 i 1<GOAL>b.repr (↑f i • (fun i => b.repr.symm (lp.single 2 i 1)) i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>f : ↥(lp (fun i => 𝕜) 2)<VAR>i : ι<VAR>this✝ : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance<VAR>this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1<GOAL>b.repr (↑f i • (fun i => b.repr.symm (lp.single 2 i 1)) i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>f : ↥(lp (fun i => 𝕜) 2)<VAR>i : ι<VAR>this✝ : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance<VAR>this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1<GOAL>lp.single 2 i (↑f i) = b.repr (b.repr.symm ((fun i => lp.single 2 i (↑f i)) i))
<VAR>a b c : Ordinal.{u}<VAR>f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}<VAR>hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj<GOAL>(a ♯ b).blsub f = max (a.blsub fun a' ha' => f (a' ♯ b) ⋯) (b.blsub fun b' hb' => f (a ♯ b') ⋯)
<VAR>a b c : Ordinal.{u}<VAR>f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}<VAR>hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj<GOAL>∀ (i : Ordinal.{u}) (h : i < a ♯ b), f i h < max (a.blsub fun a' ha' => f (a' ♯ b) ⋯) (b.blsub fun b' hb' => f (a ♯ b') ⋯)
<VAR>a b c : Ordinal.{u}<VAR>f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}<VAR>hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj<GOAL>(a.blsub fun a' ha' => f (a' ♯ b) ⋯) ≤ (a ♯ b).blsub f
<VAR>a b c : Ordinal.{u}<VAR>f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}<VAR>hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj<GOAL>(b.blsub fun b' hb' => f (a ♯ b') ⋯) ≤ (a ♯ b).blsub f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hx : x ∈ periodicPts f<GOAL>0 < minimalPeriod f x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a : R<VAR>a0 : a ≠ 0<VAR>n : ℤ<GOAL>(C a * T n).support = {n}
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a : R<VAR>a0 : a ≠ 0<VAR>n : ℤ<GOAL>(Finsupp.single n a).support = {n}
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<GOAL>∀ {a₁ b₁ a₂ b₂ : α}, Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>AnalyticWithinOn 𝕜 f s ↔ AnalyticOn 𝕜 f s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>AnalyticWithinOn 𝕜 f s → AnalyticOn 𝕜 f s