ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>fderivWithin ℝ (fun x => Real.cos (f x)) s x = -Real.sin (f x) • fderivWithin ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hc : DifferentiableAt ℝ f x<GOAL>fderiv ℝ (fun x => Real.cos (f x)) x = -Real.sin (f x) • fderiv ℝ f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>h : ContDiff ℝ n f<GOAL>ContDiff ℝ n fun x => Real.cos (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<GOAL>ContDiffAt ℝ n (fun x => Real.cos (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<GOAL>ContDiffOn ℝ n (fun x => Real.cos (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<GOAL>ContDiffWithinAt ℝ n (fun x => Real.cos (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => Real.sin (f x)) (Real.cos (f x) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<GOAL>DifferentiableWithinAt ℝ (fun x => Real.sin (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hc : DifferentiableAt ℝ f x<GOAL>DifferentiableAt ℝ (fun x => Real.sin (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>hc : DifferentiableOn ℝ f s<GOAL>DifferentiableOn ℝ (fun x => Real.sin (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>hc : Differentiable ℝ f<GOAL>Differentiable ℝ fun x => Real.sin (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>fderivWithin ℝ (fun x => Real.sin (f x)) s x = Real.cos (f x) • fderivWithin ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hc : DifferentiableAt ℝ f x<GOAL>fderiv ℝ (fun x => Real.sin (f x)) x = Real.cos (f x) • fderiv ℝ f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>h : ContDiff ℝ n f<GOAL>ContDiff ℝ n fun x => Real.sin (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<GOAL>ContDiffAt ℝ n (fun x => Real.sin (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<GOAL>ContDiffOn ℝ n (fun x => Real.sin (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<GOAL>ContDiffWithinAt ℝ n (fun x => Real.sin (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => Real.cosh (f x)) (Real.sinh (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => Real.cosh (f x)) (Real.sinh (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => Real.cosh (f x)) (Real.sinh (f x) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<GOAL>DifferentiableWithinAt ℝ (fun x => Real.cosh (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hc : DifferentiableAt ℝ f x<GOAL>DifferentiableAt ℝ (fun x => Real.cosh (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>hc : DifferentiableOn ℝ f s<GOAL>DifferentiableOn ℝ (fun x => Real.cosh (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>hc : Differentiable ℝ f<GOAL>Differentiable ℝ fun x => Real.cosh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>fderivWithin ℝ (fun x => Real.cosh (f x)) s x = Real.sinh (f x) • fderivWithin ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hc : DifferentiableAt ℝ f x<GOAL>fderiv ℝ (fun x => Real.cosh (f x)) x = Real.sinh (f x) • fderiv ℝ f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>h : ContDiff ℝ n f<GOAL>ContDiff ℝ n fun x => Real.cosh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<GOAL>ContDiffAt ℝ n (fun x => Real.cosh (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<GOAL>ContDiffOn ℝ n (fun x => Real.cosh (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<GOAL>ContDiffWithinAt ℝ n (fun x => Real.cosh (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => Real.sinh (f x)) (Real.cosh (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => Real.sinh (f x)) (Real.cosh (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => Real.sinh (f x)) (Real.cosh (f x) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<GOAL>DifferentiableWithinAt ℝ (fun x => Real.sinh (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hc : DifferentiableAt ℝ f x<GOAL>DifferentiableAt ℝ (fun x => Real.sinh (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>hc : DifferentiableOn ℝ f s<GOAL>DifferentiableOn ℝ (fun x => Real.sinh (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>hc : Differentiable ℝ f<GOAL>Differentiable ℝ fun x => Real.sinh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>fderivWithin ℝ (fun x => Real.sinh (f x)) s x = Real.cosh (f x) • fderivWithin ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hc : DifferentiableAt ℝ f x<GOAL>fderiv ℝ (fun x => Real.sinh (f x)) x = Real.cosh (f x) • fderiv ℝ f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>h : ContDiff ℝ n f<GOAL>ContDiff ℝ n fun x => Real.sinh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<GOAL>ContDiffAt ℝ n (fun x => Real.sinh (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<GOAL>ContDiffOn ℝ n (fun x => Real.sinh (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<GOAL>ContDiffWithinAt ℝ n (fun x => Real.sinh (f x)) s x
<GOAL>polarCoord.source = {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
<GOAL>polarCoord.target = Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi
<VAR>q : ℝ × ℝ<GOAL>↑polarCoord q = (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)
<VAR>p : ℝ × ℝ<GOAL>↑polarCoord.symm p = (p.1 * Real.cos p.2, p.1 * Real.sin p.2)
<VAR>p : ℝ × ℝ<GOAL>HasFDerivAt (↑polarCoord.symm) (LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) !![Real.cos p.2, -p.1 * Real.sin p.2; Real.sin p.2, p.1 * Real.cos p.2])) p
<GOAL>polarCoord.source =ᵐ[MeasureTheory.volume] Set.univ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ × ℝ → E<GOAL>∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p) = ∫ (p : ℝ × ℝ), f p
<VAR>a : ℂ<GOAL>↑Complex.polarCoord a = (Complex.abs a, a.arg)
<GOAL>Complex.polarCoord.target = Set.Ioi 0 ×ˢ Set.Ioo (-Real.pi) Real.pi
<VAR>p : ℝ × ℝ<GOAL>↑Complex.polarCoord.symm p = ↑p.1 * (↑(Real.cos p.2) + ↑(Real.sin p.2) * Complex.I)
<VAR>p : ℝ × ℝ<GOAL>Complex.abs (↑Complex.polarCoord.symm p) = |p.1|
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℂ → E<GOAL>∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) = ∫ (p : ℂ), f p
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>h : 0 < (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasStrictFDerivAt (NormedSpace.exp 𝕂) 1 0
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>h : 0 < (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasFDerivAt (NormedSpace.exp 𝕂) 1 0
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasFDerivAt (NormedSpace.exp 𝕂) (NormedSpace.exp 𝕂 x • 1) x
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasStrictFDerivAt (NormedSpace.exp 𝕂) (NormedSpace.exp 𝕂 x • 1) x
<VAR>𝕂 : Type u_1<VAR>NontriviallyNormedField 𝕂<VAR>CompleteSpace 𝕂<VAR>CharZero 𝕂<VAR>x : 𝕂<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝕂).radius<GOAL>HasStrictDerivAt (NormedSpace.exp 𝕂) (NormedSpace.exp 𝕂 x) x
<VAR>𝕂 : Type u_1<VAR>NontriviallyNormedField 𝕂<VAR>CompleteSpace 𝕂<VAR>CharZero 𝕂<VAR>x : 𝕂<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝕂).radius<GOAL>HasDerivAt (NormedSpace.exp 𝕂) (NormedSpace.exp 𝕂 x) x
<VAR>𝕂 : Type u_1<VAR>NontriviallyNormedField 𝕂<VAR>CompleteSpace 𝕂<VAR>h : 0 < (NormedSpace.expSeries 𝕂 𝕂).radius<GOAL>HasStrictDerivAt (NormedSpace.exp 𝕂) 1 0
<VAR>𝕂 : Type u_1<VAR>NontriviallyNormedField 𝕂<VAR>CompleteSpace 𝕂<VAR>h : 0 < (NormedSpace.expSeries 𝕂 𝕂).radius<GOAL>HasDerivAt (NormedSpace.exp 𝕂) 1 0
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<GOAL>HasStrictFDerivAt (NormedSpace.exp 𝕂) 1 0
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<GOAL>HasFDerivAt (NormedSpace.exp 𝕂) 1 0
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>HasStrictFDerivAt (NormedSpace.exp 𝕂) (NormedSpace.exp 𝕂 x • 1) x
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>HasFDerivAt (NormedSpace.exp 𝕂) (NormedSpace.exp 𝕂 x • 1) x
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<VAR>x : 𝕂<GOAL>HasStrictDerivAt (NormedSpace.exp 𝕂) (NormedSpace.exp 𝕂 x) x
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<VAR>x : 𝕂<GOAL>HasDerivAt (NormedSpace.exp 𝕂) (NormedSpace.exp 𝕂 x) x
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<GOAL>HasStrictDerivAt (NormedSpace.exp 𝕂) 1 0
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<GOAL>HasDerivAt (NormedSpace.exp 𝕂) 1 0
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>NontriviallyNormedField 𝕂<VAR>CharZero 𝕂<VAR>NormedCommRing 𝕊<VAR>NormedRing 𝔸<VAR>NormedSpace 𝕂 𝕊<VAR>NormedAlgebra 𝕂 𝔸<VAR>Algebra 𝕊 𝔸<VAR>ContinuousSMul 𝕊 𝔸<VAR>IsScalarTower 𝕂 𝕊 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasFDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (NormedSpace.exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>NontriviallyNormedField 𝕂<VAR>CharZero 𝕂<VAR>NormedCommRing 𝕊<VAR>NormedRing 𝔸<VAR>NormedSpace 𝕂 𝕊<VAR>NormedAlgebra 𝕂 𝔸<VAR>Algebra 𝕊 𝔸<VAR>ContinuousSMul 𝕊 𝔸<VAR>IsScalarTower 𝕂 𝕊 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasFDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp 𝕂 (t • x))) t
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>NontriviallyNormedField 𝕂<VAR>CharZero 𝕂<VAR>NormedCommRing 𝕊<VAR>NormedRing 𝔸<VAR>NormedSpace 𝕂 𝕊<VAR>NormedAlgebra 𝕂 𝔸<VAR>Algebra 𝕊 𝔸<VAR>ContinuousSMul 𝕊 𝔸<VAR>IsScalarTower 𝕂 𝕊 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasStrictFDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (NormedSpace.exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>NontriviallyNormedField 𝕂<VAR>CharZero 𝕂<VAR>NormedCommRing 𝕊<VAR>NormedRing 𝔸<VAR>NormedSpace 𝕂 𝕊<VAR>NormedAlgebra 𝕂 𝔸<VAR>Algebra 𝕊 𝔸<VAR>ContinuousSMul 𝕊 𝔸<VAR>IsScalarTower 𝕂 𝕊 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasStrictFDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp 𝕂 (t • x))) t
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_3<VAR>NontriviallyNormedField 𝕂<VAR>CharZero 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕂<VAR>htx : t • x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasStrictDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (NormedSpace.exp 𝕂 (t • x) * x) t
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_3<VAR>NontriviallyNormedField 𝕂<VAR>CharZero 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕂<VAR>htx : t • x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasStrictDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (x * NormedSpace.exp 𝕂 (t • x)) t
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_3<VAR>NontriviallyNormedField 𝕂<VAR>CharZero 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕂<VAR>htx : t • x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (NormedSpace.exp 𝕂 (t • x) * x) t
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_3<VAR>NontriviallyNormedField 𝕂<VAR>CharZero 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕂<VAR>htx : t • x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (x * NormedSpace.exp 𝕂 (t • x)) t
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>RCLike 𝕂<VAR>NormedCommRing 𝕊<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝕊<VAR>NormedAlgebra 𝕂 𝔸<VAR>Algebra 𝕊 𝔸<VAR>ContinuousSMul 𝕊 𝔸<VAR>IsScalarTower 𝕂 𝕊 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<GOAL>HasFDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (NormedSpace.exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>RCLike 𝕂<VAR>NormedCommRing 𝕊<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝕊<VAR>NormedAlgebra 𝕂 𝔸<VAR>Algebra 𝕊 𝔸<VAR>ContinuousSMul 𝕊 𝔸<VAR>IsScalarTower 𝕂 𝕊 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<GOAL>HasFDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp 𝕂 (t • x))) t
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>RCLike 𝕂<VAR>NormedCommRing 𝕊<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝕊<VAR>NormedAlgebra 𝕂 𝔸<VAR>Algebra 𝕊 𝔸<VAR>ContinuousSMul 𝕊 𝔸<VAR>IsScalarTower 𝕂 𝕊 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<GOAL>HasStrictFDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (NormedSpace.exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>RCLike 𝕂<VAR>NormedCommRing 𝕊<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝕊<VAR>NormedAlgebra 𝕂 𝔸<VAR>Algebra 𝕊 𝔸<VAR>ContinuousSMul 𝕊 𝔸<VAR>IsScalarTower 𝕂 𝕊 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<GOAL>HasStrictFDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp 𝕂 (t • x))) t
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_3<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕂<GOAL>HasStrictDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (NormedSpace.exp 𝕂 (t • x) * x) t
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_3<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕂<GOAL>HasStrictDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (x * NormedSpace.exp 𝕂 (t • x)) t
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_3<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕂<GOAL>HasDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (NormedSpace.exp 𝕂 (t • x) * x) t
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_3<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕂<GOAL>HasDerivAt (fun u => NormedSpace.exp 𝕂 (u • x)) (x * NormedSpace.exp 𝕂 (t • x)) t
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>ι : Type u_3<VAR>f : ι → 𝔸<VAR>a : 𝔸<VAR>h : HasSum f a<GOAL>HasProd (NormedSpace.exp 𝕂 ∘ f) (NormedSpace.exp 𝕂 a)
<VAR>z : ℂ<GOAL>AnalyticAt ℂ cexp z
<VAR>E : Type<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>fa : AnalyticAt ℂ f x<GOAL>AnalyticAt ℂ (fun z => cexp (f z)) x
<VAR>E : Type<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>fs : AnalyticOn ℂ f s<GOAL>AnalyticOn ℂ (fun z => cexp (f z)) s
<VAR>z : ℂ<VAR>m : z ∈ Complex.slitPlane<GOAL>AnalyticAt ℂ Complex.log z
<VAR>E : Type<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>fa : AnalyticAt ℂ f x<VAR>m : f x ∈ Complex.slitPlane<GOAL>AnalyticAt ℂ (fun z => Complex.log (f z)) x
<VAR>E : Type<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>fs : AnalyticOn ℂ f s<VAR>m : ∀ z ∈ s, f z ∈ Complex.slitPlane<GOAL>AnalyticOn ℂ (fun z => Complex.log (f z)) s
<VAR>E : Type<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>x : E<VAR>fa : AnalyticAt ℂ f x<VAR>ga : AnalyticAt ℂ g x<VAR>m : f x ∈ Complex.slitPlane<GOAL>AnalyticAt ℂ (fun z => f z ^ g z) x
<VAR>E : Type<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>s : Set E<VAR>fs : AnalyticOn ℂ f s<VAR>gs : AnalyticOn ℂ g s<VAR>m : ∀ z ∈ s, f z ∈ Complex.slitPlane<GOAL>AnalyticOn ℂ (fun z => f z ^ g z) s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>f_nn : 0 ≤ᵐ[μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>f_nn : 0 ≤ᵐ[μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>n ν : ℕ<VAR>x : ↑I<GOAL>(bernstein n ν) x = ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
<VAR>n : ℕ<VAR>h : 0 < ↑n<VAR>x : ↑I<GOAL>∑ k : Fin (n + 1), (↑x - ↑k/ₙ) ^ 2 * (bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
<VAR>n : ℕ<VAR>f : C(↑I, ℝ)<VAR>x : ↑I<GOAL>(bernsteinApproximation n f) x = ∑ k : Fin (n + 1), f k/ₙ * (bernstein n ↑k) x
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<GOAL>0 < bernsteinApproximation.δ f ε h
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>n : ℕ<VAR>x : ↑I<VAR>k : Fin (n + 1)<VAR>m : k ∈ bernsteinApproximation.S f ε h n x<GOAL>|f k/ₙ - f x| < ε / 2
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>n : ℕ<VAR>x : ↑I<VAR>k : Fin (n + 1)<VAR>m : k ∈ (bernsteinApproximation.S f ε h n x)ᶜ<GOAL>1 ≤ bernsteinApproximation.δ f ε h ^ (-2) * (↑x - ↑k/ₙ) ^ 2
<VAR>f : C(↑I, ℝ)<GOAL>Filter.Tendsto (fun n => bernsteinApproximation n f) Filter.atTop (𝓝 f)
<GOAL>Stirling.stirlingSeq 1 = rexp 1 / √2
<VAR>n : ℕ<GOAL>Real.log (Stirling.stirlingSeq n) = Real.log ↑n ! - 1 / 2 * Real.log (2 * ↑n) - ↑n * Real.log (↑n / rexp 1)
<VAR>m : ℕ<GOAL>HasSum (fun k => 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ (k + 1)) (Real.log (Stirling.stirlingSeq (m + 1)) - Real.log (Stirling.stirlingSeq (m + 2)))
<GOAL>Antitone (Real.log ∘ Stirling.stirlingSeq ∘ Nat.succ)
<VAR>n : ℕ<GOAL>Real.log (Stirling.stirlingSeq (n + 1)) - Real.log (Stirling.stirlingSeq (n + 2)) ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)
<VAR>n : ℕ<GOAL>Real.log (Stirling.stirlingSeq (n + 1)) - Real.log (Stirling.stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)
<GOAL>∃ c, ∀ (n : ℕ), Real.log (Stirling.stirlingSeq 1) - Real.log (Stirling.stirlingSeq (n + 1)) ≤ c
<GOAL>∃ c, ∀ (n : ℕ), c ≤ Real.log (Stirling.stirlingSeq (n + 1))
<VAR>n : ℕ<GOAL>0 < Stirling.stirlingSeq (n + 1)
<GOAL>∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ Stirling.stirlingSeq (n + 1)
<GOAL>Antitone (Stirling.stirlingSeq ∘ Nat.succ)
<GOAL>∃ a, 0 < a ∧ Filter.Tendsto Stirling.stirlingSeq Filter.atTop (𝓝 a)
<GOAL>Filter.Tendsto (fun n => ↑n / (2 * ↑n + 1)) Filter.atTop (𝓝 (1 / 2))
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Stirling.stirlingSeq n ^ 4 / Stirling.stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Real.Wallis.W n
<VAR>a : ℝ<VAR>hane : a ≠ 0<VAR>ha : Filter.Tendsto Stirling.stirlingSeq Filter.atTop (𝓝 a)<GOAL>Filter.Tendsto Real.Wallis.W Filter.atTop (𝓝 (a ^ 2 / 2))
<GOAL>Filter.Tendsto Stirling.stirlingSeq Filter.atTop (𝓝 √π)
<GOAL>(fun n => ↑n !) ~[Filter.atTop] fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>Filter.Tendsto (fun x => x ^ y) Filter.atTop Filter.atTop
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>Filter.Tendsto (fun x => x ^ (-y)) Filter.atTop (𝓝 0)
<VAR>b : ℝ<VAR>hb₀ : -1 < b<VAR>hb₁ : b < 1<GOAL>Filter.Tendsto (fun x => b ^ x) Filter.atTop (𝓝 0)
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>Filter.Tendsto (fun x => b ^ x) Filter.atBot (𝓝 0)
<VAR>b : ℝ<VAR>hb₀ : 0 < b<VAR>hb₁ : b < 1<GOAL>Filter.Tendsto (fun x => b ^ x) Filter.atBot Filter.atTop
<VAR>a b c : ℝ<VAR>hb : 0 ≠ b<GOAL>Filter.Tendsto (fun x => x ^ (a / (b * x + c))) Filter.atTop (𝓝 1)
<GOAL>Filter.Tendsto (fun x => x ^ (1 / x)) Filter.atTop (𝓝 1)
<GOAL>Filter.Tendsto (fun x => x ^ (-1 / x)) Filter.atTop (𝓝 1)
<VAR>s : ℝ<GOAL>Filter.Tendsto (fun x => rexp x / x ^ s) Filter.atTop Filter.atTop
<VAR>s b : ℝ<VAR>hb : 0 < b<GOAL>Filter.Tendsto (fun x => rexp (b * x) / x ^ s) Filter.atTop Filter.atTop
<VAR>s b : ℝ<VAR>hb : 0 < b<GOAL>Filter.Tendsto (fun x => x ^ s * rexp (-b * x)) Filter.atTop (𝓝 0)
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>Filter.Tendsto (fun x => x ^ y) (𝓝 ⊤) (𝓝 ⊤)
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>hl : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|<GOAL>(fun x => rexp ((f x).arg * (g x).im)) =Θ[l] fun x => 1
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>hl : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|<GOAL>(fun x => f x ^ g x) =O[l] fun x => Complex.abs (f x) ^ (g x).re