ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₀ f₁ : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : f₀ x = f₁ x<GOAL>HasFDerivWithinAt f₀ f' s x ↔ HasFDerivWithinAt f₁ f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₀ f₁ : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : x ∈ s<GOAL>HasFDerivWithinAt f₀ f' s x ↔ HasFDerivWithinAt f₁ f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₀ f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : f₀ x = f₁ x<GOAL>DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₀ f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : x ∈ s<GOAL>DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>h : HasFDerivWithinAt f f' s x<VAR>ht : Set.EqOn f₁ f t<VAR>hx : f₁ x = f x<VAR>h₁ : t ⊆ s<GOAL>HasFDerivWithinAt f₁ f' t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hs : Set.EqOn f₁ f s<VAR>hx : f₁ x = f x<GOAL>HasFDerivWithinAt f₁ f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hs : Set.EqOn f₁ f s<VAR>hx : x ∈ s<GOAL>HasFDerivWithinAt f₁ f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt f f' s x<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>HasFDerivWithinAt f₁ f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivAt f f' x<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>HasFDerivAt f₁ f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>s t : Set E<VAR>h : DifferentiableWithinAt 𝕜 f s x<VAR>ht : Set.EqOn f₁ f t<VAR>hx : f₁ x = f x<VAR>h₁ : t ⊆ s<GOAL>DifferentiableWithinAt 𝕜 f₁ t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableWithinAt 𝕜 f s x<VAR>ht : ∀ x ∈ s, f₁ x = f x<VAR>hx : f₁ x = f 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 : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableWithinAt 𝕜 f s x<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f 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 : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>s t : Set E<VAR>h : DifferentiableOn 𝕜 f s<VAR>h' : ∀ x ∈ t, f₁ x = f x<VAR>h₁ : t ⊆ s<GOAL>DifferentiableOn 𝕜 f₁ t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>s : Set E<VAR>h : DifferentiableOn 𝕜 f s<VAR>h' : ∀ x ∈ s, f₁ x = f x<GOAL>DifferentiableOn 𝕜 f₁ s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>s : Set E<VAR>h' : ∀ x ∈ s, f₁ x = f x<GOAL>DifferentiableOn 𝕜 f₁ s ↔ DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>h : DifferentiableAt 𝕜 f x<VAR>hL : f₁ =ᶠ[𝓝 x] f<GOAL>DifferentiableAt 𝕜 f₁ x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>s t : Set E<VAR>h : DifferentiableWithinAt 𝕜 f s x<VAR>hs : Set.EqOn f₁ f t<VAR>hx : f₁ x = f x<VAR>hxt : UniqueDiffWithinAt 𝕜 t x<VAR>h₁ : t ⊆ s<GOAL>fderivWithin 𝕜 f₁ t x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>hs : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>s t : Set E<VAR>hs : f₁ =ᶠ[𝓝[s] x] f<VAR>ht : t ⊆ s<GOAL>fderivWithin 𝕜 f₁ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 f t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>hs : f₁ =ᶠ[𝓝[s] x] f<GOAL>fderivWithin 𝕜 f₁ s =ᶠ[𝓝[s] x] fderivWithin 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>h : f₁ =ᶠ[𝓝 x] f<GOAL>fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>hs : Set.EqOn f₁ f s<VAR>hx : f₁ x = f x<GOAL>fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>s : Set E<VAR>hs : Set.EqOn f₁ f s<VAR>hx : x ∈ s<GOAL>fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>h : f₁ =ᶠ[𝓝 x] f<GOAL>fderiv 𝕜 f₁ x = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>x : E<VAR>h : f₁ =ᶠ[𝓝 x] f<GOAL>fderiv 𝕜 f₁ =ᶠ[𝓝 x] fderiv 𝕜 f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>HasStrictFDerivAt id (ContinuousLinearMap.id 𝕜 E) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>L : Filter E<GOAL>HasFDerivAtFilter id (ContinuousLinearMap.id 𝕜 E) x L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<GOAL>HasFDerivWithinAt id (ContinuousLinearMap.id 𝕜 E) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>HasFDerivAt id (ContinuousLinearMap.id 𝕜 E) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>DifferentiableAt 𝕜 id x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>DifferentiableAt 𝕜 (fun x => x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<GOAL>DifferentiableWithinAt 𝕜 id s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>Differentiable 𝕜 id
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>Differentiable 𝕜 fun x => x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>DifferentiableOn 𝕜 id s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>fderiv 𝕜 id x = ContinuousLinearMap.id 𝕜 E
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>fderiv 𝕜 (fun x => x) x = ContinuousLinearMap.id 𝕜 E
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 id s x = ContinuousLinearMap.id 𝕜 E
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => x) s x = ContinuousLinearMap.id 𝕜 E
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>c : F<VAR>x : E<GOAL>HasStrictFDerivAt (fun x => c) 0 x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>c : F<VAR>x : E<VAR>L : Filter E<GOAL>HasFDerivAtFilter (fun x => c) 0 x L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>c : F<VAR>x : E<VAR>s : Set E<GOAL>HasFDerivWithinAt (fun x => c) 0 s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>c : F<VAR>x : E<GOAL>HasFDerivAt (fun x => c) 0 x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>c : F<GOAL>DifferentiableAt 𝕜 (fun x => c) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>c : F<GOAL>DifferentiableWithinAt 𝕜 (fun x => c) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>c : F<GOAL>fderiv 𝕜 (fun x => c) x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>c : F<GOAL>(fderiv 𝕜 fun x => c) = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>c : F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => c) s x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>c : F<GOAL>Differentiable 𝕜 fun x => c
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>c : F<GOAL>DifferentiableOn 𝕜 (fun x => c) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<GOAL>HasFDerivWithinAt f 0 {x} x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>h : Subsingleton E<VAR>f : E → F<VAR>x : E<GOAL>HasFDerivAt f 0 x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>DifferentiableOn 𝕜 f ∅
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<GOAL>DifferentiableOn 𝕜 f {x}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>hs : s.Subsingleton<GOAL>DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>c : F<VAR>hf : f =ᶠ[𝓝 x] fun x => c<GOAL>HasFDerivAt f 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : x ∉ tsupport f<GOAL>HasStrictFDerivAt f 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : x ∉ tsupport f<GOAL>HasFDerivAt f 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : x ∉ tsupport f<GOAL>HasFDerivWithinAt f 0 s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : x ∉ tsupport f<GOAL>fderiv 𝕜 f x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>Function.support (fderiv 𝕜 f) ⊆ tsupport f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>tsupport (fderiv 𝕜 f) ⊆ tsupport f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>hf : HasCompactSupport f<GOAL>HasCompactSupport (fderiv 𝕜 f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>hf : HasCompactSupport f<VAR>v : E<GOAL>HasCompactSupport fun x => (fderiv 𝕜 f x) v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<GOAL>HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<GOAL>∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
<VAR>c : ℂ<VAR>r : ℝ<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<VAR>f : ℂ → ℂ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<GOAL>∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ENNReal<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<GOAL>HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ENNReal<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<GOAL>∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
<VAR>c : ℂ<VAR>r : ENNReal<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<VAR>f : ℂ → ℂ<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<GOAL>∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>hf : Differentiable ℂ f<VAR>c z : ℂ<GOAL>HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>hf : Differentiable ℂ f<VAR>c z : ℂ<GOAL>∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
<VAR>c z : ℂ<VAR>f : ℂ → ℂ<VAR>hf : Differentiable ℂ f<GOAL>∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
<VAR>x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>InnerProductGeometry.angle x y = |(x / y).arg|
<VAR>y : ℂ<VAR>hy : y ≠ 0<GOAL>InnerProductGeometry.angle 1 y = |y.arg|
<VAR>x : ℂ<VAR>hx : x ≠ 0<GOAL>InnerProductGeometry.angle x 1 = |x.arg|
<VAR>a : ℂ<VAR>ha : a ≠ 0<VAR>x y : ℂ<GOAL>InnerProductGeometry.angle (a * x) (a * y) = InnerProductGeometry.angle x y
<VAR>a : ℂ<VAR>ha : a ≠ 0<VAR>x y : ℂ<GOAL>InnerProductGeometry.angle (x * a) (y * a) = InnerProductGeometry.angle x y
<VAR>a x y : ℂ<GOAL>InnerProductGeometry.angle (x / a) y = InnerProductGeometry.angle x (y * a)
<VAR>a x y : ℂ<GOAL>InnerProductGeometry.angle x (y / a) = InnerProductGeometry.angle (x * a) y
<VAR>x y : ℝ<GOAL>InnerProductGeometry.angle (Complex.exp (↑x * Complex.I)) (Complex.exp (↑y * Complex.I)) = |toIocMod Real.two_pi_pos (-π) (x - y)|
<VAR>x : ℝ<GOAL>InnerProductGeometry.angle (Complex.exp (↑x * Complex.I)) 1 = |toIocMod Real.two_pi_pos (-π) x|
<VAR>x y : ℂ<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<GOAL>‖x - y‖ ∈ Set.Icc (2 / π * InnerProductGeometry.angle x y) (InnerProductGeometry.angle x y)
<VAR>x y : ℂ<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<GOAL>‖x - y‖ ≤ InnerProductGeometry.angle x y
<VAR>x y : ℂ<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<GOAL>2 / π * InnerProductGeometry.angle x y ≤ ‖x - y‖
<VAR>x y : ℂ<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<GOAL>InnerProductGeometry.angle x y ≤ π / 2 * ‖x - y‖
<VAR>s t : Set ℝ<GOAL>(convexHull ℝ) (s ×ℂ t) = (convexHull ℝ) s ×ℂ (convexHull ℝ) t
<VAR>z : ℂ<VAR>hz : 0 < z<GOAL>StarConvex ℝ z Complex.slitPlane
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>StarConvex ℝ (↑x) Complex.slitPlane
<GOAL>StarConvex ℝ 1 Complex.slitPlane
<VAR>x : ℝ<GOAL>HasDerivAt (fun x => ↑(𝐞 x)) (2 * ↑π * Complex.I * ↑(𝐞 x)) x
<GOAL>Differentiable ℝ fun x => ↑(𝐞 x)
<VAR>x : ℝ<GOAL>deriv (fun x => ↑(𝐞 x)) x = 2 * ↑π * Complex.I * ↑(𝐞 x)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<VAR>w : W<GOAL>HasFDerivAt (fun w => ↑(𝐞 (-(L v) w))) ((-2 * ↑π * Complex.I * ↑(𝐞 (-(L v) w))) • Complex.ofRealCLM.comp (L v)) w
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<VAR>w y : W<GOAL>(fderiv ℝ (fun w => ↑(𝐞 (-(L v) w))) w) y = -2 * ↑π * Complex.I * ↑((L v) y) * ↑(𝐞 (-(L v) w))
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<GOAL>Differentiable ℝ fun w => ↑(𝐞 (-(L v) w))
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<VAR>w : W<GOAL>HasFDerivAt (fun v => ↑(𝐞 (-(L v) w))) ((-2 * ↑π * Complex.I * ↑(𝐞 (-(L v) w))) • Complex.ofRealCLM.comp (L.flip w)) v
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v y : V<VAR>w : W<GOAL>(fderiv ℝ (fun v => ↑(𝐞 (-(L v) w))) v) y = -2 * ↑π * Complex.I * ↑((L y) w) * ↑(𝐞 (-(L v) w))
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>w : W<GOAL>Differentiable ℝ fun v => ↑(𝐞 (-(L v) w))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>w : W<GOAL>(VectorFourier.fourierSMulRight L f v) w = -(2 * ↑π * Complex.I) • (L v) w • f v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<VAR>w : W<GOAL>HasFDerivAt (fun w' => 𝐞 (-(L v) w') • f v) (𝐞 (-(L v) w) • VectorFourier.fourierSMulRight L f v) w
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<GOAL>‖VectorFourier.fourierSMulRight L f v‖ = 2 * π * ‖L v‖ * ‖f v‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<GOAL>‖VectorFourier.fourierSMulRight L f v‖ ≤ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>SecondCountableTopologyEither V (W →L[ℝ] ℝ)<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>μ : MeasureTheory.Measure V<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun v => VectorFourier.fourierSMulRight L f v) μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedAddCommGroup W<VAR>NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>SecondCountableTopology V<VAR>μ : MeasureTheory.Measure V<VAR>hf : MeasureTheory.Integrable f μ<VAR>hf' : MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) μ<VAR>w : W<GOAL>HasFDerivAt (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f) (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ (VectorFourier.fourierSMulRight L f) w) w