Series and inequalities — avoiding real analysis and reducing to a comparison of coefficients

Consider the following three series. The denominators of the coefficients are products of factorials, and the second and the third are the first differentiated once and twice.

For x ≥ 0, is F₁(x)² − F₀(x)·F₂(x) ≥ 0?
(This says the same thing as: log F₀ is concave — (log F₀)'' ≤ 0.)

F₀ is the modified Bessel function I₁ under a change of variable, and this inequality is of the form called Turán type (I₂² ≥ I₁I₃). knownThe inequality itself is known (Baricz–Ponnusamy, arXiv:1010.3346; title and abstract confirmed. Whether the proof by comparing coefficients first appeared there is unconfirmed). What is explained here is how to put it into Lean; there is no new mathematical claim.

It is a component that appears in lattice field theory, on the way from the one-link integral to the strong-coupling constants. There is no claim here about the continuum limit or the mass gap, the actual Millennium Problem.

Write the coefficients as a_k = 1/(k!(k+1)!), b_k = 1/(k!(k+2)!), d_k = 1/(k!(k+3)!). F₁² − F₀F₂ is the difference of two products of series, so the coefficient of xⁿ can be written by the Cauchy product.

Clearing the factorials, this sum becomes a sum of binomial coefficients.

The right side folds up by Vandermonde's identity with a shift (Σ_k C(n,k) C(m,k+r) = C(n+m, n+r)).

Cat is the Catalan number. Every coefficient is positive, so for x ≥ 0 the sum is nonnegative too. On paper it is 4 lines.

The value of this road is that it uses not a single property of Bessel functions. It relies neither on the infinite-product representation (the factorization by zeros) nor on the zeros being real. All it uses is an identity of binomial coefficients and the formula for the coefficients of a product of series.

The fork in the design comes first. Import Bessel functions into Lean, or define the series by hand?

mathlib has no definition of the modified Bessel functions. The closest thing is the regularized hypergeometric function, but it is built as a complex function, so using it for a real inequality needs a conversion. Defining the series by hand with tsum (infinite sum), on the other hand, is a dozen or so lines.

We chose to define the series by hand. The reason is that the paper proof uses no property of Bessel functions. Bringing into the types something the proof does not use adds the work of proving that the imported thing is consistent. Here the identification F₀(κ²/4) = 2I₁(κ)/κ is left outside Lean, and inside Lean everything is closed within talk of series.

In exchange, three jobs are needed inside Lean.

• Summability — tsum is defined to return 0 when the sum does not converge, so unless convergence is proved separately the expression has no meaning. It comes from comparison with 1/k!.
• Termwise differentiation — that differentiating F₀ gives F₁ is obtained by applying, on a ball, the theorem that one may differentiate term by term (hasDerivAt_tsum_of_isPreconnected). The dominating series is k Rᵏ⁻¹/k!.
• Cauchy product — the theorem that turns a product of series into a convolution of coefficients (tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm) is used twice. Summability of the norms is a hypothesis, so the summability job has to be finished first.

All three are "steps not written on paper". Of the 4 lines on paper, this is the only place that grows; the binomial-coefficient side takes the same length as on paper.

State the binomial-coefficient step over ℤ

The paper formula contains a subtraction, C(2n+4, n+2) − C(2n+4, n+1). Binomial coefficients are natural numbers, so written naively this becomes natural-number subtraction. Natural-number subtraction stops at 0 (the same trap as in 04), so the side where the subtraction appears is stated over ℤ.

/-- Vandermonde with shift `r` (kept in the natural numbers). -/
theorem vdm (n m r : ℕ) :
    ∑ k ∈ range (n + 1), n.choose k * m.choose (k + r) = (n + m).choose (n + r)

/-- The numerator of the coefficient (stated over `ℤ`, because a subtraction appears). -/
theorem B1 (n : ℕ) :
    ∑ j ∈ range (n + 1),
        (n.choose j : ℤ) * (((n + 4).choose (j + 2) : ℤ) - ((n + 4).choose (j + 1) : ℤ))
      = ((2 * n + 4).choose (n + 2) : ℤ) - ((2 * n + 4).choose (n + 1) : ℤ)

