Metadata

slug: boudabsa-simon-2021-kilbas-saigo-hyperbolic-bounds
bibkey: boudabsasimon2021kilbassaigo
doi: 10.3390/math9030217
triage: theorem
motivation_gids:
  - D5/S3/Analytic/KilbasSaigo/Result.result
url: https://arxiv.org/abs/2012.05666

Hyperbolic bounds for the Kilbas–Saigo function

Problem

Boudabsa and Simon, Some properties of the Kilbas–Saigo function, arXiv:2012.05666v1, §4.1, Conjecture 4.5 (Conjecture 4 in the journal):

For every α ∈ (0, 1], m > 0, l > m − 1/α and x ≥ 0, one has 1/(1 + [Γ(1+α(l−m))/Γ(1+α(l−m+1))] x) ≤ E_{α,m,l}(−x) ≤ 1/(1 + [Γ(1+αl)/Γ(1+α(1+l))] x).

Here

$E_{α, m, l} (z) = n = 0 \sum \infty c_{n} z^{n}, c_{n} = k = 0 \prod n - 1 \frac{Γ ( 1 + α ( km + l ))}{Γ ( 1 + α ( km + l + 1 ))}, c_{0} = 1.$

The source records the cases $l = m - 1$ and $m = 1$ as known.

Formal reading

All Lean names below have prefix D5.S3.Analytic.KilbasSaigo.

