Metadata
slug: baricz-ponnusamy-vuorinen-2011-gamma-gamma-nbu
bibkey: bariczponnusamyvuorinen2011functional
doi: 10.1016/j.exmath.2011.07.001
triage: theorem
motivation_gids:
- D5/S3/Analytic/GammaGammaNBU/Result.result
url: https://arxiv.org/abs/1009.4814v2
A counterexample to the gamma-gamma NBU assertion
Problem
Á. Baricz, S. Ponnusamy and M. Vuorinen, Functional inequalities for modified Bessel functions, Expo. Math. 29(4) (2011), 399–414, DOI 10.1016/j.exmath.2011.07.001, arXiv:1009.4814v2, Question 8, printed p. 13:
Question 8. Is it true that the gamma-gamma distribution satisfies the NBU property?
The preceding definition, printed p. 13, reads:
By definition a life distribution satisfies the new-is-better-than-used (NBU) property if u ↦ log F̄(u) is sub-additive, i.e.
for all u₁, u₂ > 0.
The density, §4, printed p. 10, is introduced as follows:
The probability density function fₐ,ᵦ,α : (0, ∞) → (0, ∞) of the three parameter gamma-gamma random variable is defined by (see [21])
where a, b > 0 are the distribution shaping parameters, Kν stands for the modified Bessel function of the second kind, and α > 0 is the mean of the gamma-gamma random variable.
Formal reading
Lean names have prefix D5.S3.Analytic.GammaGammaNBU.Result.
| Source object | Lean name | Correspondence |
|---|---|---|
| Modified Bessel function of the second kind | besselK | DLMF 10.32.9: , for real and . |
| Source density | density | The displayed density with Real.Gamma, real powers and nonnegative square root. |
| Survival function | survival | The Lebesgue integral of the density over . |
| Universal NBU assertion | claim | Every and every . |
| Refutation | result | Exactly . |
Only positive arguments occur in the counterexample. The total real functions outside the source domains impose no additional hypotheses and do not change the universally quantified positive-domain assertion.
Motivation
The settling declaration is D5/S3/Analytic/GammaGammaNBU/Result.result.
The source notes are D5/L/Asymptotics/bariczponnusamyvuorinen2011functional
and D5/L/Asymptotics/nist2026dlmfbesselkintegral.
A product of two exponential random variables is already a gamma-gamma
law, and supplies a counterexample to the universal reliability assertion.
Gap
The universal assertion is false at , . At these parameters the source density is and the survival function is
The counterexample concerns Question 8’s universal positive parameter range. It gives no sufficient condition for NBU in other parameter ranges.
Route
Writing in the whole-line hyperbolic integral gives
The integrand is nonnegative. Its integral in is , which is bounded by for . This proves the product integrability needed for Fubini and yields the displayed survival identity.
The function increases up to and decreases afterwards. Lower sums use 200 cells of width on ; upper sums use 96 cells of width . The upper cell containing is bounded by , since and . Each exponential bound follows from a six-term Taylor enclosure at , raised to the 32nd power. The tail is at most . Consequently,
Falsifier
The single positive parameter choice above violates the NBU inequality. An error in the source density, hyperbolic integral substitution, Fubini integrability or the directions of the finite-sum bounds would invalidate the formal refutation.
Evidence
PROVED. D5.S3.Analytic.GammaGammaNBU.Result.result states .
The theorem uses the exact density and survival definitions above.
The immutable experiment directory contains the following independent numerical checks.
- COMPUTED.
python3 gg-cert.py, exit 0; SHA-2560decfbf57b0ba234cffabbaf925a551a2f224080d0533407a05c650287e3059d. The script checks its enclosure against the alternating Taylor sums . Outward-rounded rational quadrature at gives and and verifies the strict reverse NBU inequality by exact rational comparison. These displayed decimals abbreviate the rational endpoints. - COMPUTED.
python3 gg-scan.py, exit 0; SHA-256a80cf34185f9b0d087de7300f0196f80392738c4f60c16fbcb0e154e4a6212c7; mpmath precision 30 decimal digits. At the total mass prints as 1.0. Direct density integration and the Bessel closed form both give . For the printed values of are respectively .
The supplied literature check found no settlement of Question 8 in the searched citations, Formal Conjectures or conjectures.io. The supplied check of Salazar, arXiv:2607.05538, concerns Questions 1, 2 and 7, and does not settle Question 8. This bounded scope establishes neither exhaustive coverage nor priority.
Triage
What the settlement shows
NBU implies NBUE, and NBUE implies when the moments are finite. These are standard reliability implications; see Barlow and Proschan, Statistical Theory of Reliability and Life Testing: Probability Models (Holt, Rinehart and Winston, 1975), for the NBU and NBUE classes. Their mechanism can also be seen directly. Put . Integration of in gives , the NBUE tail inequality. Integration in , with Tonelli, gives .
The product-gamma construction in the source’s §4, with the ordinary Gamma moment recurrence, gives and . Indeed, independent unit-mean Gamma variables of shapes have second moments , and multiplication and scaling by give the formula. The source cites P. S. Bithas, N. C. Sagias, P. T. Mathiopoulos, G. K. Karagiannidis and A. A. Rontogiannis, “On the performance analysis of digital communications over generalized-K fading channels,” IEEE Communications Letters 10 (2006), 353–355, for this construction. Thus NBU fails whenever . At the ratio is , strictly above the NBU threshold . This consequence is a prose derivation, not a Lean theorem of this module.
- PROVED.
D5.S3.Analytic.GammaGammaNBU.Result.resultrefutes the universal assertion by the single witness . - COMPUTED. The certificate and six-point scan above concern only . The scan is not a continuous-parameter classification.
- OPEN. The range is not classified here. Avoiding the second-moment obstruction does not prove NBU.
- OPEN. The other questions of the source are not settled by this module. Its existing theorems retain their stated parameter hypotheses; the proposed universal route through log-concavity cannot establish NBU in the second-moment obstruction range.
ASSUMED-UNVERIFIED
Exhaustive literature coverage, priority and citation-index completeness are unverified. No new network literature search is asserted. The standard reliability implications and the product-Gamma moment calculation are given in prose; only the fixed counterexample is proved by the Lean module. The scan’s finite-precision values are numerical observations, not certified uniform bounds.