/-- Its value is a Catalan number. -/
theorem B1_catalan (n : ℕ) :
    ((2 * n + 4).choose (n + 2) : ℤ) - ((2 * n + 4).choose (n + 1) : ℤ) = (catalan (n + 2) : ℤ)

The Vandermonde side can stay in the natural numbers; only B1, where the subtraction appears, is over ℤ. Putting everything over ℤ would insert a coercion at every induction and every use of Pascal's recurrence. Move types only where the subtraction needs it.

State the coefficient identity over a field of characteristic 0

The coefficients a_k and the rest contain division, so they must be stated inside a field. ℝ would do, but we left it as a field K of characteristic 0. That way the same lemma works over ℚ and over ℝ. Positivity of the coefficients is checked over the rationals, and the series inequality is stated over the reals — that division of labor becomes possible.

Go through formal power series

The computation of the coefficients was finished over formal power series (PowerSeries), where convergence is not an issue. "The coefficient is such-and-such" is an algebraic fact with nothing to do with convergence. Closing that first leaves the real-analysis side with only "the sum of a series whose coefficients are known".

/-- The coefficients of `F`. -/
noncomputable def a (k : ℕ) : K := 1 / ((k.factorial : K) * ((k + 1).factorial : K))
/-- The coefficients of `F'`. -/
noncomputable def b (k : ℕ) : K := 1 / ((k.factorial : K) * ((k + 2).factorial : K))
/-- The coefficients of `F''`. -/
noncomputable def d (k : ℕ) : K := 1 / ((k.factorial : K) * ((k + 3).factorial : K))

/-- The formal power series `F = ∑ x^k/(k!(k+1)!)`. -/
noncomputable def Fps : K⟦X⟧ := PowerSeries.mk (a K)

/-- The coefficient of `x^n` in `(F')² − F·F''` is `Cat(n+2)/(n!(n+4)!)`. -/
theorem coeff_turan (n : ℕ) :
    coeff n ((d⁄dX K (Fps K)) ^ 2 - Fps K * d⁄dX K (d⁄dX K (Fps K)))
      = (catalan (n + 2) : K) / ((n.factorial : K) * ((n + 4).factorial : K))

d⁄dX is mathlib's notation for the derivative of a formal power series, and K⟦X⟧ is the type of formal power series with coefficients in K. The coefficient equation closes without convergence ever being mentioned.

The definitions of the series, and how they are related by differentiation.

/-- `F`. -/
noncomputable def F0 (x : ℝ) : ℝ := ∑' k, a ℝ k * x ^ k
/-- `F'`. -/
noncomputable def F1 (x : ℝ) : ℝ := ∑' k, b ℝ k * x ^ k
/-- `F''`. -/
noncomputable def F2 (x : ℝ) : ℝ := ∑' k, d ℝ k * x ^ k

/-- When the coefficient sequence satisfies `|c k| ≤ 1/k!`, differentiating term by term is allowed. -/
theorem hasDerivAt_series (hc : ∀ k, |c k| ≤ 1 / (k.factorial : ℝ)) (x : ℝ) :
    HasDerivAt (fun y => ∑' k, c k * y ^ k) (∑' k : ℕ, ((k : ℝ) + 1) * c (k + 1) * x ^ k) x

theorem hasDerivAt_F0 (x : ℝ) : HasDerivAt F0 (F1 x) x
theorem hasDerivAt_F1 (x : ℝ) : HasDerivAt F1 (F2 x) x

The two main statements. Produce the equality first, and derive the inequality from it.

/-- **Turán-type equality**: holds for every real `x`. -/
theorem turan_series (x : ℝ) :
    F1 x ^ 2 - F0 x * F2 x
      = ∑' n : ℕ, (catalan (n + 2) : ℝ) / ((n.factorial : ℝ) * ((n + 4).factorial : ℝ)) * x ^ n

/-- **Turán-type inequality**: nonnegative for `x ≥ 0`. -/
theorem turan_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ F1 x ^ 2 - F0 x * F2 x

/-- Another inequality: `2 F1 ≤ F0` for `x ≥ 0`. -/
theorem two_F1_le_F0 {x : ℝ} (hx : 0 ≤ x) : 2 * F1 x ≤ F0 x

LeanOneLinkSeries.vdm · B1 · B1_catalan · cauchy_coeff_catalan · hasDerivAt_F0 · hasDerivAt_F1 · turan_series · turan_nonneg · two_F1_le_F0.