Source object	Lean name	Correspondence
$c_{n}$	`Defs.ksCoeff`	The product over $0 \leq k < n$ , including the empty product at $n = 0$ .
$E_{α, m, l} (z)$	`Defs.kilbasSaigo`	The real sum of $c_{n} z^{n}$ ; `Series.summable_kilbasSaigo` proves convergence for every real $z$ .
$a = 1 + α (l - m)$ , $b = α m$ , $ϕ (s) = Γ (a + b s + α) /Γ (a + b s)$	`Series.phi`	The hypotheses imply $a, b > 0$ and positivity of every Gamma argument used.
$f (x) = E_{α, m, l} (- x)$	`Series.g` at order zero	`Series.kilbasSaigo_neg_eq_g0` identifies the two series.
$g_{k} = (- 1)^{k} f^{(k)}$	`Series.g`	`Series.hasDerivAt_g` gives $g_{k}^{'} = - g_{k + 1}$ for every natural $k$ .
Both bounds and their quantifiers	`Defs.claim`, `Result.result`	All real $α, m, l, x$ with exactly the five displayed hypotheses; both inequalities are non-strict.

The settling declaration is D5/S3/Analytic/KilbasSaigo/Result.result. The source note is D5/L/Asymptotics/boudabsasimon2021kilbassaigo. The bounds compare an entire special function with two explicit rational functions throughout the nonnegative argument range.

Gap

Status: Proved for the complete stated range, including $α = 1$ and $x = 0$ . The strict inequality $l > m - 1/ α$ is retained. The equality $l = m - 1/ α$ is outside this statement.

Route

Put $a = 1 + α (l - m) > 0$ , $b = α m > 0$ and $ϕ (s) = Γ (a + b s + α) /Γ (a + b s)$ . The coefficient recurrence is $c_{n + 1} = c_{n} / ϕ (n + 1)$ . A beta integral and dominated convergence give $1/ ϕ (n) \to 0$ . The ratio criterion gives absolute convergence of every signed derivative series at every real argument, and uniform local bounds justify differentiation.

For $0 < α < 1$ , set $λ = r^{b}$ and

$K (r) = \frac{α}{Γ ( 1 - α )} r^{a + α - 1} (1 - r)^{- 1 - α}, 0 < r < 1.$

The divided difference of $r^{q}$ regularizes the endpoint at one. The fundamental theorem of calculus and beta integrals yield, for $q \geq 0$ ,

$\int_{0}^{1} (1 - r^{q}) K (r) d r = \frac{Γ ( a + q + α )}{Γ ( a + q )} - \frac{Γ ( a + α )}{Γ ( a )} .$

The estimate $∣1 - λ^{n} ∣ \leq n (1 - λ)$ and the absolutely convergent derivative series justify integration term by term. Thus

$(ϕ (0) + x) f (x) = ϕ (0) + \int_{0}^{1} [f (λ x) - f (x)] K (r) d r,$

$(ϕ (k) + x) g_{k} (x) = k g_{k - 1} (x) + \int_{0}^{1} λ^{k} [g_{k} (λ x) - g_{k} (x)] K (r) d r (k \geq 1) .$

A nonpositive minimum on $[0, x]$ makes the integral at that minimum nonnegative, contradicting the strictly positive forcing. Induction proves $g_{k} > 0$ for every $k$ , hence $f$ is decreasing and convex. Monotonicity gives $(ϕ (0) + x) f (x) \geq ϕ (0)$ . Convexity gives

$0 \leq f (λ x) - f (x) \leq (1 - λ) (1 - f (x)) .$

Since $\int_{0}^{1} (1 - λ) K = ϕ (1) - ϕ (0)$ , this yields $(ϕ (1) + x) f (x) \leq ϕ (1)$ .

At $α = 1$ , $ϕ (s) = a + b s$ . The coefficient recurrence gives

$b x f^{'} (x) + (a + x) f (x) = a, b x g_{k}^{'} (x) + (a + bk + x) g_{k} (x) = k g_{k - 1} (x) .$

The left derivative at a positive minimizer and the positive initial values exclude a nonpositive minimum, successively for all $g_{k}$ . The ODE, $f^{'} \leq 0$ and the convex tangent inequality $f (x) - x f^{'} (x) \leq f (0) = 1$ give the same two bounds. Rewriting $ϕ (0)$ and $ϕ (1)$ gives the two pinned Gamma quotients.

Falsifier

Real parameters satisfying $0 < α \leq 1$ , $m > 0$ , $l > m - 1/ α$ and $x \geq 0$ for which either displayed inequality fails would contradict the statement. Equality at $x = 0$ and the endpoint $α = 1$ are included.

Evidence

D5/S3/Analytic/KilbasSaigo/Result.result proves exactly Defs.claim. Its principal dependency is Bounds.bounds, using Bounds.bounds_one and the fractional scaling hierarchy. The analytic dependencies include Series.tendsto_inv_phi, Series.summable_gCoeff, Series.hasDerivAt_g, Bounds.FractionalCertificate.certificate_full, Bounds.ScalingWork.scaling_f, Bounds.ScalingWork.scaling_g_succ, Bounds.fractional_system, Bounds.ode_one_base and Bounds.ode_one_succ. The latter analytic helpers are private declarations in Bounds.lean. The axiom closure of Result.result is {propext, Classical.choice, Quot.sound}.

The proof route was derived with the assistance of the ChatGPT Pro model. No settlement was found in the bounded literature scope for Boudabsa, Simon, Kilbas–Saigo and hyperbolic bounds, including work from 2023–2026. Koide, Figshare 10.6084/m9.figshare.34328784.v1, concerns the boundary Conjecture 3.7 at $l = m - 1/ α$ , a different statement. Karp–Kuznetsov, arXiv:2403.05708, §6, supplies representations; Beghin–Leonenko–Simon–Vaz, arXiv:2606.03661, cites the source without settling this conjecture. The repository’s mathematical sources, literature notes, problem dossiers and pull requests supplied no earlier Kilbas–Saigo settlement in that scope. This bounded scope does not establish exhaustive citation-index coverage or priority.

Triage

PROVED. Positivity of $f$ and every signed derivative on $[0, \infty)$ follows from Bounds.fractional_system for $0 < α < 1$ and Bounds.g_positive_one for $α = 1$ , together with Series.hasDerivAt_g. The public Bounds.pos_decreasing_convex gives the first three signs used for monotonicity and convexity.
PROVED. The scaling equations are Bounds.ScalingWork.scaling_f and Bounds.ScalingWork.scaling_g_succ, instantiated in Bounds.fractional_system. The endpoint ODEs are Bounds.ode_one_base and Bounds.ode_one_succ.
PROVED in prose. Both constants are optimal. The series gives $f^{'} (0) = - 1/ ϕ (1)$ , forcing any upper bound $C / (C + x)$ to have $C \geq ϕ (1)$ . Also $x f (x) \to ϕ (0)$ , forcing any lower bound $C / (C + x)$ to have $C \leq ϕ (0)$ . For the fractional case, the upper bound gives $f (x) \to 0$ , and the chord inequality dominates the scaling integrand by $(1 - λ) K$ , an integrable function. Its pointwise limit is zero, so dominated convergence in the scaling equation proves the claimed limit. At $α = 1$ , convexity gives $0 \leq - x f^{'} (x) \leq 2 (f (x /2) - f (x)) \leq 2 f (x /2) \to 0$ ; the ODE then gives $x f (x) \to a = ϕ (0)$ .
PROVED in prose. The argument applies to any coefficient sequence $c_{n} = \prod_{j = 1}^{n} ϕ (j)^{- 1}$ with $ϕ (s) = A + d s + \int_{0}^{1} (1 - λ^{s}) K (λ) d λ$ , $A > 0$ , $d \geq 0$ , $K \geq 0$ , $\int_{0}^{1} (1 - λ) K < \infty$ and $ϕ (n) \to \infty$ . The ratio criterion again gives every derivative series. The same first-moment majorant gives the scaling hierarchy with the extra drift term $d x g_{k}^{'}$ . At a nonpositive minimum the left derivative is nonpositive, while the integral difference and forcing have the opposite sign, proving all signed derivatives positive. The lower bound follows from $f^{'} \leq 0$ . For the upper bound, the chord bounds the integral by $(ϕ (1) - A - d) (1 - f)$ and the tangent gives $- d x f^{'} \leq d (1 - f)$ ; their sum gives $(ϕ (1) + x) f \leq ϕ (1)$ .
OPEN. The boundary $l = m - 1/ α$ , the source’s Conjecture 3.7, is not covered by this result.

ASSUMED-UNVERIFIED

Exhaustive literature coverage, citation-index completeness and priority are unverified. The bounded literature scope does not imply that no other settlement exists.

trureturing — Discovering truth