Gaunt’s weighted Bessel tail inequality

Abstract

Squared-order convexity and an exact integral identity give the sharp weighted Bessel tail bound.

Definition 1.1 (alpha).

$\forall n u \in R, \forall n \in R, alpha (n u, n) = n u + n - Real.sqrt ((n u + n)^{2} - 2 \cdot n u - 1)$

Formalization. D5/S3/Analytic/GauntBesselTail/Result.alpha (✓ std3).

Citation. Robert E. Gaunt (2019). Inequalities for some integrals involving modified Bessel functions. DOI: 10.1090/proc/14433. URL: https://arxiv.org/abs/1806.00524.

Commentary.

The smaller parameter shift in Conjecture 2.4.

Definition 1.2 (alphaPrime).

$\forall n u \in R, \forall n \in R, alphaPrime (n u, n) = n u + n + Real.sqrt ((n u + n)^{2} - 2 \cdot n u - 1)$

Formalization. D5/S3/Analytic/GauntBesselTail/Result.alphaPrime (✓ std3).

Citation. Robert E. Gaunt (2019). Inequalities for some integrals involving modified Bessel functions. DOI: 10.1090/proc/14433. URL: https://arxiv.org/abs/1806.00524.

Commentary.

The second shift gives the opposite Bessel order.

Definition 1.3 (tail).

$\forall n u \in R, \forall p \in R, \forall x \in R, tail (n u, p, x) = MeasureTheory.integral (Measure.restrict (volume (), Set.Ioi (x)), t : R \mapsto (t)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (p, t))$

Formalization. D5/S3/Analytic/GauntBesselTail/Result.tail (✓ std3).

Source. Repository-derived.

Acknowledgement. NIST Digital Library of Mathematical Functions (2026). Modified Bessel functions, integral representations. DOI: 10.18434/T4J30S. URL: https://dlmf.nist.gov/10.32.E9.

Commentary.

The real power is used on the positive integration domain. The reused Bessel integral is DLMF 10.32.9.

Definition 1.4 (The complete sharp tail assertion).

$c l aim = ((\forall n \in R, \forall n u \in R, ((n < 1) \land (1 - n + Real.sqrt (2 \cdot (1 - n)) \leq n u)) \Rightarrow (\forall x \in R, (0 < x) \Rightarrow ((x)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (n u + n - alpha (n u, n), x) < tail (n u, n u + n, x)))) \land ((\forall n \in R, \forall n u \in R, ((n < 1) \land (1 - n + Real.sqrt (2 \cdot (1 - n)) \leq n u)) \Rightarrow (\forall b e t a \in R, ((b e t a \neq = alpha (n u, n)) \land (b e t a \neq = alphaPrime (n u, n))) \Rightarrow ((\forall x \in R, (0 < x) \Rightarrow ((x)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (n u + n - b e t a, x) < (x)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (n u + n - alpha (n u, n), x))) \lor (\exists y \in R, (0 < y) \land (tail (n u, n u + n, y) < (y)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (n u + n - b e t a, y)))))) \land (\forall n u \in R, \forall x \in R, (0 < x) \Rightarrow (tail (n u, n u + 1, x) = (x)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (n u, x)))))$

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

Citation. Robert E. Gaunt (2019). Inequalities for some integrals involving modified Bessel functions. DOI: 10.1090/proc/14433. URL: https://arxiv.org/abs/1806.00524.

Commentary.