That turan_series is an equality, with no condition on x, is the payoff of the design. Nonnegativity reduces to one line: "sum a series with nonnegative coefficients at x ≥ 0". If one tried to prove the inequality directly, the case split on x would creep into the proof. Produce the equality first, and the condition appears only in the last line.

The Vandermonde side

vdm closes by induction on n. Three points did the work.

• Generalize r before inducting. If r is fixed, the induction hypothesis cannot be used. Keeping r under ∀, both terms produced by Pascal's recurrence have the form of the hypothesis.
• For Pascal, use Nat.choose_succ_succ'. There are two orientations; choose the one that matches the shift of the summation index.
• To drop an end of the sum, Finset.sum_range_succ'. There is Finset.sum_range_succ, which drops the last term, and the primed one, which drops the first; here we drop the first.

mathlib also has Nat.add_choose_eq (Vandermonde in antidiagonal form), but induction came out shorter than the moves of dropping the end terms and transferring by symmetry. Which is shorter — "find an existing lemma and apply it" or "do the induction yourself" — you cannot tell until you try.

Clearing the factorials

The step written on paper in the single phrase "clear the factorials" is the most laborious one in Lean. What must not be done is to apply field_simp directly to an expression with factorials. The denominators are recursive terms like k!, and the expansion does not stop.

So an auxiliary lemma was set up first, with the factorials generalized to "elements of a field": from P · f_i · f_j = N and Q · f_i' · f_j' = M, derive N · M · (1/(f_i f_i')) · (1/(f_j f_j')) = P · Q. Make it forget that they are factorials, then apply field_simp. The concrete factorial equation (Nat.add_choose_mul_factorial_mul_factorial) is fed into this auxiliary lemma three times.

Cauchy product and nonnegativity

theorem turan_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ F1 x ^ 2 - F0 x * F2 x := by
  rw [turan_series]
  exact tsum_nonneg fun n => mul_nonneg (by positivity) (pow_nonneg hx n)

Two lines. rw [turan_series] rewrites to the equality, tsum_nonneg (if every term is nonnegative, so is the sum) is applied, and the nonnegativity of each term is split into the product of "the coefficient is nonnegative" and "xⁿ is nonnegative". x ≥ 0 is used in exactly one place, pow_nonneg hx n. Where the hypothesis does its work is visible in this single word.

On the turan_series side, the Cauchy product theorem is used twice (F₁·F₁ and F₀·F₂), the difference is taken with Summable.tsum_sub, and the coefficient equation (cauchy_coeff_catalan) folds it up. The Cauchy product theorem assumes summability of the norms, so the summability lemmas are needed first.

Of the 4 lines on paper, the binomial-coefficient step can be checked with small numbers. Look at Vandermonde with n = 3, m = 7, r = 2.

import Mathlib

open Finset Nat

/-- Vandermonde with shift `r`, seen at `n = 3`, `m = 7`, `r = 2`. -/
example : ∑ k ∈ range 4, Nat.choose 3 k * Nat.choose 7 (k + 2) = Nat.choose 10 5 := by decide

/-- The numerator of the coefficient is a Catalan number (`n = 0` and `n = 1`). -/
example : (Nat.choose 4 2 : ℤ) - Nat.choose 4 1 = catalan 2 := by
  rw [catalan_two]; decide
example : (Nat.choose 6 3 : ℤ) - Nat.choose 6 2 = catalan 3 := by
  rw [catalan_three]; decide

LeanChecked by hand; it went through. 21 + 105 + 105 + 21 = 252 = C(10,5). Passing catalan to decide as it is gets stuck — mathlib's catalan is defined by well-founded recursion, so the kernel does not unfold it. Replace it first with the lemmas that give its value (catalan_two · catalan_three). "It is a finite value, so decide will produce it" does not hold for every way of writing a definition.

The core of the other inequality (2 F₁ ≤ F₀) is also a coefficient identity. It holds for general k, so it can be checked over ℚ.

