Metadata
slug: karp-sitnik-2010-kummer-ratio-monotonicity
bibkey: karpsitnik2010logconvexity
doi: 10.1016/j.jmaa.2009.10.057
triage: theorem
motivation_gids:
- D5/S3/Analytic/KummerRatio/Result.result
url: https://arxiv.org/abs/0902.3073
Monotonicity and exact ranges of the shifted Kummer ratio
Problem
Karp and Sitnik, Log-convexity and log-concavity of hypergeometric-like functions, arXiv:0902.3073v1, the unnumbered Conjecture after Theorem 4:
Conjecture. The ratio in the middle of (10) is monotone decreasing from (0, ∞) onto (1, A), where A is the left-hand side of (10); the ratio in the middle of (11) is monotone increasing from (−∞, 0) onto (B, 1), where B is the left-hand side of (11).
Write and
Theorem 4 assumes throughout. Its inequality (10), for and , is
Its inequality (11), for and , is
The printed “onto (1, A)” names the endpoints in the order , . The formal image is the open interval . On the negative ray the image is , with the displayed Gamma quotient as .
Formal reading
All Lean names below have prefix D5.S3.Analytic.KummerRatio.
| Source object | Lean name | Correspondence |
|---|---|---|
Defs.kummerCoeff | Ascending Pochhammer evaluations divided by the lower Pochhammer evaluation and factorial. | |
Defs.kummer | The infinite real series with these coefficients. | |
| Middle ratio in (10) and (11) | Defs.ratio | Exactly . |
| Positive-ray clause | Defs.claim, Result.result | Every and ; strict decrease and image . |
| Negative-ray clause | Defs.claim, Result.result | Every and ; strict increase and image . |
Motivation
The settling declaration is D5/S3/Analytic/KummerRatio/Result.result.
The source note is D5/L/Asymptotics/karpsitnik2010logconvexity.
The conclusion determines the full variation of the ratio in the real
argument, including the sharp Gamma endpoints in both parameter regimes.
Gap
Status: Proved for both clauses with the stated quantifiers. Both monotonicity conclusions are strict and both images are exact. Ratios with more than one upper parameter are outside this claim.
Route
For , the entire defining series solves and satisfies for . The logarithmic derivative satisfies
For , the weight gives
The weighted difference extends continuously to zero with value zero, so for . Put and . A second identity is
Its value at zero is again zero. Thus and .
For , the beta integral represents . Endpoint concentration gives . The contiguous relation extends this limit to every . The four limits in the ratio give . Continuity, , strict decrease and the intermediate value theorem give the image . Kummer’s transformation gives ; the positive-ray result therefore gives the negative-ray result and .
The comparison uses positivity on the closed positive ray, continuity of the solution and its first derivative there, and two derivatives satisfying the equation on the positive ray. The value at zero can be any positive normalization: the vanishing factor provides both zero boundary values in the weighted identities.
Falsifier
An admissible pair with , or an admissible
pair with , would contradict the respective
strict monotonicity clause. A ratio value outside the asserted interval,
or an interior value missing from the image, would contradict the exact
image clause of Result.result.
Evidence
D5/S3/Analytic/KummerRatio/Result.result proves exactly Defs.claim.
Its principal dependencies are Comparison.ratio_strictAntiOn,
Asymptotics.tendsto_kummer_atTop, Transform.kummer_transform,
Series.continuous_kummer, Series.one_le_kummer, and Series.kummer_zero.
The general ODE comparison is Comparison.solution_ratio_strictAntiOn;
the integral representation is BetaIntegral.kummer_eq_betaIntegral.
The accepted axiom closure of the result is contained in
{propext, Classical.choice, Quot.sound}.
The proof route was derived with the assistance of the ChatGPT Pro model. Mehrez–Sitnik, arXiv:1410.6120, Analysis 36 (2016), settles the related lower-parameter ratio . That is a different function. No settlement of the present conjecture was found in the bounded scope consisting of queries combining Karp, Sitnik, Kalmykov, Kummer ratio monotonicity and upper parameters; Karp–Zhang arXiv:2305.09029; Segura arXiv:2408.05573, Section 5; Derbazi arXiv:2607.02511; and the repository’s D5, Library, Problems and pull-request entries for Kummer, Karp, Sitnik and confluent hypergeometric functions. The existing Karp entry concerns polynomial truncations. This scope does not provide exhaustive citation-index or priority coverage.
Triage
- PROVED. The logarithmic-derivative ordering for
and the finite-increment comparison
hold for , under the regular
positive ODE-family hypotheses in Route. They are the internal comparison
steps used by
Comparison.solution_ratio_strictAntiOn. - PROVED. The beta-integral representation holds for .
The endpoint asymptotic
holds for all ,
by
BetaIntegral.kummer_eq_betaIntegralandAsymptotics.tendsto_kummer_atTop. - PROVED in prose. The comparison argument applies to any family of
positive solutions of with and the
regularity in Route, so it covers the ratios
for that ODE family. The Lean theorem
Comparison.solution_ratio_strictAntiOnallows arbitrary positive normalizations at zero and hence includes this normalized case. - OPEN. The analogous monotonicity in for the generalized hypergeometric ratio with upper parameters is not settled here.
ASSUMED-UNVERIFIED
Exhaustive literature coverage, priority and citation-index completeness are unverified. The full texts of the Sablica–Hornik papers in Mathematics of Computation 91 (2022) and Journal of Mathematical Analysis and Applications 537 (2024), concerning contiguous Kummer ratio bounds, were not read. No conclusion about their coverage of this conjecture is asserted.