Complex.integral_cpow_mul_exp_neg_mul_Ioi
theorem Complex.integral_cpow_mul_exp_neg_mul_Ioi :
∀ {a : ℂ} {r : ℝ},
0 < a.re → 0 < r → ∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (a - 1) * (-(↑r * ↑t)).exp = (1 / ↑r) ^ a * a.Gamma
This theorem states that, for any complex number `a` with real part greater than zero and any real number `r` greater than zero, the definite integral over the interval `(0, ∞)` (represented by `Set.Ioi 0`) of the function `t ^ (a - 1) * exp (-(r * t))`, where `^` represents exponentiation, `exp` is the exponential function, and `t` is the variable of integration, is equal to `(1 / r)^a * Gamma(a)`, where `Gamma` is the Gamma function.
More concisely: For complex numbers `a` with real part greater than 0 and real `r > 0`, the definite integral of `t ^ (a - 1) * exp(-r * t)` over `(0, ∞)` equals `(1 / r)^a * Gamma(a)`.
|
Complex.hasDerivAt_GammaIntegral
theorem Complex.hasDerivAt_GammaIntegral :
∀ {s : ℂ},
0 < s.re → HasDerivAt Complex.GammaIntegral (∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (s - 1) * (↑t.log * ↑(-t).exp)) s
This theorem states that for any complex number `s`, such that the real part of `s` is greater than zero, the derivative of the Euler's gamma function (`Γ` integral) at `s` is given by the Mellin transform of the function `log(t) * exp(-t)`. The gamma function is defined as the integral over the positive real numbers, of `exp(-x) * x^(s - 1)`. The Mellin transform in this case is used in the form of an integral over the positive real numbers, of `t^(s - 1) * (log(t) * exp(-t))`.
More concisely: For complex numbers `s` with positive real part, the derivative of the gamma function is equal to the Mellin transform of `log(t) * exp(-t)`.
|
Complex.tendsto_self_mul_Gamma_nhds_zero
theorem Complex.tendsto_self_mul_Gamma_nhds_zero : Filter.Tendsto (fun z => z * z.Gamma) (nhdsWithin 0 {0}ᶜ) (nhds 1)
This theorem, titled `Complex.tendsto_self_mul_Gamma_nhds_zero`, states that at `s = 0`, the Gamma function multiplied by `z` tends towards 1. More specifically, it asserts that the limit of the function `z * z.Gamma` as `z` approaches 0, but excluding 0 itself (denoted by `{0}ᶜ`), is 1. This is a formal way of stating in Lean 4 that the Gamma function has a simple pole with residue 1 at `s = 0`.
More concisely: The theorem asserts that the limit of the product of `z` and `Gamma z` as `z` approaches 0 from non-zero values is 1.
|
Real.Gamma_add_one
theorem Real.Gamma_add_one : ∀ {s : ℝ}, s ≠ 0 → (s + 1).Gamma = s * s.Gamma
This theorem states that for any real number `s` not equal to zero, the Gamma function of `s` plus 1 equals `s` multiplied by the Gamma function of `s`. In mathematical terms, it's saying that for all `s ∈ ℝ, s ≠ 0`, we have `Γ(s + 1) = s * Γ(s)`. This is a property of the Gamma function often stated in mathematics as `Γ(n) = (n-1)!` for any positive integer `n`.
More concisely: For any non-zero real number `s`, the Gamma function satisfies `Γ(s + 1) = s * Γ(s)`.
|
Complex.Gamma_add_one
theorem Complex.Gamma_add_one : ∀ (s : ℂ), s ≠ 0 → (s + 1).Gamma = s * s.Gamma
This theorem states the recurrence relation for the Gamma function over complex numbers. Specifically, for any complex number `s` that is not zero, the value of the Gamma function at `s + 1` is equal to `s` multiplied by the value of the Gamma function at `s`. In mathematical notation, this could be written as Γ(s + 1) = s * Γ(s) for any complex s ≠ 0.
More concisely: For complex numbers `s` not equal to zero, the Gamma function satisfies the recurrence relation Γ(s + 1) = s * Γ(s).
|
Complex.Gamma_neg_nat_eq_zero
theorem Complex.Gamma_neg_nat_eq_zero : ∀ (n : ℕ), (-↑n).Gamma = 0
This theorem states that for any natural number `n`, the Gamma function of the negative of `n` (i.e., `-n`) is undefined, and by convention, we assign it the value of 0. In mathematical terms, it is saying that for all `n` in the set of natural numbers ℕ, the Gamma function Γ(-n) equals 0.
More concisely: For all natural numbers `n`, the Gamma function Γ(-`n`) is undefined and is conventionally assigned the value 0.
|
Complex.Gamma_zero
theorem Complex.Gamma_zero : Complex.Gamma 0 = 0
This theorem states that the Gamma function, when evaluated at zero, is undefined. However, by convention, we assign it the value zero. This is expressed in Lean 4 using the `Complex.Gamma` function, which computes the Gamma function for complex numbers. In the theorem `Complex.Gamma_zero`, it is asserted that `Complex.Gamma 0` equals zero.
More concisely: The Gamma function, usually undefined at 0, is conventionally assigned the value 0 in Lean 4. (Or equivalently, the theorem `Complex.Gamma_zero` asserts that `Complex.Gamma 0 = 0`.)
|
Complex.Gamma_ofReal
theorem Complex.Gamma_ofReal : ∀ (s : ℝ), (↑s).Gamma = ↑s.Gamma
This theorem states that for every real number `s`, the complex Gamma function evaluated at `s` equals the real Gamma function at `s` casted to a complex number. In mathematical terms, it says that for all `s` in the set of real numbers, the equation Γ(s) = Γ(s) holds, where the left side Γ denotes the complex Gamma function and the right side Γ denotes the real Gamma function.
More concisely: The complex Gamma function equals the real Gamma function for all real numbers.
|
Complex.GammaIntegral_eq_mellin
theorem Complex.GammaIntegral_eq_mellin : Complex.GammaIntegral = mellin fun x => ↑(-x).exp
This theorem states that Euler's integral for the Gamma function, denoted as `Complex.GammaIntegral`, can be rewritten as an example of a Mellin transform. In specific terms, the integral `∫ x in Ioi 0, exp (-x) * x ^ (s - 1)` that defines the Gamma function for a complex variable `s` is equivalent to the Mellin transform of the function `f` where `f(x) = exp(-x)`.
More concisely: The Gamma function's complex integral representation, `Complex.GammaIntegral`, is equal to the Mellin transform of `exp(-x)`.
|
Real.GammaIntegral_convergent
theorem Real.GammaIntegral_convergent :
∀ {s : ℝ}, 0 < s → MeasureTheory.IntegrableOn (fun x => (-x).exp * x ^ (s - 1)) (Set.Ioi 0) MeasureTheory.volume
The theorem `Real.GammaIntegral_convergent` states that for any positive real number `s`, the Euler integral for the gamma function, which is given by the expression `(-x).exp * x ^ (s - 1)` where `exp` is the exponential function, is integrable over the interval `(0, ∞)`. In other words, the integral of the function `(-x).exp * x ^ (s - 1)` from 0 to infinity exists and is finite. This integral is almost everywhere strongly measurable and its integral over this interval is less than infinity.
More concisely: The Euler integral for the gamma function, given by `(-x).exp * x ^ (s - 1)` for `s > 0`, is convergent over the interval `(0, ∞)`.
|
Real.Gamma_ne_zero
theorem Real.Gamma_ne_zero : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → s.Gamma ≠ 0
This theorem states that the Gamma function, denoted by Gamma, does not evaluate to zero for any real number `s` except at non-positive integers. At these non-positive integers, the Gamma function is not mathematically defined, hence we conventionally set it to `0`. In other words, for any real number `s` that is not the negative of a natural number `m` (represented as `-↑m` in Lean 4), the value of the Gamma function at `s` (denoted as `s.Gamma`) is not zero.
More concisely: The Gamma function is never zero for real numbers not equal to the negative of a natural number.
|
Real.Gamma_integrand_isLittleO
theorem Real.Gamma_integrand_isLittleO :
∀ (s : ℝ), (fun x => (-x).exp * x ^ s) =o[Filter.atTop] fun x => (-(1 / 2) * x).exp
This theorem states that for any real number `s`, the function `x => (-x).exp * x ^ s` is infinitesimally small compared to the function `x => (-(1 / 2) * x).exp` as `x` goes to infinity. In terms of Big O notation, it asserts that the Gamma function integrand, `(-x).exp * x ^ s`, is little o of `(-(1 / 2) * x).exp` when x tends to infinity. This means that the growth rate of `(-x).exp * x ^ s` is dominated by the growth rate of `(-(1 / 2) * x).exp` as x becomes sufficiently large.
More concisely: For any real number `s`, as `x` approaches infinity, `(-x).exp * x^s` is infinitesimally small compared to `(-(1/2)*x).exp`, or equivalently, `(-x).exp * x^s` is little o of `(-(1/2)*x).exp` in Big O notation.
|
Mathlib.Analysis.SpecialFunctions.Gamma.Basic._auxLemma.4
theorem Mathlib.Analysis.SpecialFunctions.Gamma.Basic._auxLemma.4 : ∀ {z w : ℝ}, (↑z = ↑w) = (z = w)
This theorem, which resides in the `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` namespace and is named `_auxLemma.4`, states that for any two real numbers `z` and `w`, the assertion that their complex number equivalents are equal is equivalent to the assertion that `z` and `w` themselves are equal. In other words, a real number `z` equals to a real number `w` if and only if the complex representation of `z` equals to the complex representation of `w`.
More concisely: The real numbers `z` and `w` are equal if and only if their complex number representations are equal.
|
Complex.GammaIntegral_add_one
theorem Complex.GammaIntegral_add_one : ∀ {s : ℂ}, 0 < s.re → (s + 1).GammaIntegral = s * s.GammaIntegral
This theorem states that for any complex number `s` with a positive real part, the gamma integral (`Γ` integral) of `s + 1` is equal to `s` multiplied by the gamma integral of `s`. This corresponds to the recurrence relation for the gamma function in complex analysis.
More concisely: For complex numbers `s` with positive real part, the gamma function `Γ(s + 1)` equals `Γ(s) * s`.
|
Complex.partialGamma_add_one
theorem Complex.partialGamma_add_one :
∀ {s : ℂ}, 0 < s.re → ∀ {X : ℝ}, 0 ≤ X → (s + 1).partialGamma X = s * s.partialGamma X - ↑(-X).exp * ↑X ^ s := by
sorry
This theorem describes the recurrence relation for the complex partial gamma function. For any complex number `s` with a positive real part and for any non-negative real number `X`, the value of the partial gamma function at `s + 1` and `X` equals the product of `s` and the partial gamma function at `s` and `X`, minus `e` to the power of `-X` times `X` to the power of `s`.
More concisely: The complex partial gamma function satisfies the recurrence relation: (s + 1)Γ(s + 1, X) = sΓ(s, X) - X^s * e^(-X), where s has a positive real part and X is non-negative.
|
Real.Gamma_one
theorem Real.Gamma_one : Real.Gamma 1 = 1
This theorem states that the Gamma function of 1 (`Real.Gamma 1`) is equal to 1. In the context of real numbers, the Gamma function, denoted as Γ(s), is a special function that generalizes the factorial function. For this theorem, when the input to the Gamma function is 1, the output is also 1.
More concisely: The Gamma function equals 1 for the input of 1, i.e., `Real.Gamma 1 = 1`.
|
Real.Gamma_pos_of_pos
theorem Real.Gamma_pos_of_pos : ∀ {s : ℝ}, 0 < s → 0 < s.Gamma
This theorem states that for all real numbers `s`, if `s` is greater than 0, then the real Gamma function of `s` is also greater than 0. Specifically, the Gamma function, denoted as `Real.Gamma`, is a function mapping from the set of real numbers to the set of real numbers and is defined as the real part of the Complex Gamma function evaluated at `s`.
More concisely: For all real numbers `s` greater than 0, the real Gamma function `Real.Gamma s` is positive.
|
Complex.GammaIntegral_convergent
theorem Complex.GammaIntegral_convergent :
∀ {s : ℂ},
0 < s.re → MeasureTheory.IntegrableOn (fun x => ↑(-x).exp * ↑x ^ (s - 1)) (Set.Ioi 0) MeasureTheory.volume
The theorem `Complex.GammaIntegral_convergent` states that for any complex number `s` with a positive real part (`0 < s.re`), the integral that defines the Gamma function converges. This integral is over the interval (0, ∞) and the integrand is the function `x ↦ exp(-x) * x^(s - 1)`. This is proved by reducing it to the analogous statement in the real case.
More concisely: For complex numbers `s` with positive real part, the integral of `exp(-x) * x^(s - 1)` over the interval (0, ∞) converges.
|
Real.integral_rpow_mul_exp_neg_mul_Ioi
theorem Real.integral_rpow_mul_exp_neg_mul_Ioi :
∀ {a r : ℝ}, 0 < a → 0 < r → ∫ (t : ℝ) in Set.Ioi 0, t ^ (a - 1) * (-(r * t)).exp = (1 / r) ^ a * a.Gamma := by
sorry
The theorem `Real.integral_rpow_mul_exp_neg_mul_Ioi` states that for any positive real numbers `a` and `r`, the integral over the interval (0, ∞) of the function `t ^ (a - 1) * exp (-(r * t))` with respect to `t` is equal to `(1 / r) ^ a * Gamma(a)`, where `Gamma(a)` refers to the Gamma function. In mathematical notation, this can be represented as ∫₀⁺ t^(a - 1) * exp(-rt) dt = (1 / r) ^ a * Γ(a).
More concisely: The integral of `t ^ (a - 1) * exp(-rt)` with respect to `t` over the interval (0, ∞) equals `(1 / r) ^ a * Gamma(a)`.
|
Real.Gamma_neg_nat_eq_zero
theorem Real.Gamma_neg_nat_eq_zero : ∀ (n : ℕ), (-↑n).Gamma = 0
The theorem `Real.Gamma_neg_nat_eq_zero` states that for any natural number `n`, the Gamma function evaluated at `-n` is undefined and, by convention, we assign it the value `0`. Here, `(-↑n).Gamma` signifies the Gamma function evaluated at the negative of the natural number `n`. Essentially, this theorem is acknowledging the discontinuities of the Gamma function at all non-positive integers by setting its value to `0` at these points.
More concisely: For any natural number `n`, `(-↑n).Gamma = 0` by convention.
|
Real.Gamma_zero
theorem Real.Gamma_zero : Real.Gamma 0 = 0
This theorem states that for the Gamma function on real numbers, the value at `0` is undefined. However, by convention, we assign this undefined value to be `0`. In other words, the Gamma function of `0` (`Γ(0)` in mathematical notation) is defined to be `0`.
More concisely: The Gamma function, which is undefined at 0 in its traditional definition, is conventionally assigned the value 0.
|