ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>hl_im : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|<VAR>hl : ∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0<GOAL>(fun x => f x ^ g x) =Θ[l] fun x => Complex.abs (f x) ^ (g x).re
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℂ<VAR>b : ℂ<VAR>hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0<GOAL>(fun x => f x ^ b) =Θ[l] fun x => Complex.abs (f x) ^ b.re
<VAR>α : Type u_1<VAR>r c : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>h : Asymptotics.IsBigOWith c l f g<VAR>hc : 0 ≤ c<VAR>hr : 0 ≤ r<VAR>hg : 0 ≤ᶠ[l] g<GOAL>Asymptotics.IsBigOWith (c ^ r) l (fun x => f x ^ r) fun x => g x ^ r
<VAR>α : Type u_1<VAR>r : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>hr : 0 ≤ r<VAR>hg : 0 ≤ᶠ[l] g<VAR>h : f =O[l] g<GOAL>(fun x => f x ^ r) =O[l] fun x => g x ^ r
<VAR>α : Type u_1<VAR>r : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>hr : 0 ≤ r<VAR>hf : 0 ≤ᶠ[l] f<VAR>hg : 0 ≤ᶠ[l] g<VAR>h : f =Θ[l] g<GOAL>(fun x => f x ^ r) =Θ[l] fun x => g x ^ r
<VAR>α : Type u_1<VAR>r : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>hr : 0 < r<VAR>hg : 0 ≤ᶠ[l] g<VAR>h : f =o[l] g<GOAL>(fun x => f x ^ r) =o[l] fun x => g x ^ r
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>hfg : f =O[l] g<VAR>hg : 0 ≤ᶠ[l] g<GOAL>(fun x => √(f x)) =O[l] fun x => √(g x)
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>hfg : f =o[l] g<VAR>hg : 0 ≤ᶠ[l] g<GOAL>(fun x => √(f x)) =o[l] fun x => √(g x)
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>hfg : f =Θ[l] g<VAR>hf : 0 ≤ᶠ[l] f<VAR>hg : 0 ≤ᶠ[l] g<GOAL>(fun x => √(f x)) =Θ[l] fun x => √(g x)
<VAR>s : ℝ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(fun x => x ^ s) =o[Filter.atTop] fun x => rexp (b * x)
<VAR>k : ℤ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(fun x => x ^ k) =o[Filter.atTop] fun x => rexp (b * x)
<VAR>k : ℕ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(fun x => x ^ k) =o[Filter.atTop] fun x => rexp (b * x)
<VAR>s : ℝ<GOAL>(fun x => x ^ s) =o[Filter.atTop] rexp
<VAR>a : ℝ<VAR>ha : 0 < a<VAR>b : ℝ<GOAL>(fun x => rexp (-a * x)) =o[Filter.atTop] fun x => x ^ b
<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Real.log =o[Filter.atTop] fun x => x ^ r
<VAR>s : ℝ<VAR>r : ℝ<VAR>hs : 0 < s<GOAL>(fun x => Real.log x ^ r) =o[Filter.atTop] fun x => x ^ s
<VAR>s : ℝ<VAR>r : ℝ<VAR>hs : s < 0<GOAL>(fun x => |Real.log x| ^ r) =o[𝓝[>] 0] fun x => x ^ s
<VAR>r : ℝ<VAR>hr : r < 0<GOAL>Real.log =o[𝓝[>] 0] fun x => x ^ r
<VAR>r : ℝ<VAR>hr : r < 0<GOAL>Filter.Tendsto (fun x => Real.log x / x ^ r) (𝓝[>] 0) (𝓝 0)
<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Filter.Tendsto (fun x => Real.log x * x ^ r) (𝓝[>] 0) (𝓝 0)
<GOAL>Filter.Tendsto (fun x => Real.log x * x) (𝓝[<] 0) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P : 𝕜[X]<VAR>hP : P ≠ 0<GOAL>∀ᶠ (x : 𝕜) in Filter.atTop, ¬P.IsRoot x
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P : 𝕜[X]<VAR>OrderTopology 𝕜<GOAL>(fun x => Polynomial.eval x P) ~[Filter.atTop] fun x => P.leadingCoeff * x ^ P.natDegree
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hdeg : 0 < P.degree<VAR>hnng : 0 ≤ P.leadingCoeff<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P) Filter.atTop Filter.atTop
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P : 𝕜[X]<VAR>OrderTopology 𝕜<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P) Filter.atTop Filter.atTop ↔ 0 < P.degree ∧ 0 ≤ P.leadingCoeff
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P : 𝕜[X]<VAR>OrderTopology 𝕜<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P) Filter.atTop Filter.atBot ↔ 0 < P.degree ∧ P.leadingCoeff ≤ 0
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hdeg : 0 < P.degree<VAR>hnps : P.leadingCoeff ≤ 0<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P) Filter.atTop Filter.atBot
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hdeg : 0 < P.degree<GOAL>Filter.Tendsto (fun x => |Polynomial.eval x P|) Filter.atTop Filter.atTop
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P : 𝕜[X]<VAR>OrderTopology 𝕜<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) Filter.atTop fun x => |Polynomial.eval x P|) ↔ P.degree ≤ 0
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P : 𝕜[X]<VAR>OrderTopology 𝕜<GOAL>Filter.Tendsto (fun x => |Polynomial.eval x P|) Filter.atTop Filter.atTop ↔ 0 < P.degree
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>c : 𝕜<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P) Filter.atTop (𝓝 c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>OrderTopology 𝕜<GOAL>(fun x => Polynomial.eval x P / Polynomial.eval x Q) ~[Filter.atTop] fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hdeg : P.degree < Q.degree<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hQ : Q ≠ 0<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (𝓝 0) ↔ P.degree < Q.degree
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hdeg : P.degree = Q.degree<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hdeg : Q.degree < P.degree<VAR>hpos : 0 < P.leadingCoeff / Q.leadingCoeff<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atTop
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hdeg : Q.degree < P.degree<VAR>hQ : Q ≠ 0<VAR>hnng : 0 ≤ P.leadingCoeff / Q.leadingCoeff<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atTop
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hdeg : Q.degree < P.degree<VAR>hneg : P.leadingCoeff / Q.leadingCoeff < 0<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atBot
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hdeg : Q.degree < P.degree<VAR>hQ : Q ≠ 0<VAR>hnps : P.leadingCoeff / Q.leadingCoeff ≤ 0<GOAL>Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atBot
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>hdeg : Q.degree < P.degree<VAR>hQ : Q ≠ 0<GOAL>Filter.Tendsto (fun x => |Polynomial.eval x P / Polynomial.eval x Q|) Filter.atTop Filter.atTop
<VAR>𝕜 : Type u_1<VAR>NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>OrderTopology 𝕜<VAR>h : P.degree ≤ Q.degree<GOAL>(fun x => Polynomial.eval x P) =O[Filter.atTop] fun x => Polynomial.eval x Q
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x
<VAR>x : ℝ<VAR>n : ℕ∞<VAR>hx : x ≠ 0<GOAL>ContDiffAt ℝ n (fun x => √x) x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasDerivAt (fun x => √x) (1 / (2 * √x)) x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>f' x : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hx : f x ≠ 0<GOAL>HasDerivWithinAt (fun y => √(f y)) (f' / (2 * √(f x))) s x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasDerivAt (fun y => √(f y)) (f' / (2 * √(f x))) x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasStrictDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasStrictDerivAt (fun t => √(f t)) (f' / (2 * √(f x))) x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>x : ℝ<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hx : f x ≠ 0<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>derivWithin (fun x => √(f x)) s x = derivWithin f s x / (2 * √(f x))
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hf : DifferentiableAt ℝ f x<VAR>hx : f x ≠ 0<GOAL>deriv (fun x => √(f x)) x = deriv f x / (2 * √(f x))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>f' : E →L[ℝ] ℝ<VAR>hf : HasFDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasFDerivAt (fun y => √(f y)) ((1 / (2 * √(f x))) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>f' : E →L[ℝ] ℝ<VAR>hf : HasStrictFDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasStrictFDerivAt (fun y => √(f y)) ((1 / (2 * √(f x))) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>x : E<VAR>f' : E →L[ℝ] ℝ<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hx : f x ≠ 0<GOAL>HasFDerivWithinAt (fun y => √(f y)) ((1 / (2 * √(f x))) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>x : E<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hx : f x ≠ 0<GOAL>DifferentiableWithinAt ℝ (fun y => √(f y)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hf : DifferentiableAt ℝ f x<VAR>hx : f x ≠ 0<GOAL>DifferentiableAt ℝ (fun y => √(f y)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>hf : DifferentiableOn ℝ f s<VAR>hs : ∀ x ∈ s, f x ≠ 0<GOAL>DifferentiableOn ℝ (fun y => √(f y)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>hf : Differentiable ℝ f<VAR>hs : ∀ (x : E), f x ≠ 0<GOAL>Differentiable ℝ fun y => √(f y)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>x : E<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hx : f x ≠ 0<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>fderivWithin ℝ (fun x => √(f x)) s x = (1 / (2 * √(f x))) • fderivWithin ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hf : DifferentiableAt ℝ f x<VAR>hx : f x ≠ 0<GOAL>fderiv ℝ (fun x => √(f x)) x = (1 / (2 * √(f x))) • fderiv ℝ f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>x : E<VAR>hf : ContDiffAt ℝ n f x<VAR>hx : f x ≠ 0<GOAL>ContDiffAt ℝ n (fun y => √(f y)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>s : Set E<VAR>x : E<VAR>hf : ContDiffWithinAt ℝ n f s x<VAR>hx : f x ≠ 0<GOAL>ContDiffWithinAt ℝ n (fun y => √(f y)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>s : Set E<VAR>hf : ContDiffOn ℝ n f s<VAR>hs : ∀ x ∈ s, f x ≠ 0<GOAL>ContDiffOn ℝ n (fun y => √(f y)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>h : ∀ (x : E), f x ≠ 0<GOAL>ContDiff ℝ n fun y => √(f y)
<VAR>x y : ℂ<GOAL>x.cpow y = x ^ y
<VAR>x y : ℂ<GOAL>x ^ y = if x = 0 then if y = 0 then 1 else 0 else Complex.exp (Complex.log x * y)
<VAR>x : ℂ<VAR>hx : x ≠ 0<VAR>y : ℂ<GOAL>x ^ y = Complex.exp (Complex.log x * y)
<VAR>x a : ℂ<GOAL>0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
<VAR>x : ℂ<GOAL>x ^ 1 = x
<VAR>x : ℂ<VAR>y z : ℂ<VAR>hx : x ≠ 0<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>x y : ℂ<VAR>z : ℂ<VAR>h₁ : -π < (Complex.log x * y).im<VAR>h₂ : (Complex.log x * y).im ≤ π<GOAL>x ^ (y * z) = (x ^ y) ^ z
<VAR>x : ℂ<VAR>y z : ℂ<VAR>hx : x ≠ 0<GOAL>x ^ (y - z) = x ^ y / x ^ z
<VAR>x : ℂ<VAR>n : ℕ<VAR>y : ℂ<GOAL>x ^ (↑n * y) = (x ^ y) ^ n
<VAR>x : ℂ<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>y : ℂ<GOAL>x ^ (OfNat.ofNat n * y) = (x ^ y) ^ OfNat.ofNat n
<VAR>x y : ℂ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>x ^ (y * OfNat.ofNat n) = (x ^ y) ^ OfNat.ofNat n
<VAR>x : ℂ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>x ^ OfNat.ofNat n = x ^ OfNat.ofNat n
<VAR>x : ℂ<GOAL>x ^ 2 = x ^ 2
<VAR>x : ℂ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(x ^ (OfNat.ofNat n)⁻¹) ^ OfNat.ofNat n = x
<VAR>x : ℂ<VAR>n : ℕ<VAR>hlt : -π < ↑n * x.arg<VAR>hle : ↑n * x.arg ≤ π<VAR>y : ℂ<GOAL>x ^ (↑n * y) = (x ^ n) ^ y
<VAR>x : ℂ<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>hlt : -π < OfNat.ofNat n * x.arg<VAR>hle : OfNat.ofNat n * x.arg ≤ π<VAR>y : ℂ<GOAL>x ^ (OfNat.ofNat n * y) = (x ^ OfNat.ofNat n) ^ y
<VAR>x : ℂ<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>hlt : -(π / OfNat.ofNat n) < x.arg<VAR>hle : x.arg ≤ π / OfNat.ofNat n<GOAL>(x ^ OfNat.ofNat n) ^ (OfNat.ofNat n)⁻¹ = x
<VAR>x : ℂ<VAR>hx : 0 < x.re<GOAL>(x ^ 2) ^ 2⁻¹ = x
<VAR>m n : ℕ<VAR>s : ℂ<GOAL>(↑m * ↑n) ^ s = ↑m ^ s * ↑n ^ s
<VAR>x : ℂ<GOAL>(Complex.log x).re = Real.log (Complex.abs x)
<VAR>x : ℂ<GOAL>(Complex.log x).im = x.arg
<VAR>x : ℂ<GOAL>-Real.pi < (Complex.log x).im
<VAR>x : ℂ<GOAL>(Complex.log x).im ≤ Real.pi
<VAR>x : ℂ<VAR>hx : x ≠ 0<GOAL>Complex.exp (Complex.log x) = x
<VAR>x : ℂ<VAR>hx₁ : -Real.pi < x.im<VAR>hx₂ : x.im ≤ Real.pi<GOAL>Complex.log (Complex.exp x) = x
<VAR>x y : ℂ<VAR>hx₁ : -Real.pi < x.im<VAR>hx₂ : x.im ≤ Real.pi<VAR>hy₁ : -Real.pi < y.im<VAR>hy₂ : y.im ≤ Real.pi<VAR>hxy : Complex.exp x = Complex.exp y<GOAL>x = y
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>↑(Real.log x) = Complex.log ↑x
<VAR>n : ℕ<GOAL>↑(Real.log ↑n) = Complex.log ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑(Real.log (OfNat.ofNat n)) = Complex.log (OfNat.ofNat n)
<VAR>x : ℝ<GOAL>(Complex.log ↑x).re = Real.log x
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℂ<VAR>hx : x ≠ 0<GOAL>Complex.log (↑r * x) = ↑(Real.log r) + Complex.log x
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℂ<VAR>hx : x ≠ 0<GOAL>Complex.log (x * ↑r) = ↑(Real.log r) + Complex.log x
<VAR>x y : ℂ<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<GOAL>Complex.log (x * y) = Complex.log x + Complex.log y ↔ x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi
<GOAL>Complex.log (-1) = ↑Real.pi * Complex.I
<GOAL>Complex.log Complex.I = ↑Real.pi / 2 * Complex.I
<GOAL>Complex.log (-Complex.I) = -(↑Real.pi / 2) * Complex.I
<VAR>x : ℂ<GOAL>Complex.log ((starRingEnd ℂ) x) = if x.arg = Real.pi then Complex.log x else (starRingEnd ℂ) (Complex.log x)
<VAR>x : ℂ<VAR>h : x.arg ≠ Real.pi<GOAL>Complex.log ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.log x)
<VAR>x : ℂ<GOAL>Complex.log x⁻¹ = if x.arg = Real.pi then -(starRingEnd ℂ) (Complex.log x) else -Complex.log x
<VAR>x : ℂ<VAR>hx : x.arg ≠ Real.pi<GOAL>Complex.log x⁻¹ = -Complex.log x
<GOAL>2 * ↑Real.pi * Complex.I ≠ 0
<VAR>x : ℂ<GOAL>Complex.exp x = 1 ↔ ∃ n, x = ↑n * (2 * ↑Real.pi * Complex.I)
<VAR>x y : ℂ<GOAL>Complex.exp x = Complex.exp y ↔ Complex.exp (x - y) = 1
<VAR>x y : ℂ<GOAL>Complex.exp x = Complex.exp y ↔ ∃ n, x = y + ↑n * (2 * ↑Real.pi * Complex.I)
<VAR>s : Set ℂ<GOAL>(Complex.exp ⁻¹' s).Countable ↔ s.Countable
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>Filter.Tendsto Complex.log (nhdsWithin z {z | z.im < 0}) (nhds (↑(Real.log (Complex.abs z)) - ↑Real.pi * Complex.I))
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>ContinuousWithinAt Complex.log {z | 0 ≤ z.im} z
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>Filter.Tendsto Complex.log (nhdsWithin z {z | 0 ≤ z.im}) (nhds (↑(Real.log (Complex.abs z)) + ↑Real.pi * Complex.I))
<GOAL>Filter.map Complex.exp (Filter.comap Complex.re Filter.atBot) = nhdsWithin 0 {0}ᶜ
<GOAL>Filter.map Complex.exp (Filter.comap Complex.re Filter.atTop) = Bornology.cobounded ℂ
<VAR>x : ℂ<VAR>h : x ∈ Complex.slitPlane<GOAL>ContinuousAt Complex.log x
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℂ<VAR>x : ℂ<VAR>h : Filter.Tendsto f l (nhds x)<VAR>hx : x ∈ Complex.slitPlane<GOAL>Filter.Tendsto (fun t => Complex.log (f t)) l (nhds (Complex.log x))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>x : α<VAR>h₁ : ContinuousAt f x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>ContinuousAt (fun t => Complex.log (f t)) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>s : Set α<VAR>x : α<VAR>h₁ : ContinuousWithinAt f s x<VAR>h₂ : f x ∈ Complex.slitPlane<GOAL>ContinuousWithinAt (fun t => Complex.log (f t)) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>s : Set α<VAR>h₁ : ContinuousOn f s<VAR>h₂ : ∀ x ∈ s, f x ∈ Complex.slitPlane<GOAL>ContinuousOn (fun t => Complex.log (f t)) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>h₁ : Continuous f<VAR>h₂ : ∀ (x : α), f x ∈ Complex.slitPlane<GOAL>Continuous fun t => Complex.log (f t)
<VAR>p b : ℝ<VAR>hb : 0 < b<VAR>hp : 1 < p<GOAL>(fun x => rexp (-b * x ^ p)) =o[Filter.atTop] fun x => rexp (-x)
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(fun x => rexp (-b * x ^ 2)) =o[Filter.atTop] fun x => rexp (-x)
<VAR>s : ℝ<VAR>b p : ℝ<VAR>hp : 1 < p<VAR>hb : 0 < b<GOAL>(fun x => x ^ s * rexp (-b * x ^ p)) =o[Filter.atTop] fun x => rexp (-(1 / 2) * x)
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<GOAL>(fun x => x ^ s * rexp (-b * x ^ 2)) =o[Filter.atTop] fun x => rexp (-(1 / 2) * x)
<VAR>p s : ℝ<VAR>hs : -1 < s<VAR>hp : 1 ≤ p<GOAL>MeasureTheory.IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Set.Ioi 0) MeasureTheory.volume
<VAR>p s b : ℝ<VAR>hs : -1 < s<VAR>hp : 1 ≤ p<VAR>hb : 0 < b<GOAL>MeasureTheory.IntegrableOn (fun x => x ^ s * rexp (-b * x ^ p)) (Set.Ioi 0) MeasureTheory.volume
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<VAR>hs : -1 < s<GOAL>MeasureTheory.IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Set.Ioi 0) MeasureTheory.volume
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<VAR>hs : -1 < s<GOAL>MeasureTheory.Integrable (fun x => x ^ s * rexp (-b * x ^ 2)) MeasureTheory.volume
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>MeasureTheory.Integrable (fun x => rexp (-b * x ^ 2)) MeasureTheory.volume
<VAR>b : ℝ<GOAL>MeasureTheory.IntegrableOn (fun x => rexp (-b * x ^ 2)) (Set.Ioi 0) MeasureTheory.volume ↔ 0 < b
<VAR>b : ℝ<GOAL>MeasureTheory.Integrable (fun x => rexp (-b * x ^ 2)) MeasureTheory.volume ↔ 0 < b
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>MeasureTheory.Integrable (fun x => x * rexp (-b * x ^ 2)) MeasureTheory.volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>MeasureTheory.Integrable (fun x => cexp (-b * ↑x ^ 2)) MeasureTheory.volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>MeasureTheory.Integrable (fun x => ↑x * cexp (-b * ↑x ^ 2)) MeasureTheory.volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>∫ (r : ℝ) in Set.Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>∫ (x : ℝ) in Set.Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2
<VAR>b : ℝ<GOAL>∫ (x : ℝ) in Set.Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2
<GOAL>Complex.Gamma (1 / 2) = ↑π ^ (1 / 2)
<VAR>n : ℕ<GOAL>‖↑n‖₊ = ↑n
<VAR>x : ℂ<GOAL>HasDerivAt Complex.exp (Complex.exp x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<GOAL>Differentiable 𝕜 Complex.exp
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>x : ℂ<GOAL>DifferentiableAt 𝕜 Complex.exp x
<VAR>n : ℕ<GOAL>deriv^[n] Complex.exp = Complex.exp
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n Complex.exp
<VAR>x : ℂ<GOAL>HasStrictDerivAt Complex.exp (Complex.exp x) x
<VAR>x : ℂ<GOAL>HasStrictFDerivAt Complex.exp (Complex.exp x • 1) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>f : 𝕜 → ℂ<VAR>f' : ℂ<VAR>x : 𝕜<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Complex.exp (f x)) (Complex.exp (f x) * f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>f : 𝕜 → ℂ<VAR>f' : ℂ<VAR>x : 𝕜<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Complex.exp (f x)) (Complex.exp (f x) * f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>f : 𝕜 → ℂ<VAR>f' : ℂ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Complex.exp (f x)) (Complex.exp (f x) * f') s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>f : 𝕜 → ℂ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => Complex.exp (f x)) s x = Complex.exp (f x) * derivWithin f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>f : 𝕜 → ℂ<VAR>x : 𝕜<VAR>hc : DifferentiableAt 𝕜 f x<GOAL>deriv (fun x => Complex.exp (f x)) x = Complex.exp (f x) * deriv f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<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 => Complex.exp (f x)) (Complex.exp (f x) • f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<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 => Complex.exp (f x)) (Complex.exp (f x) • f') s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<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 => Complex.exp (f x)) (Complex.exp (f x) • f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<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 => Complex.exp (f x)) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : E → ℂ<VAR>x : E<VAR>hc : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜 (fun x => Complex.exp (f x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : E → ℂ<VAR>s : Set E<VAR>hc : DifferentiableOn 𝕜 f s<GOAL>DifferentiableOn 𝕜 (fun x => Complex.exp (f x)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : E → ℂ<VAR>hc : Differentiable 𝕜 f<GOAL>Differentiable 𝕜 fun x => Complex.exp (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : E → ℂ<VAR>n : ℕ∞<VAR>h : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n fun x => Complex.exp (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<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 => Complex.exp (f x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<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 => Complex.exp (f x)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 ℂ<VAR>E : Type u_2<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 => Complex.exp (f x)) s x
<VAR>n : ℕ<VAR>c : ℂ<GOAL>(iteratedDeriv n fun s => Complex.exp (c * s)) = fun s => c ^ n * Complex.exp (c * s)
<VAR>x : ℝ<GOAL>HasStrictDerivAt Real.exp (Real.exp x) x
<VAR>x : ℝ<GOAL>HasDerivAt Real.exp (Real.exp x) x
<VAR>n : ℕ∞<GOAL>ContDiff ℝ n Real.exp
<VAR>x : ℝ<GOAL>DifferentiableAt ℝ Real.exp x
<VAR>n : ℕ<GOAL>deriv^[n] Real.exp = Real.exp
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Real.exp (f x)) (Real.exp (f x) * f') s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>s : Set ℝ<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>derivWithin (fun x => Real.exp (f x)) s x = Real.exp (f x) * derivWithin f s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hc : DifferentiableAt ℝ f x<GOAL>deriv (fun x => Real.exp (f x)) x = Real.exp (f x) * deriv f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<GOAL>ContDiff ℝ n fun x => Real.exp (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.exp (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.exp (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.exp (f x)) s x