Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

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 objectLean nameCorrespondence
Defs.kummerCoeffAscending Pochhammer evaluations divided by the lower Pochhammer evaluation and factorial.
Defs.kummerThe infinite real series with these coefficients.
Middle ratio in (10) and (11)Defs.ratioExactly .
Positive-ray clauseDefs.claim, Result.resultEvery and ; strict decrease and image .
Negative-ray clauseDefs.claim, Result.resultEvery 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_betaIntegral and Asymptotics.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_strictAntiOn allows 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.