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>P : Type uP<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace G<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup P<VAR>NormedSpace 𝕜 P<VAR>μ : MeasureTheory.Measure G<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)
<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>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace G<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup P<VAR>NormedSpace 𝕜 P<VAR>μ : MeasureTheory.Measure G<VAR>n : ℕ∞<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>s : Set P<VAR>v : P → G<VAR>hv : ContDiffOn 𝕜 n v s<VAR>f : G → E<VAR>g : P → G → E'<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 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>P : Type uP<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace G<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup P<VAR>NormedSpace 𝕜 P<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>L : E' →L[𝕜] E →L[𝕜] F<VAR>f : G → E<VAR>n : ℕ∞<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 (g q.1) f 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>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace G<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>NormedSpace 𝕜 G<VAR>NormedAddCommGroup P<VAR>NormedSpace 𝕜 P<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>L : E' →L[𝕜] E →L[𝕜] F<VAR>s : Set P<VAR>n : ℕ∞<VAR>v : P → G<VAR>hv : ContDiffOn 𝕜 n v s<VAR>f : G → E<VAR>g : P → G → E'<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 x => MeasureTheory.convolution (g x) f 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>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace G<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>NormedSpace 𝕜 G<VAR>μ : MeasureTheory.Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>n : ℕ∞<VAR>hcg : HasCompactSupport g<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n (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>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 E'<VAR>NormedSpace ℝ F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>MeasurableSpace G<VAR>NormedAddCommGroup G<VAR>BorelSpace G<VAR>NormedSpace 𝕜 G<VAR>μ : MeasureTheory.Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>μ.IsAddLeftInvariant<VAR>μ.IsNegInvariant<VAR>n : ℕ∞<VAR>hcf : HasCompactSupport f<VAR>hf : ContDiff 𝕜 n f<VAR>hg : MeasureTheory.LocallyIntegrable g μ<GOAL>ContDiff 𝕜 n (MeasureTheory.convolution f g L μ)
<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ E'<VAR>NormedSpace ℝ F<VAR>f : ℝ → E<VAR>g : ℝ → E'<VAR>L : E →L[ℝ] E' →L[ℝ] F<VAR>ν : MeasureTheory.Measure ℝ := by volume_tac<VAR>MeasureTheory.NoAtoms ν<GOAL>MeasureTheory.posConvolution f g L ν = MeasureTheory.convolution ((Set.Ioi 0).indicator f) ((Set.Ioi 0).indicator g) L ν
<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ E'<VAR>NormedSpace ℝ F<VAR>f : ℝ → E<VAR>g : ℝ → E'<VAR>μ ν : MeasureTheory.Measure ℝ<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>μ.IsAddRightInvariant<VAR>MeasureTheory.NoAtoms ν<VAR>hf : MeasureTheory.IntegrableOn f (Set.Ioi 0) ν<VAR>hg : MeasureTheory.IntegrableOn g (Set.Ioi 0) μ<VAR>L : E →L[ℝ] E' →L[ℝ] F<GOAL>MeasureTheory.Integrable (MeasureTheory.posConvolution f g L ν) μ
<VAR>E : Type uE<VAR>E' : Type uE'<VAR>F : Type uF<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ E'<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>CompleteSpace E'<VAR>μ ν : MeasureTheory.Measure ℝ<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>μ.IsAddRightInvariant<VAR>MeasureTheory.NoAtoms ν<VAR>f : ℝ → E<VAR>g : ℝ → E'<VAR>hf : MeasureTheory.IntegrableOn f (Set.Ioi 0) ν<VAR>hg : MeasureTheory.IntegrableOn g (Set.Ioi 0) μ<VAR>L : E →L[ℝ] E' →L[ℝ] F<GOAL>∫ (x : ℝ) in Set.Ioi 0, ∫ (t : ℝ) in 0 ..x, (L (f t)) (g (x - t)) ∂ν ∂μ = (L (∫ (x : ℝ) in Set.Ioi 0, f x ∂ν)) (∫ (x : ℝ) in Set.Ioi 0, g x ∂μ)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>f : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f' : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<GOAL>LinearMap.range (f'.prod φ') ≠ ⊤
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>f : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f' : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<GOAL>∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>φ' : E →L[ℝ] ℝ<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<GOAL>∃ a b, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>Fintype ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<GOAL>∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>Finite ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<GOAL>¬LinearIndependent ℝ (Option.elim' φ' f')
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>x : ι → 𝕜<VAR>i : ι<VAR>y : 𝕜<GOAL>HasDerivAt (Function.update x i) (Pi.single i 1) y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>i : ι<VAR>y : 𝕜<GOAL>HasDerivAt (Pi.single i) (Pi.single i 1) y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>x : ι → 𝕜<VAR>i : ι<VAR>y : 𝕜<GOAL>deriv (Function.update x i) y = Pi.single i 1
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>i : ι<VAR>y : 𝕜<GOAL>deriv (Pi.single i) y = Pi.single i 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>x : 𝕜<VAR>h : x ≠ 0 ∨ 0 ≤ m<GOAL>HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>x : 𝕜<VAR>h : x ≠ 0 ∨ 0 ≤ m<GOAL>HasDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>x : 𝕜<VAR>h : x ≠ 0 ∨ 0 ≤ m<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt (fun x => x ^ m) (↑m * x ^ (m - 1)) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>m : ℤ<GOAL>DifferentiableAt 𝕜 (fun x => x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>s : Set 𝕜<VAR>m : ℤ<VAR>x : 𝕜<VAR>h : x ≠ 0 ∨ 0 ≤ m<GOAL>DifferentiableWithinAt 𝕜 (fun x => x ^ m) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>s : Set 𝕜<VAR>h : 0 ∉ s ∨ 0 ≤ m<GOAL>DifferentiableOn 𝕜 (fun x => x ^ m) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>x : 𝕜<GOAL>deriv (fun x => x ^ m) x = ↑m * x ^ (m - 1)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>m : ℤ<GOAL>(deriv fun x => x ^ m) = fun x => ↑m * x ^ (m - 1)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>m : ℤ<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>h : x ≠ 0 ∨ 0 ≤ m<GOAL>derivWithin (fun x => x ^ m) s x = ↑m * x ^ (m - 1)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>k : ℕ<GOAL>(deriv^[k] fun x => x ^ m) = fun x => (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>m : ℤ<VAR>x : 𝕜<VAR>k : ℕ<GOAL>deriv^[k] (fun y => y ^ m) x = (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<VAR>x : 𝕜<VAR>k : ℕ<GOAL>deriv^[k] (fun x => x ^ n) x = (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ (n - k)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>n k : ℕ<GOAL>(deriv^[k] fun x => x ^ n) = fun x => (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ (n - k)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>k : ℕ<VAR>x : 𝕜<GOAL>deriv^[k] Inv.inv x = (∏ i ∈ Finset.range k, (-1 - ↑i)) * x ^ (-1 - ↑k)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>k : ℕ<GOAL>deriv^[k] Inv.inv = fun x => (∏ i ∈ Finset.range k, (-1 - ↑i)) * x ^ (-1 - ↑k)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>m : ℤ<VAR>f : E → 𝕜<VAR>t : Set E<VAR>a : E<VAR>hf : DifferentiableWithinAt 𝕜 f t a<VAR>h : f a ≠ 0 ∨ 0 ≤ m<GOAL>DifferentiableWithinAt 𝕜 (fun x => f x ^ m) t a
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>m : ℤ<VAR>f : E → 𝕜<VAR>a : E<VAR>hf : DifferentiableAt 𝕜 f a<VAR>h : f a ≠ 0 ∨ 0 ≤ m<GOAL>DifferentiableAt 𝕜 (fun x => f x ^ m) a
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>m : ℤ<VAR>f : E → 𝕜<VAR>t : Set E<VAR>hf : DifferentiableOn 𝕜 f t<VAR>h : (∀ x ∈ t, f x ≠ 0) ∨ 0 ≤ m<GOAL>DifferentiableOn 𝕜 (fun x => f x ^ m) t
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>m : ℤ<VAR>f : E → 𝕜<VAR>hf : Differentiable 𝕜 f<VAR>h : (∀ (x : E), f x ≠ 0) ∨ 0 ≤ m<GOAL>Differentiable 𝕜 fun x => f x ^ m
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₁ : 𝕜 → F<VAR>f₁' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>G : Type w<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₂ : 𝕜 → G<VAR>f₂' : G<VAR>hf₁ : HasDerivAtFilter f₁ f₁' x L<VAR>hf₂ : HasDerivAtFilter f₂ f₂' x L<GOAL>HasDerivAtFilter (fun x => (f₁ x, f₂ x)) (f₁', f₂') x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₁ : 𝕜 → F<VAR>f₁' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>G : Type w<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₂ : 𝕜 → G<VAR>f₂' : G<VAR>hf₁ : HasDerivWithinAt f₁ f₁' s x<VAR>hf₂ : HasDerivWithinAt f₂ f₂' s x<GOAL>HasDerivWithinAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₁ : 𝕜 → F<VAR>f₁' : F<VAR>x : 𝕜<VAR>G : Type w<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₂ : 𝕜 → G<VAR>f₂' : G<VAR>hf₁ : HasDerivAt f₁ f₁' x<VAR>hf₂ : HasDerivAt f₂ f₂' x<GOAL>HasDerivAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₁ : 𝕜 → F<VAR>f₁' : F<VAR>x : 𝕜<VAR>G : Type w<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f₂ : 𝕜 → G<VAR>f₂' : G<VAR>hf₁ : HasStrictDerivAt f₁ f₁' x<VAR>hf₂ : HasStrictDerivAt f₂ f₂' x<GOAL>HasStrictDerivAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>ι : Type u_1<VAR>Fintype ι<VAR>E' : ι → Type u_2<VAR>(i : ι) → NormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>φ : 𝕜 → (i : ι) → E' i<VAR>φ' : (i : ι) → E' i<GOAL>HasStrictDerivAt φ φ' x ↔ ∀ (i : ι), HasStrictDerivAt (fun x => φ x i) (φ' i) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>ι : Type u_1<VAR>Fintype ι<VAR>E' : ι → Type u_2<VAR>(i : ι) → NormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>φ : 𝕜 → (i : ι) → E' i<VAR>φ' : (i : ι) → E' i<GOAL>HasDerivAtFilter φ φ' x L ↔ ∀ (i : ι), HasDerivAtFilter (fun x => φ x i) (φ' i) x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>ι : Type u_1<VAR>Fintype ι<VAR>E' : ι → Type u_2<VAR>(i : ι) → NormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>φ : 𝕜 → (i : ι) → E' i<VAR>φ' : (i : ι) → E' i<GOAL>HasDerivAt φ φ' x ↔ ∀ (i : ι), HasDerivAt (fun x => φ x i) (φ' i) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>ι : Type u_1<VAR>Fintype ι<VAR>E' : ι → Type u_2<VAR>(i : ι) → NormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>φ : 𝕜 → (i : ι) → E' i<VAR>φ' : (i : ι) → E' i<GOAL>HasDerivWithinAt φ φ' s x ↔ ∀ (i : ι), HasDerivWithinAt (fun x => φ x i) (φ' i) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>ι : Type u_1<VAR>Fintype ι<VAR>E' : ι → Type u_2<VAR>(i : ι) → NormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>φ : 𝕜 → (i : ι) → E' i<VAR>h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => φ x i) s x<VAR>hs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>ι : Type u_1<VAR>Fintype ι<VAR>E' : ι → Type u_2<VAR>(i : ι) → NormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>φ : 𝕜 → (i : ι) → E' i<VAR>h : ∀ (i : ι), DifferentiableAt 𝕜 (fun x => φ x i) x<GOAL>deriv φ x = fun i => deriv (fun x => φ x i) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>e : 𝕜 →L[𝕜] F<GOAL>HasDerivAtFilter (⇑e) (e 1) x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>e : 𝕜 →L[𝕜] F<GOAL>HasStrictDerivAt (⇑e) (e 1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>e : 𝕜 →L[𝕜] F<GOAL>HasDerivAt (⇑e) (e 1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>e : 𝕜 →L[𝕜] F<GOAL>HasDerivWithinAt (⇑e) (e 1) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>e : 𝕜 →L[𝕜] F<GOAL>deriv (⇑e) x = e 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>e : 𝕜 →L[𝕜] F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (⇑e) s x = e 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>e : 𝕜 →ₗ[𝕜] F<GOAL>HasDerivAtFilter (⇑e) (e 1) x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>e : 𝕜 →ₗ[𝕜] F<GOAL>HasStrictDerivAt (⇑e) (e 1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>e : 𝕜 →ₗ[𝕜] F<GOAL>HasDerivAt (⇑e) (e 1) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>e : 𝕜 →ₗ[𝕜] F<GOAL>HasDerivWithinAt (⇑e) (e 1) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>e : 𝕜 →ₗ[𝕜] F<GOAL>deriv (⇑e) x = e 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>e : 𝕜 →ₗ[𝕜] F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (⇑e) s x = e 1
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<VAR>x : 𝕜<GOAL>HasStrictDerivAt (fun x => x ^ n) (↑n * x ^ (n - 1)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<VAR>x : 𝕜<GOAL>HasDerivAt (fun x => x ^ n) (↑n * x ^ (n - 1)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt (fun x => x ^ n) (↑n * x ^ (n - 1)) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>n : ℕ<GOAL>DifferentiableAt 𝕜 (fun x => x ^ n) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>n : ℕ<GOAL>DifferentiableWithinAt 𝕜 (fun x => x ^ n) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<GOAL>Differentiable 𝕜 fun x => x ^ n
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>s : Set 𝕜<VAR>n : ℕ<GOAL>DifferentiableOn 𝕜 (fun x => x ^ n) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>n : ℕ<GOAL>deriv (fun x => x ^ n) x = ↑n * x ^ (n - 1)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ<GOAL>(deriv fun x => x ^ n) = fun x => ↑n * x ^ (n - 1)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>n : ℕ<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => x ^ n) s x = ↑n * x ^ (n - 1)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>c : 𝕜 → 𝕜<VAR>c' : 𝕜<VAR>n : ℕ<VAR>hc : HasDerivWithinAt c c' s x<GOAL>HasDerivWithinAt (fun y => c y ^ n) (↑n * c x ^ (n - 1) * c') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>c : 𝕜 → 𝕜<VAR>c' : 𝕜<VAR>n : ℕ<VAR>hc : HasDerivAt c c' x<GOAL>HasDerivAt (fun y => c y ^ n) (↑n * c x ^ (n - 1) * c') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>c : 𝕜 → 𝕜<VAR>n : ℕ<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => c x ^ n) s x = ↑n * c x ^ (n - 1) * derivWithin c s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>c : 𝕜 → 𝕜<VAR>n : ℕ<VAR>hc : DifferentiableAt 𝕜 c x<GOAL>deriv (fun x => c x ^ n) x = ↑n * c x ^ (n - 1) * deriv c x
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>x : Unitization 𝕜 A<GOAL>(Unitization.splitMul 𝕜 A) x = (x.fst, (algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (ContinuousLinearMap.mul 𝕜 A) x.snd)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>h : Function.Injective ⇑(ContinuousLinearMap.mul 𝕜 A)<GOAL>Function.Injective ⇑(Unitization.splitMul 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<GOAL>Function.Injective ⇑(Unitization.splitMul 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖x‖ = ‖(Unitization.splitMul 𝕜 A) x‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖x‖₊ = ‖(Unitization.splitMul 𝕜 A) x‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖x‖ = ‖x.fst‖ ⊔ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (ContinuousLinearMap.mul 𝕜 A) x.snd‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖x‖₊ = ‖x.fst‖₊ ⊔ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (ContinuousLinearMap.mul 𝕜 A) x.snd‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<GOAL>LipschitzWith 2 ⇑(Unitization.addEquiv 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<GOAL>AntilipschitzWith 2 ⇑(Unitization.addEquiv 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<GOAL>uniformity (Unitization 𝕜 A) = uniformity (Unitization 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<GOAL>Bornology.cobounded (Unitization 𝕜 A) = Bornology.cobounded (Unitization 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<GOAL>UniformEmbedding ⇑(Unitization.addEquiv 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<VAR>a : A<GOAL>‖↑a‖ = ‖a‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<VAR>a : A<GOAL>‖↑a‖₊ = ‖a‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<GOAL>Isometry Unitization.inr
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<VAR>a b : A<GOAL>dist ↑a ↑b = dist a b
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>RegularNormedAlgebra 𝕜 A<VAR>a b : A<GOAL>nndist ↑a ↑b = nndist a b
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>hx : x ≠ 0<GOAL>HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>x_ne_zero : x ≠ 0<GOAL>HasDerivAt (fun y => y⁻¹) (-(x ^ 2)⁻¹) x