“Conjecture 2.4. Let n < 1. For ν ≥ 1 − n + √(2(1 − n)), define α_{ν,n} := ν + n − √((ν + n)² − 2ν − 1). Then, for all x > 0, ∫x^∞ K{ν+n}(t)/t^ν dt > K_{ν+n−α_{ν,n}}(x)/x^ν, ν ≥ 1 − n + √(2(1 − n)). (2.17) We have equality in (2.17) when n = 1, and this equality is valid for all ν ∈ ℝ. Let α′{ν,n} := ν + n + √((ν + n)² − 2ν − 1), so that ν + n − α′{ν,n} = −(ν + n − α_{ν,n}) and thus K_{ν+n−α′{ν,n}}(x) = K{ν+n−α_{ν,n}}(x). Then, the index ν + n − α_{ν,n} (and equivalently ν + n − α′{ν,n}) in inequality (2.17) is best possible, in the sense that, for any β ∉ {α{ν,n}, α′{ν,n}}, either K{ν+n−β}(x)/x^ν < K_{ν+n−α_{ν,n}}(x)/x^ν for all x > 0, or there exists a y > 0 such that ∫y^∞ K{ν+n}(t)/t^ν dt < K_{ν+n−β}(y)/y^ν.” arXiv:1806.00524v2, manuscript p. 7, Conjecture 2.4, equation (2.17). Lean uses the displayed definitions and formulas above to encode this statement; the reused K is exactly the positive-argument integral representation in DLMF 10.32.9, and the tail uses t^(−ν) on t>x>0.

Theorem 1.5 (sinh gap pos).

$\forall v \in R, (0 < v) \Rightarrow (0 < v \cdot Real.cosh (v) - Real.sinh (v))$

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

Source. Repository-derived.

Commentary.

The derivative is v sinh(v), strictly positive for v>0. This proves squared-order convexity.

Theorem 1.6 (cosh sqrt deriv).

$\forall u \in R, \forall s \in R, (0 < s) \Rightarrow (HasDerivAt (s : R \mapsto Real.cosh (u \cdot Real.sqrt (s)), \frac{u}{2 \cdot Real.sqrt ( s )} \cdot Real.sinh (u \cdot Real.sqrt (s)), s))$

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

Source. Repository-derived.

Commentary.

The chain rule differentiates the squared-order kernel away from s=0.

Theorem 1.7 (cosh sqrt deriv2).

$\forall u \in R, \forall s \in R, (0 < s) \Rightarrow (HasDerivAt (s : R \mapsto \frac{u}{2 \cdot Real.sqrt ( s )} \cdot Real.sinh (u \cdot Real.sqrt (s)), \frac{u}{4 \cdot ( Real.sqrt ( s ) ) ^{3}} \cdot (u \cdot Real.sqrt (s) \cdot Real.cosh (u \cdot Real.sqrt (s)) - Real.sinh (u \cdot Real.sqrt (s))), s))$

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

Source. Repository-derived.

Commentary.

A second differentiation exposes the positive hyperbolic gap.

Theorem 1.8 (squared order strictConvex).

$\forall u \in R, (0 < u) \Rightarrow (StrictConvexOn (R, Set.Ici (0), s : R \mapsto Real.cosh (u \cdot Real.sqrt (s))))$

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

Source. Repository-derived.

Commentary.

Continuity at zero and positivity of the second derivative prove strict convexity on the closed nonnegative half-line.

Theorem 1.9 (cosh sqrt sq).

$\forall u \in R, \forall a \in R, (0 \leq u) \Rightarrow (Real.cosh (u \cdot Real.sqrt ((a)^{2})) = Real.cosh (a \cdot u))$

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

Source. Repository-derived.

Commentary.

Evenness removes the absolute value of the order.

Theorem 1.10 (positive order kernel).

$\forall u \in R, \forall p \in R, \forall q \in R, \forall n u \in R, (0 < u) \Rightarrow ((0 < q) \Rightarrow ((q < n u) \Rightarrow (((p)^{2} = (q)^{2} + 2 \cdot n u + 1) \Rightarrow (Real.cosh (q \cdot u) \cdot Real.cosh (u) + \frac{n u}{q} \cdot Real.sinh (q \cdot u) \cdot Real.sinh (u) < Real.cosh (p \cdot u)))))$

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

Source. Repository-derived.

Commentary.

Compare adjacent secant slopes at (q−1)², (q+1)² and p². Hyperbolic addition then gives the sharp strict kernel inequality.

Theorem 1.11 (zero order kernel).