/-- The difference of the coefficients is "`k/(k+2)` times the same coefficient" (over `ℚ`, for every `k`). -/
example (k : ℕ) : (1 : ℚ) / (k ! * (k + 1)!) - 2 / (k ! * (k + 2)!)
    = (1 / (k ! * (k + 1)!)) * (k / (k + 2)) := by
  have h2 : (((k + 2)! : ℕ) : ℚ) = (k + 2) * ((k + 1)! : ℕ) := by
    rw [Nat.factorial_succ]; push_cast; ring
  have hk : ((k ! : ℕ) : ℚ) ≠ 0 := Nat.cast_ne_zero.2 (Nat.factorial_ne_zero k)
  have hk1 : (((k + 1)! : ℕ) : ℚ) ≠ 0 := Nat.cast_ne_zero.2 (Nat.factorial_ne_zero _)
  have hk2 : ((k : ℚ) + 2) ≠ 0 := by positivity
  rw [h2]
  field_simp
  ring

The right side is nonnegative, so a_k − 2 b_k ≥ 0 holds for every k. Inserting (k+2)! = (k+2)·(k+1)! by hand before applying field_simp is the real instance of "do not apply field_simp with the factorials still in", written above. Apply it only once the denominators are just k! and (k+1)!.

Summability can be checked briefly too.

/-- Summability of the coefficient sequence comes from comparison with `1/k!` (just throw away `(k+1)! ≥ 1`). -/
example (x : ℝ) : Summable (fun k : ℕ => x ^ k / ((k ! : ℝ) * ((k + 1)! : ℝ))) := by
  refine Summable.of_norm_bounded (Real.summable_pow_div_factorial |x|) ?_
  intro k
  have hk : (0:ℝ) < (k ! : ℕ) := by exact_mod_cast k.factorial_pos
  have hk1 : (1:ℝ) ≤ ((k + 1)! : ℕ) := by exact_mod_cast (k + 1).factorial_pos
  rw [Real.norm_eq_abs, abs_div, abs_pow, abs_mul, abs_of_pos hk,
    abs_of_pos (by exact_mod_cast (k + 1).factorial_pos : (0:ℝ) < ((k + 1)! : ℕ))]
  gcongr
  nlinarith [hk, hk1]

LeanChecked by hand; it went through. To Real.summable_pow_div_factorial (Σ |x|ᵏ/k! converges) one only adds the termwise comparison. Choosing 1/k! as the comparison partner, the only thing thrown away is (k+1)! ≥ 1.

lake env lean LatticeGaugeOneLink.lean

3,979 lines, 0 errors, 0 warnings, about 58 seconds. A few lines from the axiom output:

'OneLinkSeries.vdm' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.B1' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.B1_catalan' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.cauchy_coeff_catalan' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.hasDerivAt_F0' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.turan_series' depends on axioms: [propext, Classical.choice, Quot.sound]
'OneLinkSeries.turan_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]

All within the three standard axioms; no sorryAx and no Lean.ofReduceBool. In proofs that deal with real analysis, Classical.choice almost always appears — the construction of the reals themselves, and the definition of tsum (the convention of returning 0 when there is no convergence), go through the axiom of choice. This contrasts with the combinatorial lemmas of 05, where it did not appear.

What turan_nonneg says is this.

For a real number x ≥ 0, F1 x ^ 2 - F0 x * F2 x is at least 0. Here F0, F1 and F2 are the functions defined by tsum inside this Lean file.

Three things it does not say.

• It says nothing about x < 0. The hypothesis 0 ≤ x cannot be dropped. The other inequality (2 F₁ ≤ F₀) actually fails at x = −30 (F₀ − 2F₁ = −0.041…). computationA value checked numerically on this machine.
• It does not say "this is an inequality about Bessel functions". F₀ is a function defined as a series, and the identification F₀(κ²/4) = 2I₁(κ)/κ is not inside Lean. If you doubt this correspondence, the place to doubt is outside Lean. By hand we have confirmed numerical agreement to 15 digits, but that is not a proof. computation
• What the inequality is good for lies outside the statement. Everything from the concavity of log F₀ onward — the estimate of the strong-coupling constants — is a separate chain of theorems, and there a step not yet in Lean (the geometric side of the lattice) remains.

The second is a debt that always appears when a definition is written as a series. Whether the function defined by hand is the same as the function whose name you wanted to invoke lies outside the definition. Continued in It compiles — but does it say what you meant?

Sources and reproduction

Next: 07 Having Lean check a certificate — a way of building that separates search from checking. Terms are in 12 Glossary.