The modified Bessel product need not be log-convex in its order

Abstract

Half-integer modified Bessel values contradict log-convexity in the order.

Definition 1.1 (The second-kind function at noninteger orders).

$\forall n u \in R, \forall u \in R, besselK (n u, u) = \frac{\frac{Real.pi}{2} \cdot ( besselI ( - n u , u ) - besselI ( n u , u ) )}{Real.sin ( n u \cdot Real.pi )}$

Formalization. D5/S3/Analytic/BesselProductOrderLogConvexity/Result.besselK (✓ std3).

Citation. NIST Digital Library of Mathematical Functions (2026). Modified Bessel Functions: Definitions and Basic Properties; Connection Formulas. URL: https://dlmf.nist.gov/10.25.

Commentary.

DLMF §10.25(ii), equation 10.25.2 (https://dlmf.nist.gov/10.25.E2), defines the first-kind function by: “I_ν(z) = (½z)^ν Σ_{k=0}^∞ (¼z²)^k / (k! Γ(ν+k+1)).” The page states that the principal branch of I_ν(z) “is analytic in ℂ∖(−∞,0]”.

The first-kind function besselI in every formula is the existing D5.S3.Analytic.BesselRatioLogConcavity.Result.besselI. At real z=u>0, the principal branch agrees with the real power: (u/2)^nu (u²/4)^k=(u/2)^(2k+nu). Thus the owner’s summand (u/2)^(2k+nu)/(k! Gamma(k+nu+1)) has exactly the DLMF normalization.

DLMF §10.27(ii), equation 10.27.4 (https://dlmf.nist.gov/10.27.E4), gives: “K_ν(z) = ½π (I_{−ν}(z) − I_ν(z)) / sin(νπ)”, followed by “When ν is an integer limiting values are taken”. Equation 10.27.1 (https://dlmf.nist.gov/10.27.E1) states: “I_{−n}(z) = I_n(z), n an integer.”

For positive u and noninteger nu, besselK is this standard connection formula with the same first-kind normalization. Lean’s real quotient is a total operation; only noninteger orders enter the assertion below, so no value assigned by that operation at an integer is used. Integer-order K values require the stated limiting convention and are outside this definition’s asserted correspondence.

Definition 1.2 (The product at a fixed argument).

$\forall u \in R, \forall n u \in R, P (u, n u) = besselI (n u, u) \cdot besselK (n u, u)$

Formalization. D5/S3/Analytic/BesselProductOrderLogConvexity/Result.P (✓ std3).

Citation. Á. Baricz and S. Ponnusamy (2013). On Turán type inequalities for modified Bessel functions. URL: https://arxiv.org/abs/1010.3346.

Commentary.

On printed p. 1 of arXiv:1010.3346v1, §1, Baricz and Ponnusamy write: “Let us denote with Iν and Kν the modified Bessel functions of the first and second kind, respectively. For definitions, recurrence formulas and other properties of modified Bessel functions of the first and second kind we refer to the classical book of G.N. Watson [Wa].”

The product is P(u,nu)=Iν(u)Kν(u). The argument u is its first parameter, while the order nu is its second parameter. The defining-series and connection-formula quotations above are from DLMF; the paper’s passage identifies the functions and refers the reader to Watson.

Definition 1.3 (The necessary midpoint product inequality).

$c l aim = (\forall u \in R, (0 < u) \Rightarrow (\forall n u \in R, \forall h \in R, (- 1 < n u) \Rightarrow ((0 < h) \Rightarrow ((\forall n \in Z, n u \neq = n) \Rightarrow ((\forall n \in Z, n u + h \neq = n) \Rightarrow ((\forall n \in Z, n u + 2 \cdot h \neq = n) \Rightarrow ((P (u, n u + h))^{2} \leq P (u, n u) \cdot P (u, n u + 2 \cdot h))))))))$

Formalization. D5/S3/Analytic/BesselProductOrderLogConvexity/Result.claim (✓ std3).

Citation. Á. Baricz and S. Ponnusamy (2013). On Turán type inequalities for modified Bessel functions. URL: https://arxiv.org/abs/1010.3346.

Commentary.

The final Conjecture in §3, printed page 7 of arXiv:1010.3346v1, reads: “Motivated by Theorems 1 and 2 we conjecture the following. Conjecture. The function ν ↦ I_ν(u)K_ν(u) is log-convex on (−1, ∞) for all u > 0 fixed.”

Theorem 1(4), printed page 4, states: “the function ν ↦ I_{√ν}(u)K_{√ν}(u) is log-convex on (0, ∞) for all u > 0 fixed;”

Theorem 2, printed page 6, with equation (19) joined to its sentence, states: “The function ν ↦ I_ν(u)K_ν(u) is decreasing and (0, ∞) for all u > 0 fixed. Moreover, for all ν ≥ 1/2 and u > 0 we have 2I_ν(u)K_ν(u) ≤ I_{ν−1}(u)K_{ν−1}(u) + I_{ν+1}(u)K_{ν+1}(u).” The word ‘and’ in the first sentence is retained from the source text.

For a positive function, log-convexity on (−1,∞) implies 2 log P(u,nu+h)≤log P(u,nu)+log P(u,nu+2h), hence P(u,nu+h)^2≤P(u,nu)P(u,nu+2h). The orders nu, nu+h and nu+2h all lie in the interval when nu>−1 and h>0. The formal assertion restricts to triples of noninteger orders, where the connection formula is valid. It is therefore weaker than the conjecture, and its refutation refutes the conjecture. The square-root parametrization in Theorem 1(4) is a different assertion.

Theorem 1.4 (The half-integer Gamma normalization).

$\forall k \in N, Nat.factorial (k) \cdot Real.Gamma (k + \frac{1}{2}) \cdot (4)^{k} = Nat.factorial (2 \cdot k) \cdot Real.sqrt (Real.pi)$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.gamma_factorial (✓ std3). ∎

Source. Repository-derived.

Commentary.

Mathlib’s Gamma duplication formula at k+1/2, together with the Gamma values at positive integers, gives the even-factorial identity after real-power normalization.

Theorem 1.5 (The terms at order minus one half).

$\forall k \in N, \frac{( \frac{1}{2} ) ^{2 \cdot k +- \frac{1}{2}}}{Nat.factorial ( k ) \cdot Real.Gamma ( k + - \frac{1}{2} + 1 )} = \frac{a}{Nat.factorial ( 2 \cdot k )}$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.minus_term (✓ std3). ∎

Source. Repository-derived.

Commentary.

The private real constant a is (1/2)^(−1/2)/sqrt(pi). The half-integer Gamma identity converts each defining term of I−1/2(1) into a/(2k)!. Natural indices in real expressions are coerced to real numbers.

Theorem 1.6 (The terms at order one half).

$\forall k \in N, \frac{( \frac{1}{2} ) ^{2 \cdot k + \frac{1}{2}}}{Nat.factorial ( k ) \cdot Real.Gamma ( k + \frac{1}{2} + 1 )} = \frac{a}{Nat.factorial ( 2 \cdot k + 1 )}$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.plus_term (✓ std3). ∎

Source. Repository-derived.

Commentary.

One Gamma step and one factorial step transform the order-one-half summand into a/(2k+1)!.

Theorem 1.7 (The elementary square-root factor).

$a = Real.sqrt (\frac{2}{Real.pi})$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.a_eq_sqrt (✓ std3). ∎

Source. Repository-derived.

Commentary.

The positive real-power factor (1/2)^(−1/2) divided by sqrt(pi) equals sqrt(2/pi). Positivity determines the square root uniquely.

Theorem 1.8 (The first two half-integer evaluations).

$(besselI (- \frac{1}{2}, 1) = Real.sqrt (\frac{2}{Real.pi}) \cdot Real.cosh (1)) \land (besselI (\frac{1}{2}, 1) = Real.sqrt (\frac{2}{Real.pi}) \cdot Real.sinh (1))$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.half_values (✓ std3). ∎

Source. Repository-derived.

Commentary.

Summing the even and odd factorial terms gives cosh(1) and sinh(1), respectively. The prefactor is sqrt(2/pi).

Theorem 1.9 (A Gamma recurrence for the summands).

$\forall n u \in R, \forall k \in N, (k + n u + 1 \neq = 0) \Rightarrow (summand (n u, k) = 2 \cdot (k + n u + 1) \cdot summand (n u + 1, k))$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.lower (✓ std3). ∎

Source. Repository-derived.

Commentary.

Here summand(nu,k) denotes the defining Bessel summand at argument one. The Gamma recurrence relates adjacent orders at the same index, provided k+nu+1 is nonzero.

Theorem 1.10 (An index-shift identity).

$\forall n u \in R, \forall k \in N, summand (n u + 2, k) = 2 \cdot (k + 1) \cdot summand (n u + 1, k + 1)$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.shift (✓ std3). ∎

Source. Repository-derived.

Commentary.

Increasing the natural index raises the exponent by two and the factorial by one step. A factor 2(k+1) relates the resulting summands.

Theorem 1.11 (The summand form of the order recurrence).

$\forall n u \in R, \forall k \in N, (k + 1 + n u + 1 \neq = 0) \Rightarrow (summand (n u, k + 1) = summand (n u + 2, k) + 2 \cdot (n u + 1) \cdot summand (n u + 1, k + 1))$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.step (✓ std3). ∎

Source. Repository-derived.

Commentary.

Combining the adjacent-order Gamma identity with the index shift gives the additive relation between three consecutive orders.

Theorem 1.12 (The order recurrence at argument one).

$\forall n u \in R, (- 2 < n u) \Rightarrow ((\forall k \in N, k + n u + 1 \neq = 0) \Rightarrow (besselI (n u, 1) = besselI (n u + 2, 1) + 2 \cdot (n u + 1) \cdot besselI (n u + 1, 1)))$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.recurrence (✓ std3). ∎

Source. Repository-derived.

Commentary.

For nu>−2 the series at nu+1 and nu+2 converge. The summand relation then proves convergence at nu and identifies its sum. Splitting off index zero yields Iν(1)=Iν+2(1)+2(nu+1)Iν+1(1). The nonzero hypotheses exclude the Gamma recurrence’s exceptional arguments.

Theorem 1.13 (The order minus three halves).

$besselI (- \frac{3}{2}, 1) = besselI (\frac{1}{2}, 1) - besselI (- \frac{1}{2}, 1)$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.recurrence_minus (✓ std3). ∎

Source. Repository-derived.

Commentary.

The order recurrence at nu=−3/2 expresses I−3/2(1) as I1/2(1)−I−1/2(1).

Theorem 1.14 (The order three halves).

$besselI (\frac{3}{2}, 1) = besselI (- \frac{1}{2}, 1) - besselI (\frac{1}{2}, 1)$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.recurrence_plus (✓ std3). ∎

Source. Repository-derived.

Commentary.

The order recurrence at nu=−1/2 expresses I3/2(1) as I−1/2(1)−I1/2(1). This is sqrt(2/pi)(cosh(1)−sinh(1)).

Theorem 1.15 (Three exact product values).

$(P (1, - \frac{1}{2}) = \frac{1 + Real.exp ( - 2 )}{2}) \land ((P (1, \frac{1}{2}) = \frac{1 - Real.exp ( - 2 )}{2}) \land (P (1, \frac{3}{2}) = 2 \cdot Real.exp (- 2)))$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.product_values (✓ std3). ∎

Source. Repository-derived.

Commentary.

The sine values at −pi/2, pi/2 and 3pi/2 are −1, 1 and −1. Substituting the four first-kind values into the connection formula gives P(1,−1/2)=(1+exp(−2))/2, P(1,1/2)=(1−exp(−2))/2 and P(1,3/2)=2exp(−2). The factor pi cancels the square 2/pi of the common prefactor.

Theorem 1.16 (A rational upper bound on the exponential).

$(0 < Real.exp (- 2)) \land (Real.exp (- 2) < \frac{1}{7})$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.exp_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exponential is positive. The lower bound exp(1)>8/3 implies exp(1)^2>7, so exp(−2)=1/exp(1)^2<1/7.

Theorem 1.17 (The strict reversal of the midpoint inequality).

$P (1, - \frac{1}{2}) \cdot P (1, \frac{3}{2}) < (P (1, \frac{1}{2}))^{2}$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

Put t=exp(−2). The product difference is (1+t)t−(1−t)^2/4=(3t^2+6t−1)/4. A rational bound on exp(1) gives an upper bound on t for which this expression is strictly negative.

Theorem 1.18 (Half-integer orders are noninteger).

$\forall k \in Z, \forall n \in Z, (Int.cast (k) : R) + \frac{1}{2} \neq = (Int.cast (n) : R)$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.half_noninteger (✓ std3). ∎

Source. Repository-derived.

Commentary.

For integers k and n, the real number k+1/2 differs from n because doubling would equate an odd integer with an even one.

Theorem 1.19 (Refutation of order log-convexity).

$\neg c l aim$

Proof. Machine-checked in Lean as D5/S3/Analytic/BesselProductOrderLogConvexity/Result.result (✓ std3). ∎

Resolves. Problems/baricz-ponnusamy-2013-bessel-product-order-log-convexity (refuted) by D5/S3/Analytic/BesselProductOrderLogConvexity/Result.result.

Source. Repository-derived.

Acknowledgement. Á. Baricz and S. Ponnusamy (2013). On Turán type inequalities for modified Bessel functions. URL: https://arxiv.org/abs/1010.3346.

Commentary.

Take u=1, nu=−1/2 and h=1. All three orders are noninteger and greater than −1. The strict product comparison contradicts the asserted three-point inequality. Thus the positive modified Bessel product is not log-convex in its order on the entire interval (−1,∞) for every positive argument. The conclusion concerns the order itself, rather than the square-root parametrization.

References

Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.P
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.a_eq_sqrt
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.besselK
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.claim
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.exp_bound
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.gamma_factorial
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.half_noninteger
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.half_values
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.lower
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.minus_term
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.plus_term
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.product_values
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.recurrence
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.recurrence_minus
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.recurrence_plus
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.result
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.shift
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.step
Truth anchor: D5/S3/Analytic/BesselProductOrderLogConvexity/Result.witness
Dependency: D5/S3/Analytic/BesselRatioLogConcavity/Result

Keyboard shortcuts

trureturing — Discovering truth

The modified Bessel product need not be log-convex in its order

Abstract

References