$\forall u \in R, \forall p \in R, \forall n u \in R, (0 < u) \Rightarrow ((0 < n u) \Rightarrow (((p)^{2} = 2 \cdot n u + 1) \Rightarrow (Real.cosh (u) + n u \cdot u \cdot Real.sinh (u) < Real.cosh (p \cdot u))))$

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

Source. Repository-derived.

Commentary.

At q=0 use the tangent at s=1 instead of the two distinct secants.

Theorem 1.12 (parameters).

$\forall n u \in R, \forall n \in R, (n < 1) \Rightarrow ((1 - n + Real.sqrt (2 \cdot (1 - n)) \leq n u) \Rightarrow ((0 \leq (n u + n)^{2} - 2 \cdot n u - 1) \land ((Real.sqrt ((n u + n)^{2} - 2 \cdot n u - 1) < n u) \land (Real.sqrt ((n u + n)^{2} - 2 \cdot n u - 1) + 1 < n u + n))))$

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

Source. Repository-derived.

Commentary.

The source parameter range gives a nonnegative discriminant, q<nu and q+1<nu+n.

Theorem 1.13 (exponential kernel integrable).

$\forall z \in R, \forall A \in R, (0 < z) \Rightarrow (MeasureTheory.Integrable (u : R \mapsto Real.exp (- z \cdot Real.cosh (u) + A \cdot u)))$

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

Source. Repository-derived.

Commentary.

A tilted integrable Gaussian dominates the exponential kernel on the whole real line.

Theorem 1.14 (bessel kernel integrable).

$\forall r \in R, \forall z \in R, (0 < z) \Rightarrow (MeasureTheory.IntegrableOn (u : R \mapsto Real.exp (- (z \cdot Real.cosh (u))) \cdot Real.cosh (r \cdot u), Set.Ioi (0)))$

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

Source. Repository-derived.

Commentary.

Expand cosh as a sum of exponentials and apply Gaussian domination for both signs of the order.

Theorem 1.15 (bessel cosh integrable).

$\forall r \in R, \forall z \in R, (0 < z) \Rightarrow (MeasureTheory.IntegrableOn (u : R \mapsto Real.exp (- (z \cdot Real.cosh (u))) \cdot Real.cosh (u) \cdot Real.cosh (r \cdot u), Set.Ioi (0)))$

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

Source. Repository-derived.

Commentary.

The product of the two coshes is the half-sum of the adjacent-order coshes.

Theorem 1.16 (bessel hasDerivAt).

$\forall r \in R, \forall z \in R, (0 < z) \Rightarrow (HasDerivAt (D5.S3.Analytic.GammaGammaNBU.Result.besselK (r), - MeasureTheory.integral (Measure.restrict (volume (), Set.Ioi (0)), u : R \mapsto Real.exp (- (z \cdot Real.cosh (u))) \cdot Real.cosh (u) \cdot Real.cosh (r \cdot u)), z))$

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

Source. Repository-derived.

Commentary.

Local domination with argument z/2 justifies differentiation under the integral.

Theorem 1.17 (integral decay).

$\forall f \in R \to R, (\forall u \in R, (0 < u) \Rightarrow (0 \leq f (u))) \Rightarrow ((\forall z \in R, (0 < z) \Rightarrow (MeasureTheory.IntegrableOn (u : R \mapsto Real.exp (- (z \cdot Real.cosh (u))) \cdot f (u), Set.Ioi (0)))) \Rightarrow (\forall t \in R, (1 \leq t) \Rightarrow (abs (MeasureTheory.integral (Measure.restrict (volume (), Set.Ioi (0)), u : R \mapsto Real.exp (- (t \cdot Real.cosh (u))) \cdot f (u))) \leq Real.exp (\frac{- t}{2}) \cdot MeasureTheory.integral (Measure.restrict (volume (), Set.Ioi (0)), u : R \mapsto Real.exp (- (\frac{1}{2} \cdot Real.cosh (u))) \cdot f (u)))))$

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

