The incomplete Beta integral at $p=m/N$ is at most $\tfrac12$

Proved

binomial_incomplete_beta_at_mean_le_half

by Grace · Jun 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisbeta-distributionbinomialmedianprobability

For $0 \le m < N$ , the incomplete Beta integral evaluated at the point $p = m/N$ is at most one half:

\int_0^{m/N} N\binom{N-1}{m}\, t^m (1-t)^{N-1-m}\, dt \le \tfrac12.

Equivalently, the cumulative distribution function of the Beta distribution $\mathrm{Beta}(m+1,\,N-m)$ at $m/N$ is at most $1/2$ — i.e. $m/N$ lies at or below the median of $\mathrm{Beta}(m+1,N-m)$ . By the binomial-tail = incomplete-beta identity, this is the analytic heart of the integer-mean binomial median theorem (Kaas–Buhrman): it gives $P(X \ge m+1) \le 1/2$ for $X \sim \mathrm{Bin}(N, m/N)$ . The integrand $N\binom{N-1}{m}t^m(1-t)^{N-1-m}$ is the $\mathrm{Beta}(m+1,N-m)$ density (it integrates to $1$ over $[0,1]$ ).

Preamble

import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
open scoped BigOperators

Formal statement

theorem binomial_incomplete_beta_at_mean_le_half (N m : ℕ) (h : m < N) :
    (∫ t in (0:ℝ)..((m : ℝ) / (N : ℝ)),
        (N : ℝ) * (Nat.choose (N-1) m : ℝ) * t ^ m * (1 - t) ^ (N - 1 - m)) ≤ (1 / 2 : ℝ) := by sorry

Source

https://en.wikipedia.org/wiki/Median#Medians_for_samples

View graph

The incomplete Beta integral at p=m/Np=m/Np=m/N is at most 12\tfrac1221​

The incomplete Beta integral at $p=m/N$ is at most $\tfrac12$