ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_2<VAR>P : Type u_4<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>h : (↑s).Nonempty<GOAL>IsConnected {y | s.WSameSide x y}
<VAR>V : Type u_2<VAR>P : Type u_4<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<GOAL>IsPreconnected {y | s.WSameSide x y}
<VAR>V : Type u_2<VAR>P : Type u_4<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>hx : x ∉ s<VAR>h : (↑s).Nonempty<GOAL>IsConnected {y | s.SSameSide x y}
<VAR>V : Type u_2<VAR>P : Type u_4<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<GOAL>IsPreconnected {y | s.SSameSide x y}
<VAR>V : Type u_2<VAR>P : Type u_4<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>h : (↑s).Nonempty<GOAL>IsConnected {y | s.WOppSide x y}
<VAR>V : Type u_2<VAR>P : Type u_4<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<GOAL>IsPreconnected {y | s.WOppSide x y}
<VAR>V : Type u_2<VAR>P : Type u_4<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>hx : x ∉ s<VAR>h : (↑s).Nonempty<GOAL>IsConnected {y | s.SOppSide x y}
<VAR>V : Type u_2<VAR>P : Type u_4<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<GOAL>IsPreconnected {y | s.SOppSide x y}
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>RCLike 𝕜<VAR>NonUnitalNormedRing A<VAR>StarRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>ContinuousFunctionalCalculus 𝕜 p₁<GOAL>(cfcₙAux ⋯ a ha) (ContinuousMapZero.id ⋯) = ↑a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>RCLike 𝕜<VAR>NonUnitalNormedRing A<VAR>StarRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>ContinuousFunctionalCalculus 𝕜 p₁<GOAL>ClosedEmbedding ⇑(cfcₙAux ⋯ a ha)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>RCLike 𝕜<VAR>NonUnitalNormedRing A<VAR>StarRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜<GOAL>spectrum 𝕜 ((cfcₙAux ⋯ a ha) f) = Set.range ⇑f
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>RCLike 𝕜<VAR>NonUnitalNormedRing A<VAR>StarRing A<VAR>CompleteSpace A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜<GOAL>(cfcₙAux ⋯ a ha) f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>RCLike 𝕜<VAR>NonUnitalNormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>ContinuousFunctionalCalculus 𝕜 p₁<GOAL>NonUnitalContinuousFunctionalCalculus 𝕜 p
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module ℂ A<VAR>IsScalarTower ℂ A A<VAR>SMulCommClass ℂ A A<VAR>NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<GOAL>IsSelfAdjoint a ↔ IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module ℂ A<VAR>IsScalarTower ℂ A A<VAR>SMulCommClass ℂ A A<VAR>NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<VAR>ha : QuasispectrumRestricts a ⇑Complex.reCLM<VAR>IsStarNormal a<GOAL>IsSelfAdjoint a
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℂ A<VAR>ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<GOAL>IsSelfAdjoint a ↔ IsStarNormal a ∧ SpectrumRestricts a ⇑Complex.reCLM
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℂ A<VAR>ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>SpectrumRestricts a ⇑Complex.reCLM
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℂ A<VAR>ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<VAR>ha : SpectrumRestricts a ⇑Complex.reCLM<VAR>IsStarNormal a<GOAL>IsSelfAdjoint a
<VAR>A : Type u_1<VAR>NonUnitalRing A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Module ℝ A<VAR>IsScalarTower ℝ A A<VAR>SMulCommClass ℝ A A<VAR>NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>a : A<VAR>ha₁ : IsSelfAdjoint a<VAR>ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>∃ x, IsSelfAdjoint x ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x * x = a
<VAR>A : Type u_1<VAR>NonUnitalRing A<VAR>PartialOrder A<VAR>StarRing A<VAR>StarOrderedRing A<VAR>TopologicalSpace A<VAR>Module ℝ A<VAR>IsScalarTower ℝ A A<VAR>SMulCommClass ℝ A A<VAR>NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>NonnegSpectrumClass ℝ A<VAR>a : A<GOAL>0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_1<VAR>Ring A<VAR>StarRing A<VAR>TopologicalSpace A<VAR>Algebra ℝ A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>a : A<VAR>ha₁ : IsSelfAdjoint a<VAR>ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>∃ x, IsSelfAdjoint x ∧ SpectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x ^ 2 = a
<VAR>A : Type u_1<VAR>Ring A<VAR>PartialOrder A<VAR>StarRing A<VAR>StarOrderedRing A<VAR>TopologicalSpace A<VAR>Algebra ℝ A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>NonnegSpectrumClass ℝ A<VAR>a : A<GOAL>0 ≤ a ↔ IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>a : A<VAR>t : NNReal<VAR>ha : IsSelfAdjoint a<VAR>ht : ‖a‖₊ ≤ t<GOAL>SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>a b : A<VAR>ha₁ : IsSelfAdjoint a<VAR>hb₁ : IsSelfAdjoint b<VAR>ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal<GOAL>SpectrumRestricts (a + b) ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>SpectrumRestricts (a ^ 2) ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>ha₁ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>ha₂ : SpectrumRestricts (-a) ⇑ContinuousMap.realToNNReal<GOAL>a = 0
<VAR>A : Type u_2<VAR>Ring A<VAR>Algebra ℝ A<VAR>a : A<VAR>ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>SpectrumRestricts (r • a) ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>CstarRing A<VAR>CompleteSpace A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<VAR>b : A<VAR>x : ℝ<GOAL>x ∈ spectrum ℝ (star b * b) → 0 ≤ x
<VAR>A : Type u_2<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℂ A<VAR>ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<VAR>x : ℝ<VAR>ha : IsSelfAdjoint a := by cfc_tac<GOAL>↑x ∈ spectrum ℂ a ↔ x ∈ spectrum ℝ a
<VAR>A : Type u_1<VAR>NormedRing A<VAR>CompleteSpace A<VAR>StarRing A<VAR>CstarRing A<VAR>NormedAlgebra ℂ A<VAR>StarModule ℂ A<GOAL>StarOrderedRing A
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℂ A<VAR>ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>UniqueContinuousFunctionalCalculus ℝ A<VAR>UniqueContinuousFunctionalCalculus ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra ℂ A<VAR>ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>UniqueContinuousFunctionalCalculus ℝ A<VAR>UniqueContinuousFunctionalCalculus ℂ A<VAR>a : A<VAR>f : ℝ → ℝ<VAR>ha : IsSelfAdjoint a := by cfc_tac<GOAL>cfc f a = cfc (fun x => ↑(f x.re)) a
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>Ring A<VAR>PartialOrder A<VAR>StarRing A<VAR>StarOrderedRing A<VAR>Algebra ℝ A<VAR>TopologicalRing A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>ContinuousFunctionalCalculus NNReal fun x => 0 ≤ x<VAR>UniqueContinuousFunctionalCalculus ℝ A<VAR>NonnegSpectrumClass ℝ A<VAR>a : A<VAR>ha : 0 ≤ a<GOAL>cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯
<VAR>A : Type u_1<VAR>TopologicalSpace A<VAR>Ring A<VAR>PartialOrder A<VAR>StarRing A<VAR>StarOrderedRing A<VAR>Algebra ℝ A<VAR>TopologicalRing A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>ContinuousFunctionalCalculus NNReal fun x => 0 ≤ x<VAR>UniqueContinuousFunctionalCalculus ℝ A<VAR>NonnegSpectrumClass ℝ A<VAR>a : A<VAR>f : NNReal → NNReal<VAR>ha : 0 ≤ a := by cfc_tac<GOAL>cfc f a = cfc (fun x => ↑(f x.toNNReal)) a
<VAR>x : ENNReal<VAR>h : x ≠ 0<VAR>h' : x ≠ ⊤<GOAL>x.log = ↑(Real.log x.toReal)
<VAR>x : ENNReal<VAR>h : 0 < x.toReal<GOAL>x.log = ↑(Real.log x.toReal)
<VAR>x : NNReal<VAR>h : x ≠ 0<GOAL>(↑x).log = ↑(Real.log ↑x)
<VAR>x y : ENNReal<GOAL>x.log = y.log ↔ x = y
<VAR>x : ENNReal<GOAL>x.log = ⊥ ↔ x = 0
<VAR>x : ENNReal<GOAL>x.log = 0 ↔ x = 1
<VAR>x : ENNReal<GOAL>x.log = ⊤ ↔ x = ⊤
<VAR>x y : ENNReal<GOAL>x.log < y.log ↔ x < y
<VAR>x : ENNReal<GOAL>⊥ < x.log ↔ 0 < x
<VAR>x : ENNReal<GOAL>x.log < ⊤ ↔ x < ⊤
<VAR>x : ENNReal<GOAL>x.log < 0 ↔ x < 1
<VAR>x : ENNReal<GOAL>0 < x.log ↔ 1 < x
<VAR>x y : ENNReal<GOAL>x.log ≤ y.log ↔ x ≤ y
<VAR>x : ENNReal<GOAL>x.log ≤ 0 ↔ x ≤ 1
<VAR>x : ENNReal<GOAL>0 ≤ x.log ↔ 1 ≤ x
<VAR>x y : ENNReal<GOAL>(x * y).log = x.log + y.log
<VAR>x : ENNReal<VAR>n : ℕ<GOAL>(x ^ n).log = ↑n * x.log
<VAR>x : ENNReal<VAR>y : ℝ<GOAL>(x ^ y).log = ↑y * x.log
<VAR>x : ENNReal<GOAL>x⁻¹.log = -x.log
<GOAL>MonotoneOn (fun x => Real.log x * x) {x | 1 ≤ x}
<GOAL>AntitoneOn (fun x => Real.log x / x) {x | Real.exp 1 ≤ x}
<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>AntitoneOn (fun x => Real.log x / x ^ a) {x | Real.exp (1 / a) ≤ x}
<GOAL>AntitoneOn (fun x => Real.log x / √x) {x | Real.exp 2 ≤ x}
<GOAL>DifferentiableOn ℝ (fun x => x * Real.log x) {0}ᶜ
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv (fun x => x * Real.log x) x = Real.log x + 1
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasDerivAt (fun x => x * Real.log x) (Real.log x + 1) x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv^[2] (fun x => x * Real.log x) x = x⁻¹
<GOAL>StrictConvexOn ℝ (Set.Ici 0) fun x => x * Real.log x
<GOAL>ConvexOn ℝ (Set.Ici 0) fun x => x * Real.log x
<VAR>x : ℝ<VAR>hx : 1 ≤ x<GOAL>0 ≤ x * Real.log x
<VAR>x : ℝ<VAR>hx₀ : 0 ≤ x<VAR>hx₁ : x ≤ 1<GOAL>x * Real.log x ≤ 0
<GOAL>Real.negMulLog = fun x => -x * Real.log x
<GOAL>Real.negMulLog = fun x => -(x * Real.log x)
<GOAL>DifferentiableOn ℝ Real.negMulLog {0}ᶜ
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv Real.negMulLog x = -Real.log x - 1
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasDerivAt Real.negMulLog (-Real.log x - 1) x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv^[2] Real.negMulLog x = -x⁻¹
<GOAL>StrictConcaveOn ℝ (Set.Ici 0) Real.negMulLog
<GOAL>ConcaveOn ℝ (Set.Ici 0) Real.negMulLog
<VAR>l : Filter ℂ<VAR>self : Complex.IsExpCmpFilter l<GOAL>Filter.Tendsto Complex.re l Filter.atTop
<VAR>l : Filter ℂ<VAR>self : Complex.IsExpCmpFilter l<VAR>n : ℕ<GOAL>(fun z => z.im ^ n) =O[l] fun z => Real.exp z.re
<VAR>l : Filter ℂ<VAR>hre : Filter.Tendsto Complex.re l Filter.atTop<VAR>r : ℝ<VAR>hr : Complex.im =O[l] fun z => z.re ^ r<GOAL>Complex.IsExpCmpFilter l
<VAR>l : Filter ℂ<VAR>hre : Filter.Tendsto Complex.re l Filter.atTop<VAR>n : ℕ<VAR>hr : Complex.im =O[l] fun z => z.re ^ n<GOAL>Complex.IsExpCmpFilter l
<VAR>l : Filter ℂ<VAR>hre : Filter.Tendsto Complex.re l Filter.atTop<VAR>him : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun z => |z.im|<GOAL>Complex.IsExpCmpFilter l
<VAR>l : Filter ℂ<VAR>hre : Filter.Tendsto Complex.re l Filter.atTop<VAR>him_le : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l Complex.im<VAR>him_ge : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l Complex.im<GOAL>Complex.IsExpCmpFilter l
<VAR>l : Filter ℂ<VAR>hl : Complex.IsExpCmpFilter l<GOAL>∀ᶠ (w : ℂ) in l, w ≠ 0
<VAR>l : Filter ℂ<VAR>hl : Complex.IsExpCmpFilter l<GOAL>Filter.Tendsto (fun z => |z.re|) l Filter.atTop
<VAR>l : Filter ℂ<VAR>hl : Complex.IsExpCmpFilter l<GOAL>Filter.Tendsto (⇑Complex.abs) l Filter.atTop
<VAR>l : Filter ℂ<VAR>hl : Complex.IsExpCmpFilter l<GOAL>(fun z => Real.log z.re) =o[l] Complex.re
<VAR>l : Filter ℂ<VAR>hl : Complex.IsExpCmpFilter l<VAR>n : ℕ<GOAL>(fun z => z.im ^ n) =o[l] fun z => Real.exp z.re
<VAR>l : Filter ℂ<VAR>hl : Complex.IsExpCmpFilter l<VAR>n : ℕ<GOAL>(fun z => |z.im| ^ n) ≤ᶠ[l] fun z => Real.exp z.re
<VAR>l : Filter ℂ<VAR>hl : Complex.IsExpCmpFilter l<GOAL>(fun z => Real.log (Complex.abs z)) =o[l] Complex.re
<VAR>l : Filter ℂ<VAR>hl : Complex.IsExpCmpFilter l<VAR>a : ℂ<GOAL>(fun x => x ^ a) =Θ[l] fun z => Real.exp (a.re * Real.log (Complex.abs z))
<VAR>l : Filter ℂ<VAR>hl : Complex.IsExpCmpFilter l<VAR>a : ℂ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(fun z => z ^ a) =o[l] fun z => Complex.exp (↑b * z)
<VAR>l : Filter ℂ<VAR>b₁ b₂ : ℝ<VAR>hl : Complex.IsExpCmpFilter l<VAR>hb : b₁ < b₂<VAR>a₁ a₂ : ℂ<GOAL>(fun z => z ^ a₁ * Complex.exp (↑b₁ * z)) =o[l] fun z => z ^ a₂ * Complex.exp (↑b₂ * z)
<VAR>l : Filter ℂ<VAR>hl : Complex.IsExpCmpFilter l<VAR>a : ℂ<VAR>b : ℝ<VAR>hb : b < 0<GOAL>(fun z => Complex.exp (↑b * z)) =o[l] fun z => z ^ a
<VAR>l : Filter ℂ<VAR>b₁ b₂ : ℝ<VAR>hl : Complex.IsExpCmpFilter l<VAR>hb : b₁ < b₂<VAR>m n : ℕ<GOAL>(fun z => z ^ m * Complex.exp (↑b₁ * z)) =o[l] fun z => z ^ n * Complex.exp (↑b₂ * z)
<VAR>l : Filter ℂ<VAR>b₁ b₂ : ℝ<VAR>hl : Complex.IsExpCmpFilter l<VAR>hb : b₁ < b₂<VAR>m n : ℤ<GOAL>(fun z => z ^ m * Complex.exp (↑b₁ * z)) =o[l] fun z => z ^ n * Complex.exp (↑b₂ * z)
<VAR>b x : ℝ<GOAL>Real.log x / Real.log b = Real.logb b x
<VAR>b : ℝ<GOAL>Real.logb b 0 = 0
<VAR>b : ℝ<GOAL>Real.logb b 1 = 0
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>Real.logb b b = 1
<VAR>b : ℝ<GOAL>Real.logb b b = 1 ↔ b ≠ 0 ∧ b ≠ 1 ∧ b ≠ -1
<VAR>b : ℝ<VAR>x : ℝ<GOAL>Real.logb b |x| = Real.logb b x
<VAR>b : ℝ<VAR>x : ℝ<GOAL>Real.logb b (-x) = Real.logb b x
<VAR>b x y : ℝ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.logb b (x * y) = Real.logb b x + Real.logb b y
<VAR>b x y : ℝ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.logb b (x / y) = Real.logb b x - Real.logb b y
<VAR>b : ℝ<VAR>x : ℝ<GOAL>Real.logb b x⁻¹ = -Real.logb b x
<VAR>a b : ℝ<GOAL>(Real.logb a b)⁻¹ = Real.logb b a
<VAR>a b : ℝ<VAR>h₁ : a ≠ 0<VAR>h₂ : b ≠ 0<VAR>c : ℝ<GOAL>(Real.logb (a * b) c)⁻¹ = (Real.logb a c)⁻¹ + (Real.logb b c)⁻¹
<VAR>a b : ℝ<VAR>h₁ : a ≠ 0<VAR>h₂ : b ≠ 0<VAR>c : ℝ<GOAL>(Real.logb (a / b) c)⁻¹ = (Real.logb a c)⁻¹ - (Real.logb b c)⁻¹
<VAR>a b : ℝ<VAR>h₁ : a ≠ 0<VAR>h₂ : b ≠ 0<VAR>c : ℝ<GOAL>Real.logb (a * b) c = ((Real.logb a c)⁻¹ + (Real.logb b c)⁻¹)⁻¹
<VAR>a b : ℝ<VAR>h₁ : a ≠ 0<VAR>h₂ : b ≠ 0<VAR>c : ℝ<GOAL>Real.logb (a / b) c = ((Real.logb a c)⁻¹ - (Real.logb b c)⁻¹)⁻¹
<VAR>a b c : ℝ<VAR>h₁ : b ≠ 0<VAR>h₂ : b ≠ 1<VAR>h₃ : b ≠ -1<GOAL>Real.logb a b * Real.logb b c = Real.logb a c
<VAR>a b c : ℝ<VAR>h₁ : c ≠ 0<VAR>h₂ : c ≠ 1<VAR>h₃ : c ≠ -1<GOAL>Real.logb a c / Real.logb b c = Real.logb a b
<VAR>b x y : ℝ<VAR>hx : 0 < x<GOAL>Real.logb b (x ^ y) = y * Real.logb b x
<VAR>b x : ℝ<VAR>k : ℕ<VAR>hx : 0 < x<GOAL>Real.logb b (x ^ k) = ↑k * Real.logb b x
<VAR>b : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<GOAL>Real.log b ≠ 0
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<GOAL>Real.logb b (b ^ x) = x
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : x ≠ 0<GOAL>b ^ Real.logb b x = |x|
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : 0 < x<GOAL>b ^ Real.logb b x = x
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : x < 0<GOAL>b ^ Real.logb b x = -x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hy : 0 < y<GOAL>Real.logb b y = x ↔ b ^ x = y
<VAR>b : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<GOAL>Set.SurjOn (Real.logb b) (Set.Ioi 0) Set.univ
<VAR>b : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<GOAL>Function.Surjective (Real.logb b)
<VAR>b : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<GOAL>Set.range (Real.logb b) = Set.univ
<VAR>b : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<GOAL>Set.SurjOn (Real.logb b) (Set.Iio 0) Set.univ
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>0 < b
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>b ≠ 1
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>h : 0 < x<VAR>h₁ : 0 < y<GOAL>Real.logb b x ≤ Real.logb b y ↔ x ≤ y
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>h : 0 < x<VAR>hxy : x ≤ y<GOAL>Real.logb b x ≤ Real.logb b y
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<VAR>hxy : x < y<GOAL>Real.logb b x < Real.logb b y
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>Real.logb b x < Real.logb b y ↔ x < y
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>Real.logb b x ≤ y ↔ x ≤ b ^ y
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>Real.logb b x < y ↔ x < b ^ y
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hy : 0 < y<GOAL>x ≤ Real.logb b y ↔ b ^ x ≤ y
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hy : 0 < y<GOAL>x < Real.logb b y ↔ b ^ x < y
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>0 < Real.logb b x ↔ 1 < x
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>hx : 1 < x<GOAL>0 < Real.logb b x
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>h : 0 < x<GOAL>Real.logb b x < 0 ↔ x < 1
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>h0 : 0 < x<VAR>h1 : x < 1<GOAL>Real.logb b x < 0
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>0 ≤ Real.logb b x ↔ 1 ≤ x
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>hx : 1 ≤ x<GOAL>0 ≤ Real.logb b x
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>Real.logb b x ≤ 0 ↔ x ≤ 1
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>hx : 0 ≤ x<GOAL>Real.logb b x ≤ 0 ↔ x ≤ 1
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>hx : 0 ≤ x<VAR>h'x : x ≤ 1<GOAL>Real.logb b x ≤ 0
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>StrictMonoOn (Real.logb b) (Set.Ioi 0)
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>StrictAntiOn (Real.logb b) (Set.Iio 0)
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>Set.InjOn (Real.logb b) (Set.Ioi 0)
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>h₁ : 0 < x<VAR>h₂ : Real.logb b x = 0<GOAL>x = 1
<VAR>b x : ℝ<VAR>hb : 1 < b<VAR>hx_pos : 0 < x<VAR>hx : x ≠ 1<GOAL>Real.logb b x ≠ 0
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>Filter.Tendsto (Real.logb b) Filter.atTop Filter.atTop
<VAR>b : ℝ<VAR>b_lt_one : b < 1<GOAL>b ≠ 1
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>h : 0 < x<VAR>h₁ : 0 < y<GOAL>Real.logb b x ≤ Real.logb b y ↔ y ≤ x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hxy : x < y<GOAL>Real.logb b y < Real.logb b x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>Real.logb b x < Real.logb b y ↔ y < x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<GOAL>Real.logb b x ≤ y ↔ b ^ y ≤ x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<GOAL>Real.logb b x < y ↔ b ^ y < x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hy : 0 < y<GOAL>x ≤ Real.logb b y ↔ y ≤ b ^ x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hy : 0 < y<GOAL>x < Real.logb b y ↔ y < b ^ x
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<GOAL>0 < Real.logb b x ↔ x < 1
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hx' : x < 1<GOAL>0 < Real.logb b x
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>h : 0 < x<GOAL>Real.logb b x < 0 ↔ 1 < x
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>h1 : 1 < x<GOAL>Real.logb b x < 0
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<GOAL>0 ≤ Real.logb b x ↔ x ≤ 1
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<GOAL>0 ≤ Real.logb b x
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<GOAL>Real.logb b x ≤ 0 ↔ 1 ≤ x
<VAR>b : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<GOAL>StrictAntiOn (Real.logb b) (Set.Ioi 0)
<VAR>b : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<GOAL>StrictMonoOn (Real.logb b) (Set.Iio 0)
<VAR>b : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<GOAL>Set.InjOn (Real.logb b) (Set.Ioi 0)
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>h₁ : 0 < x<VAR>h₂ : Real.logb b x = 0<GOAL>x = 1
<VAR>b x : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx_pos : 0 < x<VAR>hx : x ≠ 1<GOAL>Real.logb b x ≠ 0
<VAR>b : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<GOAL>Filter.Tendsto (Real.logb b) Filter.atTop Filter.atBot
<VAR>b : ℕ<VAR>r : ℝ<VAR>hb : 1 < b<VAR>hr : 0 ≤ r<GOAL>⌊Real.logb (↑b) r⌋ = Int.log b r
<VAR>b : ℕ<VAR>r : ℝ<VAR>hb : 1 < b<VAR>hr : 0 ≤ r<GOAL>⌈Real.logb (↑b) r⌉ = Int.clog b r
<VAR>b x : ℝ<GOAL>Real.logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
<VAR>b : ℝ<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ x ∈ s, f x ≠ 0<GOAL>Real.logb b (∏ i ∈ s, f i) = ∑ i ∈ s, Real.logb b (f i)
<VAR>P : ℝ → Prop<VAR>x₀ r : ℝ<VAR>hr : 1 < r<VAR>hx₀ : 0 < x₀<VAR>base : ∀ x ∈ Set.Ico x₀ (r * x₀), P x<VAR>step : ∀ n ≥ 1, (∀ z ∈ Set.Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Set.Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z<VAR>x : ℝ<GOAL>x ≥ x₀ → P x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>Real.log x = Real.expOrderIso.symm ⟨|x|, ⋯⟩
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>Real.log x = Real.expOrderIso.symm ⟨x, hx⟩
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>Real.exp (Real.log x) = |x|
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>Real.exp (Real.log x) = x
<VAR>x : ℝ<VAR>hx : x < 0<GOAL>Real.exp (Real.log x) = -x
<VAR>x : ℝ<GOAL>x ≤ Real.exp (Real.log x)
<VAR>x : ℝ<GOAL>Real.log (Real.exp x) = x
<GOAL>Set.SurjOn Real.log (Set.Ioi 0) Set.univ
<VAR>x : ℝ<GOAL>Real.log |x| = Real.log x
<VAR>x : ℝ<GOAL>Real.log (-x) = Real.log x
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>Real.sinh (Real.log x) = (x - x⁻¹) / 2
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>Real.cosh (Real.log x) = (x + x⁻¹) / 2
<GOAL>Set.SurjOn Real.log (Set.Iio 0) Set.univ
<VAR>x y : ℝ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.log (x * y) = Real.log x + Real.log y
<VAR>x y : ℝ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.log (x / y) = Real.log x - Real.log y
<VAR>x : ℝ<GOAL>Real.log x⁻¹ = -Real.log x
<VAR>x y : ℝ<VAR>h : 0 < x<VAR>h₁ : 0 < y<GOAL>Real.log x ≤ Real.log y ↔ x ≤ y
<VAR>x y : ℝ<VAR>hx : 0 < x<VAR>hxy : x ≤ y<GOAL>Real.log x ≤ Real.log y
<VAR>x y : ℝ<VAR>hx : 0 < x<VAR>h : x < y<GOAL>Real.log x < Real.log y
<VAR>x y : ℝ<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>Real.log x < Real.log y ↔ x < y
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>Real.log x ≤ y ↔ x ≤ Real.exp y
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>Real.log x < y ↔ x < Real.exp y
<VAR>x y : ℝ<VAR>hy : 0 < y<GOAL>x ≤ Real.log y ↔ Real.exp x ≤ y
<VAR>x y : ℝ<VAR>hy : 0 < y<GOAL>x < Real.log y ↔ Real.exp x < y
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>0 < Real.log x ↔ 1 < x
<VAR>x : ℝ<VAR>hx : 1 < x<GOAL>0 < Real.log x
<VAR>x : ℝ<VAR>hx : x < -1<GOAL>0 < Real.log x
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>Real.log x < 0 ↔ x < 1
<VAR>x : ℝ<VAR>h0 : 0 < x<VAR>h1 : x < 1<GOAL>Real.log x < 0
<VAR>x : ℝ<VAR>h0 : x < 0<VAR>h1 : -1 < x<GOAL>Real.log x < 0
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>0 ≤ Real.log x ↔ 1 ≤ x
<VAR>x : ℝ<VAR>hx : 1 ≤ x<GOAL>0 ≤ Real.log x
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>Real.log x ≤ 0 ↔ x ≤ 1
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>Real.log x ≤ 0 ↔ x ≤ 1
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>h'x : x ≤ 1<GOAL>Real.log x ≤ 0
<VAR>n : ℕ<GOAL>0 ≤ Real.log ↑n
<VAR>n : ℕ<GOAL>0 ≤ Real.log (-↑n)
<VAR>n : ℤ<GOAL>0 ≤ Real.log ↑n
<GOAL>StrictMonoOn Real.log (Set.Ioi 0)
<GOAL>StrictAntiOn Real.log (Set.Iio 0)
<GOAL>Set.InjOn Real.log (Set.Ioi 0)
<VAR>x : ℝ<VAR>hx1 : 0 < x<VAR>hx2 : x ≠ 1<GOAL>Real.log x < x - 1
<VAR>x : ℝ<VAR>h₁ : 0 < x<VAR>h₂ : Real.log x = 0<GOAL>x = 1
<VAR>x : ℝ<VAR>hx_pos : 0 < x<VAR>hx : x ≠ 1<GOAL>Real.log x ≠ 0
<VAR>x : ℝ<GOAL>Real.log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1