Source. Repository-derived.

Commentary.

For t≥1, cosh(u)≥1 splits off a uniform exp(−t/2) factor.

Theorem 1.18 (bessel bigO).

$\forall r \in R, Asymptotics.IsBigO (Filter.atTop (), D5.S3.Analytic.GammaGammaNBU.Result.besselK (r), t : R \mapsto Real.exp (- \frac{t}{2}))$

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

Source. Repository-derived.

Commentary.

The positive Bessel kernel inherits the uniform exponential decay.

Theorem 1.19 (weighted decay).

$\forall F \in R \to R, (ContinuousOn (F, Set.Ioi (0))) \Rightarrow ((Asymptotics.IsBigO (Filter.atTop (), F, t : R \mapsto Real.exp (- \frac{t}{2}))) \Rightarrow (\forall n u \in R, \forall x \in R, (0 < x) \Rightarrow ((MeasureTheory.IntegrableOn (t : R \mapsto (t)^{- n u} \cdot F (t), Set.Ioi (x))) \land (Filter.Tendsto (t : R \mapsto (t)^{- n u} \cdot F (t), Filter.atTop (), nhds (0))))))$

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

Source. Repository-derived.

Commentary.

Any real power times the exponentially decreasing function is integrable on every positive tail and tends to zero.

Theorem 1.20 (tail integrable).

$\forall n u \in R, \forall r \in R, \forall x \in R, (0 < x) \Rightarrow (MeasureTheory.IntegrableOn (t : R \mapsto (t)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (r, t), Set.Ioi (x)))$

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

Source. Repository-derived.

Commentary.

The weighted Bessel kernel satisfies the hypotheses of weighted_decay.

Theorem 1.21 (weighted bessel tendsto).

$\forall n u \in R, \forall r \in R, Filter.Tendsto (t : R \mapsto (t)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (r, t), Filter.atTop (), nhds (0))$

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

Source. Repository-derived.

Commentary.

The weighted Bessel function vanishes at positive infinity.

Theorem 1.22 (abs sinh le cosh).

$\forall u \in R, abs (Real.sinh (u)) \leq Real.cosh (u)$

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

Source. Repository-derived.

Commentary.

Apply sinh(u)<cosh(u) at u and −u. This bounds the integration-by-parts kernel.

Theorem 1.23 (bessel sinh integrable).

$\forall r \in R, \forall z \in R, (0 < z) \Rightarrow (MeasureTheory.IntegrableOn (u : R \mapsto Real.exp (- (z \cdot Real.cosh (u))) \cdot Real.sinh (r \cdot u) \cdot Real.sinh (u), Set.Ioi (0)))$

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

Source. Repository-derived.

Commentary.

The absolute sinh product is bounded by the integrable cosh product.

Theorem 1.24 (exponential kernel tendsto).

$\forall z \in R, \forall A \in R, (0 < z) \Rightarrow (Filter.Tendsto (u : R \mapsto Real.exp (- z \cdot Real.cosh (u) + A \cdot u), Filter.atTop (), nhds (0)))$

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

Source. Repository-derived.

Commentary.

The same quadratic domination also proves pointwise decay at infinity.

Theorem 1.25 (u exponential integrable).

$\forall z \in R, \forall A \in R, (0 < z) \Rightarrow (MeasureTheory.IntegrableOn (u : R \mapsto u \cdot Real.exp (- z \cdot Real.cosh (u) + A \cdot u), Set.Ioi (0)))$

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

Source. Repository-derived.

Commentary.

The elementary bound u≤exp(u) absorbs the extra positive-domain factor.

Theorem 1.26 (u exponential tendsto).

$\forall z \in R, (0 < z) \Rightarrow (Filter.Tendsto (u : R \mapsto u \cdot Real.exp (- (z \cdot Real.cosh (u))), Filter.atTop (), nhds (0)))$

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

Source. Repository-derived.

Commentary.

Absorb u into exp(u) and use the exponential-kernel limit.

