Metadata

slug: mahmoud-mortici-2026-wallis-remainder-monotonicity
bibkey: mahmoudmortici2026wallisratio
doi: 10.1007/s00025-026-02697-2
triage: theorem
motivation_gids:
  - D5/S3/Analytic/WallisRemainder/Result.result
url: https://link.springer.com/article/10.1007/s00025-026-02697-2

Strict monotonicity of Wallis gamma remainders

Problem

Section 4, Open Question of the source identified in D5/L/Asymptotics/mahmoudmortici2026wallisratio asks:

Do the functions μ(x)=−x²−{(3/x)[ln(√x Γ(x+1/2)/Γ(x+1))]^{−1}+24}^{−1}, θ(x)=(23040x⁵/31){3x/(24x²+1)+ln(√x Γ(x+1/2)/Γ(x+1))}, χ(x)=(358400x⁷/257){(120x²+31)/(96x(10x²+3))+ln(√x Γ(x+1/2)/Γ(x+1))} satisfy the property that μ(x) and χ(x) are strictly increasing, while θ(x) is strictly decreasing for all x>0?

Formal reading

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

Source object	Lean name	Correspondence
$B (x) = x Γ (x + 1/2) /Γ (x + 1)$	`Defs.wallisB`	The exact real Gamma quotient.
$μ (x)$	`Defs.mu`	The displayed nested reciprocal, with exactly the constants 3 and 24.
$θ (x)$	`Defs.theta`	The displayed difference multiplied by $23040 x^{5} /31$ .
$χ (x)$	`Defs.chi`	The displayed difference multiplied by $358400 x^{7} /257$ .
Implicit reciprocal conditions	First conjunct of `Defs.claim`	For every $x > 0$ , $ln B (x) \neq = 0$ and $(3/ x) [ln B (x)]^{- 1} + 24 \neq = 0$ .
Strict monotonicity	Remaining conjuncts of `Defs.claim`	For every real $0 < x < y$ , $μ (x) < μ (y)$ , $θ (y) < θ (x)$ and $χ (x) < χ (y)$ .
Complete assertion	`Result.result : Defs.claim`	Unconditional theorem with no representation assumption.

The settling declaration is D5/S3/Analytic/WallisRemainder/Result.result. The source note is D5/L/Asymptotics/mahmoudmortici2026wallisratio. Strict monotonicity determines the direction of improvement of three normalized rational approximations to a Wallis-type Gamma quotient.

Gap

Status: Proved for every positive real argument, with all three strict comparisons and both reciprocal nonvanishing assertions. No assertion at a nonpositive argument is included.

Route

Put $r (x) = - ln B (x)$ . Gamma recurrence gives $r (x) + r (x + 1/2) = \frac{1}{2} ln ((x + 1/2) / x)$ . Log convexity gives $0 \leq r (x) \leq \frac{1}{2} ln ((x + 1/2) / x)$ , hence $r (x) \to 0$ . The convergent integral

$R (x) = \int_{0}^{\infty} e^{- x t} \frac{tanh ( t /4 )}{2 t} d t$

obeys the same half-step equation and tends to zero. The difference $r - R$ is periodic with period one and tends to zero, so $r = R$ .

The cotangent partial fractions on the imaginary axis yield

$\frac{tanh u}{u} = n \geq 0 \sum \frac{8}{π ^{2} ( 2 n + 1 ) ^{2} + 4 u ^{2}} .$

Let $w_{n} = 8/ (π^{2} (2 n + 1)^{2})$ and $a_{n} = 1/ (4 π^{2} (2 n + 1)^{2})$ . These weights sum to one. Mixing the laws of $a_{n} U^{2}$ with weights $w_{n}$ , where $U$ has density $e^{- u}$ on $u > 0$ , defines a probability law $P$ on $(0, \infty)$ . Termwise integration and the substitution $u = x t$ give

$r (x) = \frac{x}{8} S_{P} (x^{2}), S_{M} (z) = \int \frac{1}{z + v} d M (v) .$

The moments of $P$ are $1/24$ , $1/80$ and $17/1792$ . The size-biased probability law $d Q (v) = 24 v d P (v)$ has mean $3/10$ . The variances of $P, Q$ are respectively $31/2880$ and $771/5600$ .

For a positive probability law with mean $a$ and finite positive variance $σ^{2}$ , centering gives

$G_{M} (z) = \frac{z ^{3}}{σ ^{2}} (S_{M} (z) - \frac{1}{z + a}) = \frac{1}{σ ^{2}} \int (v - a)^{2} (\frac{z}{z + a})^{2} \frac{z}{z + v} d M (v) .$

