ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Set.Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y<VAR>hn : 2 ≤ n<VAR>hx : 0 < x<GOAL>f ↑n + x * Real.log (↑n - 1) ≤ f (↑n + x)
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.BohrMollerup.logGammaSeq (x + 1) n = Real.BohrMollerup.logGammaSeq x (n + 1) + Real.log x - (x + 1) * (Real.log (↑n + 1) - Real.log ↑n)
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hf_conv : ConvexOn ℝ (Set.Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<VAR>n : ℕ<GOAL>f x ≤ f 1 + x * Real.log (↑n + 1) - x * Real.log ↑n + Real.BohrMollerup.logGammaSeq x n
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Set.Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y<VAR>hx : 0 < x<VAR>hn : n ≠ 0<GOAL>f 1 + Real.BohrMollerup.logGammaSeq x n ≤ f x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hf_conv : ConvexOn ℝ (Set.Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<GOAL>Filter.Tendsto (Real.BohrMollerup.logGammaSeq x) Filter.atTop (𝓝 (f x - f 1))
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hf_conv : ConvexOn ℝ (Set.Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y<VAR>hx : 0 < x<GOAL>Filter.Tendsto (Real.BohrMollerup.logGammaSeq x) Filter.atTop (𝓝 (f x - f 1))
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>Filter.Tendsto (Real.BohrMollerup.logGammaSeq x) Filter.atTop (𝓝 (Real.log (Real.Gamma x)))
<VAR>f : ℝ → ℝ<VAR>hf_conv : ConvexOn ℝ (Set.Ioi 0) (Real.log ∘ f)<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y<VAR>hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y<VAR>hf_one : f 1 = 1<GOAL>Set.EqOn f Real.Gamma (Set.Ioi 0)
<GOAL>StrictMonoOn Real.Gamma (Set.Ici 2)
<GOAL>Set.EqOn (Real.log ∘ Real.doublingGamma) (fun s => Real.log (Real.Gamma (s / 2)) + Real.log (Real.Gamma (s / 2 + 1 / 2)) + s * Real.log 2 - Real.log (2 * √π)) (Set.Ioi 0)
<GOAL>ConvexOn ℝ (Set.Ioi 0) (Real.log ∘ Real.doublingGamma)
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>s.doublingGamma = Real.Gamma s
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>Real.Gamma s * Real.Gamma (s + 1 / 2) = Real.Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π
<VAR>z : ℂ<VAR>h₁ : z ≠ Complex.I<VAR>h₂ : z ≠ -Complex.I<GOAL>Complex.tan z.arctan = z
<VAR>z : ℂ<VAR>h₀ : z ≠ ↑Real.pi / 2<VAR>h₁ : -(Real.pi / 2) < z.re<VAR>h₂ : z.re ≤ Real.pi / 2<GOAL>Complex.cos z ≠ 0
<VAR>z : ℂ<VAR>h₀ : z ≠ ↑Real.pi / 2<VAR>h₁ : -(Real.pi / 2) < z.re<VAR>h₂ : z.re ≤ Real.pi / 2<GOAL>(Complex.tan z).arctan = z
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>(1 + z).arg ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>Complex.log (1 + z * Complex.I) + -Complex.log (1 - z * Complex.I) = Complex.log ((1 + z * Complex.I) / (1 - z * Complex.I))
<VAR>x : ℝ<VAR>hx : ‖x‖ < 1<GOAL>HasSum (fun n => (-1) ^ n * x ^ (2 * n + 1) / ↑(2 * n + 1)) (Real.arctan x)
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>y : E<GOAL>↑PartialHomeomorph.univUnitBall.symm y = (√(1 - ‖y‖ ^ 2))⁻¹ • y
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<GOAL>↑PartialHomeomorph.univUnitBall x = (√(1 + ‖x‖ ^ 2))⁻¹ • x
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<GOAL>PartialHomeomorph.univUnitBall.target = Metric.ball 0 1
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<GOAL>PartialHomeomorph.univUnitBall.source = Set.univ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<GOAL>↑PartialHomeomorph.univUnitBall 0 = 0
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<GOAL>↑PartialHomeomorph.univUnitBall.symm 0 = 0
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<GOAL>∀ (a : E), ↑(Homeomorph.unitBall a) = ↑PartialHomeomorph.univUnitBall a
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<GOAL>∀ (a : ↑(Metric.ball 0 1)), Homeomorph.unitBall.symm a = ↑(PartialHomeomorph.univUnitBall.toHomeomorphSourceTarget.symm a)
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<GOAL>↑(Homeomorph.unitBall 0) = 0
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<VAR>hr : 0 < r<VAR>a : P<GOAL>↑(PartialHomeomorph.unitBallBall c r hr).symm a = r⁻¹ • (a -ᵥ c)
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(PartialHomeomorph.unitBallBall c r hr).source = Metric.ball 0 1
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<VAR>hr : 0 < r<VAR>a : E<GOAL>↑(PartialHomeomorph.unitBallBall c r hr) a = r • a +ᵥ c
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(PartialHomeomorph.unitBallBall c r hr).target = Metric.ball c r
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<GOAL>(PartialHomeomorph.univBall c r).source = Set.univ
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(PartialHomeomorph.univBall c r).target = Metric.ball c r
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<GOAL>Metric.ball c r ⊆ (PartialHomeomorph.univBall c r).target
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<GOAL>↑(PartialHomeomorph.univBall c r) 0 = c
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<GOAL>↑(PartialHomeomorph.univBall c r).symm c = 0
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<GOAL>Continuous ↑(PartialHomeomorph.univBall c r)
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>P : Type u_2<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<GOAL>ContinuousOn (↑(PartialHomeomorph.univBall c r).symm) (Metric.ball c r)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_5<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>l : Filter E<GOAL>Asymptotics.IsBigOWith ‖f‖ l ⇑f fun x => x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_5<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>l : Filter E<GOAL>⇑f =O[l] fun x => x
<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>F : Type u_5<VAR>G : Type u_6<VAR>SeminormedAddCommGroup F<VAR>SeminormedAddCommGroup G<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜₃ G<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>RingHomIsometric σ₂₃<VAR>α : Type u_7<VAR>g : F →SL[σ₂₃] G<VAR>f : α → F<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith ‖g‖ l (fun x' => g (f x')) f
<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>F : Type u_5<VAR>G : Type u_6<VAR>SeminormedAddCommGroup F<VAR>SeminormedAddCommGroup G<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜₃ G<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>RingHomIsometric σ₂₃<VAR>α : Type u_7<VAR>g : F →SL[σ₂₃] G<VAR>f : α → F<VAR>l : Filter α<GOAL>(fun x' => g (f x')) =O[l] f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_5<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>l : Filter E<VAR>x : E<GOAL>Asymptotics.IsBigOWith ‖f‖ l (fun x' => f (x' - x)) fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_5<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>l : Filter E<VAR>x : E<GOAL>(fun x' => f (x' - x)) =O[l] fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_5<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>e : E ≃SL[σ₁₂] F<VAR>RingHomIsometric σ₁₂<VAR>α : Type u_7<VAR>f : α → E<VAR>l : Filter α<GOAL>(fun x' => e (f x')) =O[l] f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_5<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>e : E ≃SL[σ₁₂] F<VAR>RingHomIsometric σ₁₂<VAR>l : Filter E<VAR>x : E<GOAL>(fun x' => e (x' - x)) =O[l] fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_5<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>e : E ≃SL[σ₁₂] F<VAR>RingHomIsometric σ₂₁<VAR>α : Type u_7<VAR>f : α → E<VAR>l : Filter α<GOAL>f =O[l] fun x' => e (f x')
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_5<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>e : E ≃SL[σ₁₂] F<VAR>RingHomIsometric σ₂₁<VAR>l : Filter E<VAR>x : E<GOAL>(fun x' => x' - x) =O[l] fun x' => e (x' - x)
<VAR>z : ℂ<VAR>hz : z ≠ 0<VAR>x : ℝ<GOAL>HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>hz : z ≠ 0<VAR>x : ℝ<GOAL>HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<GOAL>∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ n = ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(Real.sin x) * ↑(Real.cos x) ^ (n - 1)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<GOAL>∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(Real.sin x) * ↑(Real.cos x) ^ (n - 1) = (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ n) - (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (n - 2)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<GOAL>(1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ n = (↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (n - 2)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<GOAL>(1 - z ^ 2 / (↑n + 1) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (2 * n + 2) = (2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (2 * n)
<VAR>n : ℕ<GOAL>∫ (x : ℝ) in 0 ..π / 2, Real.cos x ^ n = 1 / 2 * ∫ (x : ℝ) in 0 ..π, Real.sin x ^ n
<VAR>n : ℕ<GOAL>0 < ∫ (x : ℝ) in 0 ..π / 2, Real.cos x ^ n
<VAR>z : ℂ<VAR>n : ℕ<GOAL>Complex.sin (↑π * z) = ((↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, Real.cos x ^ (2 * n))
<VAR>f : ℝ → ℂ<VAR>hf : ContinuousOn f (Set.Icc 0 (π / 2))<GOAL>Filter.Tendsto (fun n => (∫ (x : ℝ) in 0 ..π / 2, ↑(Real.cos x) ^ n * f x) / ↑(∫ (x : ℝ) in 0 ..π / 2, Real.cos x ^ n)) Filter.atTop (𝓝 (f 0))
<VAR>z : ℂ<GOAL>Filter.Tendsto (fun n => ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) Filter.atTop (𝓝 (Complex.sin (↑π * z)))
<VAR>x : ℝ<GOAL>Filter.Tendsto (fun n => π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) Filter.atTop (𝓝 (Real.sin (π * x)))
<VAR>x : ℝ≥0<VAR>y : ℝ<GOAL>x.rpow y = x ^ y
<VAR>x : ℝ≥0<VAR>y : ℝ<GOAL>↑(x ^ y) = ↑x ^ y
<VAR>x : ℝ≥0<GOAL>x ^ 0 = 1
<VAR>x : ℝ≥0<VAR>y : ℝ<GOAL>x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
<VAR>x : ℝ<VAR>h : x ≠ 0<GOAL>0 ^ x = 0
<VAR>x : ℝ≥0<GOAL>x ^ 1 = x
<VAR>x : ℝ≥0<VAR>hx : x ≠ 0<VAR>y z : ℝ<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>x : ℝ≥0<VAR>y z : ℝ<VAR>h : y + z ≠ 0<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>x : ℝ≥0<VAR>y z : ℝ<VAR>hy : 0 ≤ y<VAR>hz : 0 ≤ z<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>w y z : ℝ<VAR>x : ℝ≥0<VAR>hw : w ≠ 0<VAR>h : y + z = w<GOAL>x ^ w = x ^ y * x ^ z
<VAR>x : ℝ≥0<VAR>y z : ℝ<GOAL>x ^ (y * z) = (x ^ y) ^ z
<VAR>x : ℝ≥0<VAR>y : ℝ<GOAL>x ^ (-y) = (x ^ y)⁻¹
<VAR>x : ℝ≥0<GOAL>x ^ (-1) = x⁻¹
<VAR>x : ℝ≥0<VAR>hx : x ≠ 0<VAR>y z : ℝ<GOAL>x ^ (y - z) = x ^ y / x ^ z
<VAR>x : ℝ≥0<VAR>y z : ℝ<VAR>h : y - z ≠ 0<GOAL>x ^ (y - z) = x ^ y / x ^ z
<VAR>y : ℝ<VAR>hy : y ≠ 0<VAR>x : ℝ≥0<GOAL>(x ^ y) ^ (1 / y) = x
<VAR>y : ℝ<VAR>hy : y ≠ 0<VAR>x : ℝ≥0<GOAL>(x ^ (1 / y)) ^ y = x
<VAR>x : ℝ≥0<VAR>y : ℝ<GOAL>x⁻¹ ^ y = (x ^ y)⁻¹
<VAR>x y : ℝ≥0<VAR>z : ℝ<GOAL>(x / y) ^ z = x ^ z / y ^ z
<VAR>x : ℝ≥0<GOAL>NNReal.sqrt x = x ^ (1 / 2)
<VAR>x : ℝ≥0<VAR>n : ℕ<GOAL>x ^ ↑n = x ^ n
<VAR>x : ℝ≥0<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>x ^ OfNat.ofNat n = x ^ OfNat.ofNat n
<VAR>x : ℝ≥0<GOAL>x ^ 2 = x ^ 2
<VAR>x y : ℝ≥0<VAR>z : ℝ<GOAL>(x * y) ^ z = x ^ z * y ^ z
<VAR>r : ℝ<GOAL>∀ (x : ℝ≥0), (NNReal.rpowMonoidHom r) x = x ^ r
<VAR>l : List ℝ≥0<VAR>r : ℝ<GOAL>(List.map (fun x => x ^ r) l).prod = l.prod ^ r
<VAR>ι : Type u_1<VAR>l : List ι<VAR>f : ι → ℝ≥0<VAR>r : ℝ<GOAL>(List.map (fun x => f x ^ r) l).prod = (List.map f l).prod ^ r
<VAR>ι : Type u_1<VAR>s : Multiset ι<VAR>f : ι → ℝ≥0<VAR>r : ℝ<GOAL>(Multiset.map (fun x => f x ^ r) s).prod = (Multiset.map f s).prod ^ r
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>r : ℝ<GOAL>∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
<VAR>l : List ℝ<VAR>hl : ∀ x ∈ l, 0 ≤ x<VAR>r : ℝ<GOAL>(List.map (fun x => x ^ r) l).prod = l.prod ^ r
<VAR>ι : Type u_1<VAR>l : List ι<VAR>f : ι → ℝ<VAR>hl : ∀ i ∈ l, 0 ≤ f i<VAR>r : ℝ<GOAL>(List.map (fun x => f x ^ r) l).prod = (List.map f l).prod ^ r
<VAR>ι : Type u_1<VAR>s : Multiset ι<VAR>f : ι → ℝ<VAR>hs : ∀ i ∈ s, 0 ≤ f i<VAR>r : ℝ<GOAL>(Multiset.map (fun x => f x ^ r) s).prod = (Multiset.map f s).prod ^ r
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℝ<VAR>hs : ∀ i ∈ s, 0 ≤ f i<VAR>r : ℝ<GOAL>∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>h₁ : x ≤ y<VAR>h₂ : 0 ≤ z<GOAL>x ^ z ≤ y ^ z
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>h₁ : x < y<VAR>h₂ : 0 < z<GOAL>x ^ z < y ^ z
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z < y ^ z ↔ x < y
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z ≤ y ^ z ↔ x ≤ y
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ≤ y ^ (1 / z) ↔ x ^ z ≤ y
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ (1 / z) ≤ y ↔ x ≤ y ^ z
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x < y ^ z⁻¹ ↔ x ^ z < y
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ < y ↔ x < y ^ z
<VAR>x : ℝ≥0<VAR>y z : ℝ<VAR>hx : 1 < x<VAR>hyz : y < z<GOAL>x ^ y < x ^ z
<VAR>x : ℝ≥0<VAR>y z : ℝ<VAR>hx : 1 ≤ x<VAR>hyz : y ≤ z<GOAL>x ^ y ≤ x ^ z
<VAR>x : ℝ≥0<VAR>y z : ℝ<VAR>hx0 : 0 < x<VAR>hx1 : x < 1<VAR>hyz : z < y<GOAL>x ^ y < x ^ z
<VAR>x : ℝ≥0<VAR>y z : ℝ<VAR>hx0 : 0 < x<VAR>hx1 : x ≤ 1<VAR>hyz : z ≤ y<GOAL>x ^ y ≤ x ^ z
<VAR>p : ℝ<VAR>x : ℝ≥0<VAR>hx_pos : 0 < x<GOAL>0 < x ^ p
<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx1 : x < 1<VAR>hz : 0 < z<GOAL>x ^ z < 1
<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx2 : x ≤ 1<VAR>hz : 0 ≤ z<GOAL>x ^ z ≤ 1
<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx : 1 < x<VAR>hz : z < 0<GOAL>x ^ z < 1
<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx : 1 ≤ x<VAR>hz : z ≤ 0<GOAL>x ^ z ≤ 1
<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx : 1 < x<VAR>hz : 0 < z<GOAL>1 < x ^ z
<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>h : 1 ≤ x<VAR>h₁ : 0 ≤ z<GOAL>1 ≤ x ^ z
<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx1 : 0 < x<VAR>hx2 : x < 1<VAR>hz : z < 0<GOAL>1 < x ^ z
<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx1 : 0 < x<VAR>hx2 : x ≤ 1<VAR>hz : z ≤ 0<GOAL>1 ≤ x ^ z
<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx : x ≤ 1<VAR>h_one_le : 1 ≤ z<GOAL>x ^ z ≤ x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>Function.Injective fun y => y ^ x
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : z ≠ 0<GOAL>x ^ z = y ^ z ↔ x = y
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>Function.Surjective fun y => y ^ x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>Function.Bijective fun y => y ^ x
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : z ≠ 0<GOAL>x = y ^ z⁻¹ ↔ x ^ z = y
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : z ≠ 0<GOAL>x = y ^ (1 / z) ↔ x ^ z = y
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : z ≠ 0<GOAL>x ^ z⁻¹ = y ↔ x = y ^ z
<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : z ≠ 0<GOAL>x ^ (1 / z) = y ↔ x = y ^ z
<VAR>y : ℝ<VAR>hy : y ≠ 0<VAR>x : ℝ≥0<GOAL>(x ^ y) ^ y⁻¹ = x
<VAR>y : ℝ<VAR>hy : y ≠ 0<VAR>x : ℝ≥0<GOAL>(x ^ y⁻¹) ^ y = x
<VAR>x : ℝ≥0<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(x ^ n) ^ (↑n)⁻¹ = x
<VAR>x : ℝ≥0<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(x ^ (↑n)⁻¹) ^ n = x
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<GOAL>(x ^ y).toNNReal = x.toNNReal ^ y
<VAR>z : ℝ<VAR>h : 0 < z<GOAL>StrictMono fun x => x ^ z
<VAR>z : ℝ<VAR>h : 0 ≤ z<GOAL>Monotone fun x => x ^ z
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>x : ℝ≥0<GOAL>(NNReal.orderIsoRpow y hy) x = x ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>(NNReal.orderIsoRpow y hy).symm = NNReal.orderIsoRpow (1 / y) ⋯
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<GOAL>‖x ^ y‖₊ = ‖x‖₊ ^ y
<VAR>x : ℝ≥0∞<VAR>y : ℝ<GOAL>x.rpow y = x ^ y
<VAR>x : ℝ≥0∞<GOAL>x ^ 0 = 1
<VAR>y : ℝ<GOAL>⊤ ^ y = if 0 < y then ⊤ else if y = 0 then 1 else 0
<VAR>y : ℝ<VAR>h : 0 < y<GOAL>⊤ ^ y = ⊤
<VAR>x : ℝ≥0<VAR>y : ℝ<VAR>h : 0 ≤ y<GOAL>↑x ^ y = ↑(x ^ y)
<VAR>x : ℝ≥0<VAR>y : ℝ<GOAL>↑x ^ y = if x = 0 ∧ y < 0 then ⊤ else ↑(x ^ y)
<VAR>x : ℝ≥0∞<GOAL>x ^ 1 = x
<VAR>x : ℝ≥0∞<VAR>y : ℝ<GOAL>x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ⊤ ∧ y < 0
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>x ^ y = 0 ↔ x = 0
<VAR>x : ℝ≥0∞<VAR>y : ℝ<GOAL>x ^ y = ⊤ ↔ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>hy0 : 0 ≤ y<VAR>h : x ≠ ⊤<GOAL>x ^ y ≠ ⊤
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>hy0 : 0 ≤ y<VAR>h : x ≠ ⊤<GOAL>x ^ y < ⊤
<VAR>x : ℝ≥0∞<VAR>y z : ℝ<VAR>hx : x ≠ 0<VAR>h'x : x ≠ ⊤<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>x : ℝ≥0∞<VAR>y z : ℝ<VAR>hy : 0 ≤ y<VAR>hz : 0 ≤ z<GOAL>x ^ (y + z) = x ^ y * x ^ z
<VAR>x : ℝ≥0∞<VAR>y : ℝ<GOAL>x ^ (-y) = (x ^ y)⁻¹
<VAR>x : ℝ≥0∞<VAR>y z : ℝ<GOAL>x ^ (y * z) = (x ^ y) ^ z
<VAR>x : ℝ≥0∞<VAR>n : ℕ<GOAL>x ^ ↑n = x ^ n
<VAR>x : ℝ≥0∞<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>x ^ OfNat.ofNat n = x ^ OfNat.ofNat n
<VAR>x : ℝ≥0∞<GOAL>x ^ 2 = x ^ 2
<VAR>x y : ℝ≥0<VAR>z : ℝ<GOAL>(↑x * ↑y) ^ z = ↑x ^ z * ↑y ^ z
<VAR>x : ℝ≥0∞<VAR>y : ℝ<GOAL>x⁻¹ ^ y = (x ^ y)⁻¹
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>x : ℝ≥0∞<GOAL>(ENNReal.orderIsoRpow y hy) x = x ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>(ENNReal.orderIsoRpow y hy).symm = ENNReal.orderIsoRpow (1 / y) ⋯
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>h₁ : x ≤ y<VAR>h₂ : 0 ≤ z<GOAL>x ^ z ≤ y ^ z
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>h₁ : x < y<VAR>h₂ : 0 < z<GOAL>x ^ z < y ^ z
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z ≤ y ^ z ↔ x ≤ y
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z < y ^ z ↔ x < y
<VAR>x : ℝ≥0∞<VAR>y z : ℝ<VAR>hx : 1 < x<VAR>hx' : x ≠ ⊤<VAR>hyz : y < z<GOAL>x ^ y < x ^ z
<VAR>x : ℝ≥0∞<VAR>y z : ℝ<VAR>hx : 1 ≤ x<VAR>hyz : y ≤ z<GOAL>x ^ y ≤ x ^ z
<VAR>p : ℝ<VAR>x : ℝ≥0∞<VAR>hx_pos : 0 < x<VAR>hp_nonneg : 0 ≤ p<GOAL>0 < x ^ p
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx : 1 < x<VAR>hz : z < 0<GOAL>x ^ z < 1
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx : 1 ≤ x<VAR>hz : z < 0<GOAL>x ^ z ≤ 1
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx : 1 < x<VAR>hz : 0 < z<GOAL>1 < x ^ z
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx : 1 ≤ x<VAR>hz : 0 < z<GOAL>1 ≤ x ^ z
<VAR>x p : ℝ<VAR>hx_pos : 0 < x<GOAL>ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
<VAR>x p : ℝ<VAR>hx_nonneg : 0 ≤ x<VAR>hp_nonneg : 0 ≤ p<GOAL>ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x : ℝ≥0∞<GOAL>(x ^ n) ^ (↑n)⁻¹ = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>s : Set β<VAR>hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n<GOAL>TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : α), f n x) Filter.atTop s
<VAR>β : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>f : ℕ → β → F<VAR>u : ℕ → ℝ<VAR>hu : Summable u<VAR>s : Set β<VAR>hfu : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ u n<GOAL>TendstoUniformlyOn (fun N x => ∑ n ∈ Finset.range N, f n x) (fun x => ∑' (n : ℕ), f n x) Filter.atTop s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n<GOAL>TendstoUniformly (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : α), f n x) Filter.atTop
<VAR>β : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>f : ℕ → β → F<VAR>u : ℕ → ℝ<VAR>hu : Summable u<VAR>hfu : ∀ (n : ℕ) (x : β), ‖f n x‖ ≤ u n<GOAL>TendstoUniformly (fun N x => ∑ n ∈ Finset.range N, f n x) (fun x => ∑' (n : ℕ), f n x) Filter.atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>TopologicalSpace β<VAR>f : α → β → F<VAR>s : Set β<VAR>hf : ∀ (i : α), ContinuousOn (f i) s<VAR>hu : Summable u<VAR>hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n<GOAL>ContinuousOn (fun x => ∑' (n : α), f n x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>TopologicalSpace β<VAR>f : α → β → F<VAR>hf : ∀ (i : α), Continuous (f i)<VAR>hu : Summable u<VAR>hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n<GOAL>Continuous fun x => ∑' (n : α), f n x
<VAR>z : ℂ<VAR>hz : 1 + z ∈ Complex.slitPlane<GOAL>ContinuousOn (fun t => (1 + t • z)⁻¹) (Set.Icc 0 1)
<VAR>z : ℂ<VAR>hz : 1 + z ∈ Complex.slitPlane<GOAL>Complex.log (1 + z) = z * ∫ (t : ℝ) in 0 ..1, (1 + t • z)⁻¹
<VAR>z : ℂ<VAR>hz : 1 - z ∈ Complex.slitPlane<GOAL>Complex.log (1 - z)⁻¹ = z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹
<VAR>n : ℕ<GOAL>Complex.logTaylor (n + 1) = Complex.logTaylor n + fun z => (-1) ^ (n + 1) * z ^ n / ↑n
<VAR>n : ℕ<GOAL>Complex.logTaylor n 0 = 0
<VAR>n : ℕ<VAR>z : ℂ<GOAL>HasDerivAt (Complex.logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : 1 + z ∈ Complex.slitPlane<GOAL>HasDerivAt (fun z => Complex.log (1 + z) - Complex.logTaylor (n + 1) z) ((-z) ^ n * (1 + z)⁻¹) z
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖Complex.log (1 + z) - Complex.logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖Complex.log (1 + z) - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖Complex.log (1 - z)⁻¹ + Complex.logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖Complex.log (1 - z)⁻¹ - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>HasSum (fun n => (-1) ^ (n + 1) * z ^ n / ↑n) (Complex.log (1 + z))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>HasSum (fun n => z ^ n / ↑n) (-Complex.log (1 - z))
<VAR>s : ℝ<GOAL>(fun x => rexp (-x) * x ^ s) =o[Filter.atTop] fun x => rexp (-(1 / 2) * x)
<VAR>s : ℝ<VAR>h : 0 < s<GOAL>MeasureTheory.IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Set.Ioi 0) MeasureTheory.volume
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>MeasureTheory.IntegrableOn (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (Set.Ioi 0) MeasureTheory.volume
<VAR>s : ℝ<GOAL>(↑s).GammaIntegral = ↑(∫ (x : ℝ) in Set.Ioi 0, rexp (-x) * x ^ (s - 1))
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>Filter.Tendsto (fun X => s.partialGamma X) Filter.atTop (𝓝 s.GammaIntegral)
<VAR>s : ℂ<VAR>X : ℝ<VAR>hs : 0 < s.re<VAR>hX : 0 ≤ X<GOAL>IntervalIntegrable (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) MeasureTheory.volume 0 X