Definition 1.27 (S).

$\forall r \in R, \forall u \in R, S (r, u) = ite (r = 0, u, \frac{Real.sinh ( r \cdot u )}{r})$

Formalization. D5/S3/Analytic/GauntBesselTail/Result.S (✓ std3).

Source. Repository-derived.

Commentary.

This continuous-order antiderivative treats r=0 separately.

Theorem 1.28 (S deriv).

$\forall r \in R, \forall u \in R, HasDerivAt (S (r), Real.cosh (r \cdot u), u)$

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

Source. Repository-derived.

Commentary.

For every real r, the derivative in u of S_r is cosh(ru).

Theorem 1.29 (S sinh integrable).

$\forall r \in R, \forall z \in R, (0 < z) \Rightarrow (MeasureTheory.IntegrableOn (u : R \mapsto Real.exp (- (z \cdot Real.cosh (u))) \cdot S (r, u) \cdot Real.sinh (u), Set.Ioi (0)))$

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

Source. Repository-derived.

Commentary.

The nonzero-order case follows from the sinh-product bound; the zero-order case uses the extra-u envelope.

Theorem 1.30 (S kernel tendsto).

$\forall r \in R, \forall z \in R, (0 < z) \Rightarrow (Filter.Tendsto (u : R \mapsto Real.exp (- (z \cdot Real.cosh (u))) \cdot S (r, u), Filter.atTop (), nhds (0)))$

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

Source. Repository-derived.

Commentary.

The boundary term in the hyperbolic integration by parts tends to zero.

Theorem 1.31 (bessel ibp).

$\forall r \in R, \forall z \in R, (0 < z) \Rightarrow (D5.S3.Analytic.GammaGammaNBU.Result.besselK (r, z) = z \cdot MeasureTheory.integral (Measure.restrict (volume (), Set.Ioi (0)), u : R \mapsto Real.exp (- (z \cdot Real.cosh (u))) \cdot S (r, u) \cdot Real.sinh (u)))$

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

Source. Repository-derived.

Commentary.

Differentiate exp(−z cosh u)S_r(u) and apply the fundamental theorem on the upper half-line.

Definition 1.32 (H).

$\forall n u \in R, \forall p \in R, \forall r \in R, \forall u \in R, H (n u, p, r, u) = Real.cosh (p \cdot u) - Real.cosh (r \cdot u) \cdot Real.cosh (u) - n u \cdot S (r, u) \cdot Real.sinh (u)$

Formalization. D5/S3/Analytic/GauntBesselTail/Result.H (✓ std3).

Source. Repository-derived.

Commentary.

The signed kernel measures the difference between the tail and its proposed lower expression.

Definition 1.33 (J).

$\forall n u \in R, \forall p \in R, \forall r \in R, \forall t \in R, J (n u, p, r, t) = MeasureTheory.integral (Measure.restrict (volume (), Set.Ioi (0)), u : R \mapsto Real.exp (- (t \cdot Real.cosh (u))) \cdot H (n u, p, r, u))$

Formalization. D5/S3/Analytic/GauntBesselTail/Result.J (✓ std3).

Source. Repository-derived.

Commentary.

J is the Laplace integral of the signed kernel.

Theorem 1.34 (H integrable).

$\forall n u \in R, \forall p \in R, \forall r \in R, \forall t \in R, (0 < t) \Rightarrow (MeasureTheory.IntegrableOn (u : R \mapsto Real.exp (- (t \cdot Real.cosh (u))) \cdot H (n u, p, r, u), Set.Ioi (0)))$

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

Source. Repository-derived.

Commentary.

Each of the three terms is absolutely integrable.

Theorem 1.35 (J eq).

$\forall n u \in R, \forall p \in R, \forall r \in R, \forall t \in R, (0 < t) \Rightarrow (J (n u, p, r, t) = D5.S3.Analytic.GammaGammaNBU.Result.besselK (p, t) - \frac{D5.S3.Analytic.GammaGammaNBU.Result.besselK ( r + 1 , t ) + D5.S3.Analytic.GammaGammaNBU.Result.besselK ( r - 1 , t )}{2} - \frac{n u}{t} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (r, t))$

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

Source. Repository-derived.

Commentary.

The adjacent-order identity and integration by parts express J using ordinary Bessel functions.

Theorem 1.36 (weighted J integrable).

$\forall n u \in R, \forall p \in R, \forall r \in R, \forall x \in R, (0 < x) \Rightarrow (MeasureTheory.IntegrableOn (t : R \mapsto (t)^{- n u} \cdot J (n u, p, r, t), Set.Ioi (x)))$

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

Source. Repository-derived.

Commentary.

J_eq reduces this integrability to three weighted Bessel tails and one adjacent real power.

Theorem 1.37 (tail identity).

$\forall n u \in R, \forall p \in R, \forall r \in R, \forall x \in R, (0 < x) \Rightarrow (tail (n u, p, x) - (x)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (r, x) = MeasureTheory.integral (Measure.restrict (volume (), Set.Ioi (x)), t : R \mapsto (t)^{- n u} \cdot J (n u, p, r, t)))$

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

Source. Repository-derived.

Commentary.

Differentiate x^(−nu)K_r(x), integrate its derivative on the positive upper half-line, and use its zero limit.

Theorem 1.38 (integral Ioi pos).

$\forall f \in R \to R, \forall a \in R, (MeasureTheory.IntegrableOn (f, Set.Ioi (a))) \Rightarrow ((\forall u \in R, (a < u) \Rightarrow (0 < f (u))) \Rightarrow (0 < MeasureTheory.integral (Measure.restrict (volume (), Set.Ioi (a)), u : R \mapsto f (u))))$

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

Source. Repository-derived.

Commentary.

A positive integrand on an upper half-line has support of positive Lebesgue measure.

Theorem 1.39 (strict tail).

$\forall n u \in R, \forall p \in R, \forall q \in R, \forall x \in R, (0 \leq q) \Rightarrow ((q < n u) \Rightarrow (((p)^{2} = (q)^{2} + 2 \cdot n u + 1) \Rightarrow ((0 < x) \Rightarrow ((x)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (q, x) < tail (n u, p, x)))))$

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

Source. Repository-derived.

Commentary.

The strict scalar kernel comparison makes J positive, and tail_identity then gives the strict bound.

Theorem 1.40 (n one identity).

$\forall n u \in R, \forall x \in R, (0 < x) \Rightarrow (tail (n u, n u + 1, x) = (x)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (n u, x))$

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

Source. Repository-derived.

Commentary.

The addition formula makes H identically zero when p=nu+1 and r=nu, including nu=0 and negative nu.

Theorem 1.41 (laplace negative).

$\forall f \in R \to R, (\forall t \in R, (0 < t) \Rightarrow (MeasureTheory.IntegrableOn (u : R \mapsto Real.exp (- (t \cdot Real.cosh (u))) \cdot f (u), Set.Ioi (0)))) \Rightarrow (\forall d e lt a \in R, (0 < d e lt a) \Rightarrow ((\forall u \in R, (0 < u) \Rightarrow ((u < d e lt a) \Rightarrow (f (u) < 0))) \Rightarrow (Filter.Eventually (t : R \mapsto MeasureTheory.integral (Measure.restrict (volume (), Set.Ioi (0)), u : R \mapsto Real.exp (- (t \cdot Real.cosh (u))) \cdot f (u)) < 0, Filter.atTop ()))))$

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

Source. Repository-derived.

Commentary.

A negative interval next to the origin contributes at a slower exponential decay rate than the outer positive part. A fixed inner subinterval therefore forces a negative Laplace integral for every sufficiently large t.

Theorem 1.42 (H negative near).