The kernel is strictly increasing in $z > 0$ , and positive variance prevents its nonnegative multiplier from vanishing almost everywhere. Thus $G_{M}$ is strictly increasing. For any positive probability law not concentrated at one point, $H_{M} (z) = 1/ S_{M} (z) - z$ is also strictly increasing, without moment assumptions. An exact squared remainder for the two resolvents proves strictness: equality would force $v$ to be constant almost everywhere.

With $m = 1/24$ and $z = x^{2}$ , size biasing gives $z S_{P} (z) = 1 - m S_{Q} (z)$ . Exact algebra identifies

$θ (x) = - G_{P} (x^{2}), χ (x) = G_{Q} (x^{2}), μ (x) = H_{Q} (x^{2}) - m .$

Both transforms are strictly positive. Together with the size-bias identity and $r (x) = x S_{P} (x^{2}) /8$ , this proves both nonvanishing assertions. Squaring is strictly increasing on positive reals, giving all three comparisons.

Falsifier

A real pair $0 < x < y$ violating any of the three strict comparisons, or a positive $x$ at which either specified reciprocal denominator vanishes, would contradict the assertion. The complete positive ray is included.

Evidence

D5/S3/Analytic/WallisRemainder/Result.result proves exactly Defs.claim. Its principal dependencies are Measure.r_eq_stieltjes, Stieltjes.strictMonoOn_jensenRemainder and Stieltjes.strictMonoOn_inv_stieltjes_sub, with the positive-support, size-bias and moment theorems of Measure. The analytic representation uses Laplace.r_eq_laplace and Measure.tanh_div_hasSum. 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. The source proves continuity and boundedness of the remainders in Theorems 2.1–2.3 and leaves their monotonicity open in Section 4; Section 5 restates the question. No answer was found in the bounded literature scope covering the DOI, title, authors and the constants 23040 and 358400. Citation indexes were not checked exhaustively; this scope does not establish priority or exhaustive literature coverage.

Triage

PROVED. On $(0, \infty)$ , $μ$ and $χ$ are strictly increasing and $θ$ is strictly decreasing, with $ln B (x) \neq = 0$ and the inner bracket of $μ$ nonzero, by Result.result.
PROVED. For $x > 0$ , $r (x) = - ln B (x) = \int_{0}^{\infty} e^{- x t} tanh (t /4) / (2 t) d t$ , by Laplace.r_eq_laplace.
PROVED. For every probability measure on $(0, \infty)$ not concentrated at a point, $z \mapsto 1/ S (z) - z$ is strictly increasing, by Stieltjes.strictMonoOn_inv_stieltjes_sub. With finite positive variance and mean $a$ , the normalized Jensen remainder $z^{3} (S (z) - 1/ (z + a)) / σ^{2}$ is strictly increasing, by Stieltjes.strictMonoOn_jensenRemainder.
PROVED in prose. The endpoint limits are $μ (0 +) = 0$ , $μ (\infty) = 31/120$ , $θ (0 +) = 0$ , $θ (\infty) = - 1$ , $χ (0 +) = 0$ and $χ (\infty) = 1$ ; consequently the images are $(0, 31/120)$ , $(- 1, 0)$ and $(0, 1)$ respectively. At zero, continuity and positivity of Gamma at $1/2$ and $1$ give $ln B (x) = \frac{1}{2} ln x + O (1)$ , which yields all three zero limits directly from their definitions. At infinity, dominated convergence in the centered formula for $G_{M}$ above gives $G_{P}, G_{Q} \to 1$ . Also $H_{Q} (z) = E_{Q} [z V / (z + V)] / E_{Q} [z / (z + V)] \to 3/10$ , by domination by $V$ and $1$ , respectively. Thus $H_{Q} (z) - 1/24 \to 31/120$ . The defining expressions are continuous on the positive ray because their denominators are nonzero; the intermediate value theorem and strict monotonicity give the images.
OPEN. Complete monotonicity properties of endpoint differences or derivatives of these remainders are not established here. With the standard convention that a completely monotone function is nonnegative and nonincreasing, the three remainders themselves cannot all have that property: $μ, χ$ increase strictly and $θ < 0$ .

ASSUMED-UNVERIFIED

Exhaustive literature coverage, citation-index completeness and priority are unverified. No claim of exhaustive absence of another solution follows from the bounded literature scope.

trureturing — Discovering truth