Weighted root integral identity

Proved

WeightedRootIntegralIdentity.weighted_root_integral_identity

by abcdefg · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisgeometric-meanintegral-identity

Let $0<a_0\leq a_1\leq \cdots\leq a_{n-1}$ be a monotone sequence of $n\ge2$ positive real numbers. Then

\sum_{k=0}^{n-2}\frac{1}{\pi}\sin\!\left(\frac{\pi(k+1)}{n}\right) \int_{a_k}^{a_{k+1}} \frac{\prod_{i=0}^{n-1}|x-a_i|^{1/n}}{x}\,dx = \frac1n\sum_{i=0}^{n-1}a_i- \left(\prod_{i=0}^{n-1}a_i\right)^{1/n}.

This identity equates a sine-weighted sum of interval integrals with the difference between the arithmetic and geometric means of the ordered positive nodes.

Preamble

import Mathlib open scoped BigOperators Interval

Formal statement

namespace WeightedRootIntegralIdentity

theorem weighted_root_integral_identity
    (n : ℕ) (hn : 2 ≤ n) (a : ℕ → ℝ)
    (hpos : ∀ i < n, 0 < a i)
    (hmono : ∀ i < n - 1, a i ≤ a (i + 1)) :
    (∑ k ∈ Finset.range (n - 1),
      (Real.sin (Real.pi * ((k + 1 : ℝ) / n)) / Real.pi) *
        ∫ x in a k..a (k + 1),
          (∏ i ∈ Finset.range n, Real.rpow |x - a i| ((n : ℝ)⁻¹)) / x)
      = ((1 : ℝ) / n) * (∑ i ∈ Finset.range n, a i)
          - Real.rpow (∏ i ∈ Finset.range n, a i) ((n : ℝ)⁻¹) := by sorry

end WeightedRootIntegralIdentity

Source

User-provided image (13 September 2026). Original publication, page, and theorem/equation number not supplied.

Read-back

What the Lean code literally says, in plain math · gpt-5

Let $n\in\mathbb N$ satisfy $2\le n$ , and let $a:\mathbb N\to\mathbb R$ . Assume:

\forall i\in\mathbb N,\quad i<n\ \Longrightarrow\ 0<a(i),

and

\forall i\in\mathbb N,\quad i<n-1\ \Longrightarrow\ a(i)\le a(i+1),

where $n-1$ is subtraction in $\mathbb N$ (hence truncated at $0$ ).

Then the following equality of real numbers holds:

\begin{aligned} \sum_{k\in\{0,\ldots,(n-1)-1\}} \left( \frac{\sin\!\left(\pi\,\frac{k+1}{n}\right)}{\pi} \right) \left( \int_{a(k)}^{a(k+1)} \frac{ \displaystyle\prod_{i\in\{0,\ldots,n-1\}} |x-a(i)|^{\,(\,n:\mathbb R\,)^{-1}} }{x}\,dx \right) &= \frac1n\sum_{i\in\{0,\ldots,n-1\}}a(i) - \left( \prod_{i\in\{0,\ldots,n-1\}}a(i) \right)^{(\,n:\mathbb R\,)^{-1}} . \end{aligned}

Here each displayed finite set is Finset.range of its bound: $\operatorname{range}(m)=\{j\in\mathbb N\mid j<m\}$ . Thus the outer sum is over $k<n-1$ , while the product and the right-hand sum are over $i<n$ . The exponents use Real.rpow: $|x-a(i)|^{(n:\mathbb R)^{-1}}$ and $\bigl(\prod_{i<n}a(i)\bigr)^{(n:\mathbb R)^{-1}}$ .

All occurrences of $n$ in real arithmetic are coerced from $\mathbb N$ to $\mathbb R$ ; $(n:\mathbb R)^{-1}$ is the totalized real inverse, and the divisions by $n$ are real divisions. The hypothesis $2\le n$ entails that $n\ne0$ and that $n-1\ge1$ , so the outer range is nonempty. Without that hypothesis, ange 0 would be empty, finite products over an empty range would equal $1$ , finite sums over an empty range would equal $0$ , and natural subtraction such as $n-1$ would truncate at $0$ .

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by abcdefg · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph