Complex.betaIntegral_recurrence
theorem Complex.betaIntegral_recurrence :
∀ {u v : ℂ}, 0 < u.re → 0 < v.re → u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
This theorem demonstrates the recurrence formula for the Beta function over complex numbers. For any two complex numbers 'u' and 'v', where the real part of 'u' and 'v' is greater than 0, the theorem states that the product of 'u' and the Beta function of 'u' and 'v+1' equals the product of 'v' and the Beta function of 'u+1' and 'v'.
More concisely: For complex numbers u and v with positive real parts, u * Beta(u, v+1) = v * Beta(u+1, v).
|
Complex.Gamma_mul_Gamma_eq_betaIntegral
theorem Complex.Gamma_mul_Gamma_eq_betaIntegral :
∀ {s t : ℂ}, 0 < s.re → 0 < t.re → s.Gamma * t.Gamma = (s + t).Gamma * s.betaIntegral t
This theorem establishes a relationship between the Beta integral and the Gamma function in complex analysis. For any two complex numbers `s` and `t` where the real parts of both `s` and `t` are positive, the product of the Gamma functions of `s` and `t` equals the product of the Gamma function of `s + t` and the Beta integral of `s` and `t`.
More concisely: For complex numbers `s` and `t` with positive real parts, $\Gamma(s) \Gamma(t) = \Gamma(s + t) \int\_0^1 x^{s-1} (1-x)^{t-1} dx$.
|
Real.Gamma_mul_Gamma_one_sub
theorem Real.Gamma_mul_Gamma_one_sub : ∀ (s : ℝ), s.Gamma * (1 - s).Gamma = Real.pi / (Real.pi * s).sin
This theorem states Euler's reflection formula for the real Gamma function. Specifically, for any real number `s`, the product of the Gamma function of `s` and the Gamma function of `(1 - s)` is equal to the value of π divided by the sine of π times `s`. This relationship holds true for all real numbers `s` and is a key property of the Gamma function in mathematics.
More concisely: The real Gamma function satisfies Euler's reflection formula: Γ(s) * Γ(1-s) = π / (sin(π * s)).
|
Complex.betaIntegral_convergent
theorem Complex.betaIntegral_convergent :
∀ {u v : ℂ},
0 < u.re → 0 < v.re → IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) MeasureTheory.volume 0 1
The theorem named 'Complex.betaIntegral_convergent' states that the Beta integral is convergent for all complex numbers `u` and `v` that have positive real parts. Specifically, the function that is being integrated is `x ^ (u - 1) * (1 - x) ^ (v - 1)`, over the interval from 0 to 1, with respect to the Lebesgue measure (denoted by `MeasureTheory.volume`). The Beta integral is said to be interval integrable, meaning it is integrable on both intervals `(0, 1]` and `(1, 0]`. Given that one of these intervals is always empty, this property is equivalent to the function being integrable on `(0, 1]`.
More concisely: The Beta integral of the function `x ^ (u - 1) * (1 - x) ^ (v - 1)` over the interval [0, 1] with respect to Lebesgue measure is convergent for all complex numbers `u` and `v` with positive real parts.
|
Complex.Gamma_mul_Gamma_one_sub
theorem Complex.Gamma_mul_Gamma_one_sub : ∀ (z : ℂ), z.Gamma * (1 - z).Gamma = ↑Real.pi / (↑Real.pi * z).sin
This theorem is a statement of Euler's reflection formula for the complex Gamma function. It states that for any complex number `z`, the product of the Gamma function evaluated at `z` and the Gamma function evaluated at `1 - z` equals the real number π divided by the sine of π times `z`. The Gamma function here extends the factorial function to complex numbers. The reflection formula is significant in many areas of mathematics including functional analysis and number theory.
More concisely: The theorem asserts that for any complex number `z`, $\Gamma(z)\cdot \Gamma(1-z) = \frac{\pi}{\sin(\pi z)}$.
|
Complex.approx_Gamma_integral_tendsto_Gamma_integral
theorem Complex.approx_Gamma_integral_tendsto_Gamma_integral :
∀ {s : ℂ},
0 < s.re →
Filter.Tendsto (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) Filter.atTop (nhds s.Gamma)
This theorem, labeled as `Complex.approx_Gamma_integral_tendsto_Gamma_integral`, states that for any complex number `s` with a positive real part, the sequence of integrals given by the expression `∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)` tends to the Gamma function of `s` as `n` tends to infinity. In the integral expression, the integral range is from 0 to `n`, and the integrand is the product of the nth power of `(1 - x / n)` and `x` raised to the power `(s - 1)`, where `x` is a real number. The concept of "tending to" is formally defined using the `Filter.Tendsto` definition, with `Filter.atTop` representing the limit `n → ∞`, and `nhds s.Gamma` representing the filter of neighborhoods around the Gamma function of `s`. This theorem is a key technical lemma for proving that a certain sequence `GammaSeq` tends to the group `Gamma` under certain conditions.
More concisely: For any complex number `s` with positive real part, the sequence of integrals `∫ (x : ℝ) in 0 ..↑n, (1 - x / ↑n) ^ n * x ^ (s - 1) dx` converges to the Gamma function of `s` as `n` approaches infinity.
|
Complex.GammaSeq_tendsto_Gamma
theorem Complex.GammaSeq_tendsto_Gamma : ∀ (s : ℂ), Filter.Tendsto s.GammaSeq Filter.atTop (nhds s.Gamma)
This theorem, known as Euler's limit formula for the complex Gamma function, states that for every complex number `s`, the sequence of `s`'s Gamma function values (`s.GammaSeq`) tends towards the Gamma value of `s` (`s.Gamma`) as `s` approaches infinity. In other words, the Gamma function values of `s`, when `s` is large enough, get arbitrarily close to the Gamma value of `s`. This is expressed in Lean 4 using the `Filter.Tendsto` function, where `Filter.atTop` represents the notion of `s` approaching infinity, and `nhds s.Gamma` represents a neighborhood of the Gamma value of `s` in the topological space of complex numbers.
More concisely: For every complex number `s`, the sequence of `s.GammaSeq` converges to `s.Gamma` as `s` approaches infinity.
|
Complex.betaIntegral_convergent_left
theorem Complex.betaIntegral_convergent_left :
∀ {u : ℂ},
0 < u.re →
∀ (v : ℂ), IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) MeasureTheory.volume 0 (1 / 2)
The theorem `Complex.betaIntegral_convergent_left` states that for any complex number `u` with a positive real part and any complex number `v`, the function `f(x) = x^(u-1) * (1-x)^(v-1)` is interval integrable with respect to the Lebesgue measure on the interval from 0 to 1/2. This result is a key step towards proving the convergence of the beta integral at the left endpoint.
More concisely: The theorem `Complex.betaIntegral_convergent_left` asserts that the function `x => x^(Re(u) - 1) * (1 - x)^(Im(v) - 1)` is Lebesgue integrable over the interval [0, 1/2] when Re(u) > 0.
|
Complex.Gamma_ne_zero_of_re_pos
theorem Complex.Gamma_ne_zero_of_re_pos : ∀ {s : ℂ}, 0 < s.re → s.Gamma ≠ 0
This is a theorem regarding the gamma function in complex mathematics, specifically a simpler, more applicable version of the assertion that the gamma function does not equal zero, named `Complex.Gamma_ne_zero_of_re_pos`. It states that for any complex number `s`, if the real part of `s` is greater than zero, then the gamma function of `s` is not equal to zero. In other words, the gamma function of a complex number with a positive real part is never zero.
More concisely: For any complex number `s`, if the real part of `s` is positive, then $\Gamma(s) \neq 0$.
|
Complex.one_div_Gamma_eq_self_mul_one_div_Gamma_add_one
theorem Complex.one_div_Gamma_eq_self_mul_one_div_Gamma_add_one : ∀ (s : ℂ), s.Gamma⁻¹ = s * (s + 1).Gamma⁻¹
This theorem represents a reformulation of the Gamma function recurrence relation, which is also valid when `s = 0`. In mathematical terms, for any complex number `s`, the reciprocal of the Gamma function at `s` is equal to `s` multiplied by the reciprocal of the Gamma function at `s + 1`. This is denoted as `s.Gamma⁻¹ = s * (s + 1).Gamma⁻¹`.
More concisely: For any complex number `s`, the reciprocal of the Gamma function of `s` is equal to `s * (s + 1)^{-1} * Γ(s + 1)`, where `Γ` denotes the Gamma function.
|
Complex.differentiable_one_div_Gamma
theorem Complex.differentiable_one_div_Gamma : Differentiable ℂ fun s => s.Gamma⁻¹
The theorem states that the reciprocal of the Gamma function is differentiable at every point in the complex plane. This includes even those points where the Gamma function itself is not differentiable. Here, the Gamma function is a complex-valued function that generalizes the factorial function to complex and non-integer values. 'Differentiable' means that the function has a derivative at every point, i.e., it is smooth and has no sharp turns or corners.
More concisely: The reciprocal function of the complex Gamma function is complex differentiable at every point in the complex plane.
|
Complex.Gamma_ne_zero
theorem Complex.Gamma_ne_zero : ∀ {s : ℂ}, (∀ (m : ℕ), s ≠ -↑m) → s.Gamma ≠ 0
This theorem states that the Gamma function, denoted as `Γ`, does not yield a zero value for any complex number `s` in the complex plane `ℂ`, except at non-positive integers. In other words, the Gamma function does not vanish anywhere on the complex plane, unless the input `s` is a non-positive integer (including zero). By convention, for these non-positive integers, the Gamma function is mathematically undefined, so we set its value to `0`.
More concisely: The Gamma function `Γ(s)` never equals zero in the complex plane `ℂ`, except at non-positive integers where it is conventionally set to zero.
|
Complex.betaIntegral_eval_nat_add_one_right
theorem Complex.betaIntegral_eval_nat_add_one_right :
∀ {u : ℂ},
0 < u.re → ∀ (n : ℕ), u.betaIntegral (↑n + 1) = ↑n.factorial / (Finset.range (n + 1)).prod fun j => u + ↑j
This theorem provides an explicit formula for the Beta function in the complex plane when the second argument is a positive integer. For any complex number `u` with positive real part and any natural number `n`, the Beta function of `u` and `n + 1` is equal to the factorial of `n` divided by the product of `u` plus each natural number less than `n + 1`.
More concisely: For complex numbers `u` with positive real part and natural number `n`, the Beta function `β(u, n+1)` equals `fact(n) / prod(i in range (n+1), u + i)`.
|
Real.GammaSeq_tendsto_Gamma
theorem Real.GammaSeq_tendsto_Gamma : ∀ (s : ℝ), Filter.Tendsto s.GammaSeq Filter.atTop (nhds s.Gamma)
This theorem is a formalization of Euler's limit formula for the real Gamma function. For every real number `s`, it states that the sequence `s.GammaSeq`, when considered as tending towards infinity (`Filter.atTop`), converges to the value of the Gamma function at `s` (`s.Gamma`). Here, convergence is defined in the sense of filter theory: for every neighborhood of `s.Gamma` (which is an open set containing `s.Gamma`), there exists a point in the sequence beyond which all subsequent terms of the sequence lie within this neighborhood (`Filter.Tendsto`).
More concisely: For every real number `s`, the sequence `s.GammaSeq` converges to `s.Gamma` as `s` approaches infinity in the sense of filter theory. (Or: The limit of `s.GammaSeq` as `s` goes to infinity is `s.Gamma`.)
|