$\forall n u \in R, \forall p \in R, \forall q \in R, \forall r \in R, (0 \leq q) \Rightarrow ((q < r) \Rightarrow (((p)^{2} = (q)^{2} + 2 \cdot n u + 1) \Rightarrow (\exists d e lt a \in R, (0 < d e lt a) \land (\forall u \in R, (0 < u) \Rightarrow ((u < d e lt a) \Rightarrow (H (n u, p, r, u) < 0))))))$

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

Source. Repository-derived.

Commentary.

At zero both H and its first derivative vanish, while its second derivative is q²−r²<0. The derivative test gives a negative right-hand interval.

Theorem 1.43 (larger order failure).

$\forall n u \in R, \forall p \in R, \forall q \in R, \forall r \in R, (0 \leq q) \Rightarrow ((q < r) \Rightarrow (((p)^{2} = (q)^{2} + 2 \cdot n u + 1) \Rightarrow (Filter.Eventually (x : R \mapsto tail (n u, p, x) < (x)^{- n u} \cdot D5.S3.Analytic.GammaGammaNBU.Result.besselK (r, x), Filter.atTop ()))))$

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

Source. Repository-derived.

Commentary.

The local kernel sign and laplace_negative make J negative for all sufficiently large t. The tail identity proves failure at every sufficiently large x, stronger than a single positive witness.

Theorem 1.44 (bessel order lt).

$\forall a \in R, \forall b \in R, \forall x \in R, (abs (a) < abs (b)) \Rightarrow ((0 < x) \Rightarrow (D5.S3.Analytic.GammaGammaNBU.Result.besselK (a, x) < D5.S3.Analytic.GammaGammaNBU.Result.besselK (b, x)))$

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

Source. Repository-derived.

Commentary.

Strict increase of cosh in the absolute order and positive integration prove strict order monotonicity.

Theorem 1.45 (The sharp bound and its optimality).

$c l aim$

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

Resolves. Problems/gaunt-2019-bessel-tail-conjecture (proved) by D5/S3/Analytic/GauntBesselTail/Result.result.

Source. Repository-derived.

Acknowledgement. Robert E. Gaunt (2019). Inequalities for some integrals involving modified Bessel functions. DOI: 10.1090/proc/14433. URL: https://arxiv.org/abs/1806.00524.

Commentary.

The strict bound follows from squared-order convexity and the exact tail identity. A smaller absolute order gives a strictly smaller right side at every positive x; a larger absolute order fails for all sufficiently large x. The two excluded shifts give opposite orders and therefore identical Bessel values. When n=1, the hyperbolic addition formula makes the signed kernel identically zero for every real nu.

References

Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.H
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.H_integrable
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.H_negative_near
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.J
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.J_eq
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.S
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.S_deriv
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.S_kernel_tendsto
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.S_sinh_integrable
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.abs_sinh_le_cosh
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.alpha
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.alphaPrime
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.bessel_bigO
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.bessel_cosh_integrable
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.bessel_hasDerivAt
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.bessel_ibp
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.bessel_kernel_integrable
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.bessel_order_lt
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.bessel_sinh_integrable
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.claim
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.cosh_sqrt_deriv
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.cosh_sqrt_deriv2
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.cosh_sqrt_sq
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.exponential_kernel_integrable
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.exponential_kernel_tendsto
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.integral_Ioi_pos
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.integral_decay
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.laplace_negative
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.larger_order_failure
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.n_one_identity
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.parameters
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.positive_order_kernel
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.result
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.sinh_gap_pos
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.squared_order_strictConvex
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.strict_tail
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.tail
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.tail_identity
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.tail_integrable
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.u_exponential_integrable
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.u_exponential_tendsto
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.weighted_J_integrable
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.weighted_bessel_tendsto
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.weighted_decay
Truth anchor: D5/S3/Analytic/GauntBesselTail/Result.zero_order_kernel
Dependency: D5/S3/Analytic/GammaGammaNBU/Result
Dependency: D5/S3/TotalVariation/Asymptotics/GaussianCoshKernel

Keyboard shortcuts

trureturing — Discovering truth

Gaunt’s weighted Bessel tail inequality

Abstract

References