Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma
theorem Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma :
∀ {s t a b : ℝ}, 0 < s → 0 < t → 0 < a → 0 < b → a + b = 1 → (a * s + b * t).Gamma ≤ s.Gamma ^ a * t.Gamma ^ b := by
sorry
This theorem states that the Gamma function, when applied to the positive real numbers, exhibits log-convexity in its multiplicative form. Specifically, given any positive real numbers `s`, `t`, `a`, and `b` such that `a + b` equals `1`, the Gamma function of `(a * s + b * t)` is less than or equal to the product of `s.Gamma` raised to the power of `a` and `t.Gamma` raised to the power of `b`. The proof of this theorem involves the use of the Hölder inequality applied to Euler's integral.
More concisely: The Gamma function, when applied to positive real numbers, satisfies the multiplicative log-convexity property: for any `s`, `t`, `a`, and `b` with `a + b = 1`, `a.Gamma(s) ^ b.Gamma(t) >= Gamma(a.s + b.t)`.
|
Real.Gamma_mul_Gamma_add_half_of_pos
theorem Real.Gamma_mul_Gamma_add_half_of_pos :
∀ {s : ℝ}, 0 < s → s.Gamma * (s + 1 / 2).Gamma = (2 * s).Gamma * 2 ^ (1 - 2 * s) * Real.pi.sqrt
This theorem is a version of Legendre's duplication formula for the Gamma function, but specifically for positive real arguments. It states that for any positive real number `s`, the product of the Gamma function of `s` and the Gamma function of `s + 1/2` equals the Gamma function of `2s` times `2` raised to the power `(1 - 2s)` times the square root of Pi. This result serves as an intermediate step, and it will be later superseded by a more general theorem `Real.Gamma_mul_Gamma_add_half` that applies to all real numbers `s`, not just the positive ones.
More concisely: For any positive real number `s`, $\Gamma(s) \cdot \Gamma(s + \frac{1}{2}) = \sqrt{\pi} \cdot \Gamma(2s) \cdot 2^{1-2s}$.
|
Real.BohrMollerup.f_add_nat_ge
theorem Real.BohrMollerup.f_add_nat_ge :
∀ {f : ℝ → ℝ} {x : ℝ} {n : ℕ},
ConvexOn ℝ (Set.Ioi 0) f →
(∀ {y : ℝ}, 0 < y → f (y + 1) = f y + y.log) → 2 ≤ n → 0 < x → f ↑n + x * (↑n - 1).log ≤ f (↑n + x)
The theorem `Real.BohrMollerup.f_add_nat_ge` states that for any function `f` from real numbers to real numbers, any real number `x`, and any natural number `n`, if `f` is convex on the set of real numbers greater than 0 and for any real number `y` greater than 0, `f(y + 1)` equals `f(y) + y.log`, then if `n` is greater than or equal to 2 and `x` is greater than 0, `f(n) + x * (n - 1).log` is less than or equal to `f(n + x)`.
More concisely: Given a convex function `f` from real numbers to real numbers satisfying `f(y + 1) = f(y) + y.log` for all `y > 0`, for any `x > 0` and `n >= 2`, it holds that `f(n) + x * (n - 1).log ≤ f(n + x)`.
|
Real.BohrMollerup.f_add_nat_le
theorem Real.BohrMollerup.f_add_nat_le :
∀ {f : ℝ → ℝ} {x : ℝ} {n : ℕ},
ConvexOn ℝ (Set.Ioi 0) f →
(∀ {y : ℝ}, 0 < y → f (y + 1) = f y + y.log) → n ≠ 0 → 0 < x → x ≤ 1 → f (↑n + x) ≤ f ↑n + x * (↑n).log
The theorem `Real.BohrMollerup.f_add_nat_le` asserts that for all real-valued functions `f`, real numbers `x`, and natural numbers `n`, if `f` is a convex function on the interval `(0, ∞)`, and for all `y > 0`, `f(y + 1) = f(y) + y.log`, and if `n` is not zero and `0 < x ≤ 1`, then `f(n + x)` is less than or equal to `f(n) + x * log(n)`. This is a statement about a linear upper bound condition for the function `f` evaluated at `x + n` on the unit interval.
More concisely: If `f` is a convex function on `(0, ∞)` satisfying `f(y + 1) = f(y) + y.log` for all `y > 0`, then for `n ∈ ℕ` and `0 < x ≤ 1`, `f(n + x) ≤ f(n) + x * log(n)`.
|
Real.eq_Gamma_of_log_convex
theorem Real.eq_Gamma_of_log_convex :
∀ {f : ℝ → ℝ},
ConvexOn ℝ (Set.Ioi 0) (Real.log ∘ f) →
(∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y) →
(∀ {y : ℝ}, 0 < y → 0 < f y) → f 1 = 1 → Set.EqOn f Real.Gamma (Set.Ioi 0)
The Bohr-Mollerup theorem states that the Gamma function is the unique function on the positive real numbers that satisfies the following properties: it is log-convex, takes positive values, equals 1 at the point 1, and satisfies the functional equation `f (x + 1) = x * f x` for all `x`. In other words, for any function `f` from the set of real numbers to the set of real numbers, if `f` is log-convex on the open interval (0, ∞), satisfies the property that `f (y + 1) = y * f y` for all `y > 0`, takes positive values for all `y > 0`, and also satisfies `f 1 = 1`, then `f` must be equal to the Gamma function on the interval (0, ∞).
More concisely: The Gamma function is the unique log-convex function on (0, ∞) that satisfies Gamma (x + 1) = x * Gamma x and Gamma 1 = 1.
|