Newman’s Kantorovich inequality

Paper

Kantorovich’s Inequality, 1960. Journal of Research of the National Bureau of Standards B 64B(1), pp. 33–34. Read the original two-page paper.

The result

Positive values between m and M, averaged with nonnegative weights summing to one, satisfy the Kantorovich product bound. Equal weights on the two endpoints attain its constant.

(Σᵢ wᵢxᵢ)(Σᵢ wᵢ/xᵢ) ≤ (m + M)²/(4mM)

Scope & assumptions

5 checked theorems. The scalar interval bound, its weighted sum, the product estimate, the finite weighted inequality, and endpoint equality. The historical anchor is Newman (1960), not a claim to reproduce Kantorovich’s full earlier operator argument.

Real values, 0 < m, 0 < M, m ≤ xᵢ ≤ M, wᵢ ≥ 0 and Σwᵢ = 1. Zero weights are allowed. Finite sums only.

Prior work

No matching named formalization was located in the bounded search of two Mathlib revisions and indexed web results on 2026-09-10. Related library ingredients already exist. First-formalization status is unconfirmed; this does not establish priority.

Lean proof

Lean + Mathlib 4.33.1 · 5 checked theorems

import Mathlib.Algebra.Order.BigOperators.Ring.Finset
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity

/-! Newman (1960), Kantorovich's inequality: the finite weighted scalar case.
No diagonalization or operator functional calculus is hidden in the proof.
The endpoint equality example shows the universal constant is sharp. -/
namespace PaperToLean.Kantorovich
noncomputable section
open scoped BigOperators
variable {ι : Type*}

theorem scalar_bound (m M x : ℝ) (hm : 0 < m) (hlo : m ≤ x) (hhi : x ≤ M) :
    x + m * M / x ≤ m + M := by
  have hx : 0 < x := lt_of_lt_of_le hm hlo
  apply (le_of_sub_nonneg ?_)
  have hp := mul_nonneg (sub_nonneg.mpr hlo) (sub_nonneg.mpr hhi)
  have hi : m + M - (x + m * M / x) = (x - m) * (M - x) / x := by
    field_simp
    ring
  rw [hi]
  exact div_nonneg hp (le_of_lt hx)

theorem weighted_bound (I : Finset ι) (w x : ι → ℝ) (m M : ℝ)
    (hm : 0 < m) (hw : ∀ i ∈ I, 0 ≤ w i) (hs : ∑ i ∈ I, w i = 1)
    (hlo : ∀ i ∈ I, m ≤ x i) (hhi : ∀ i ∈ I, x i ≤ M) :
    (∑ i ∈ I, w i * x i) + m * M * (∑ i ∈ I, w i / x i) ≤ m + M := by
  have h := Finset.sum_le_sum (fun i hi =>
    mul_le_mul_of_nonneg_left (scalar_bound m M (x i) hm (hlo i hi) (hhi i hi)) (hw i hi))
  have heq : (∑ i ∈ I, w i * (x i + m * M / x i)) =
      (∑ i ∈ I, w i * x i) + m * M * (∑ i ∈ I, w i / x i) := by
    simp only [Finset.mul_sum, ← Finset.sum_add_distrib]
    apply Finset.sum_congr rfl
    intro i _
    ring
  rw [heq, ← Finset.sum_mul, hs, one_mul] at h
  exact h

theorem product_from_linear_bound (A C m M : ℝ) (hm : 0 < m) (hM : 0 < M)
    (hA : 0 ≤ A) (hC : 0 ≤ C) (h : A + m * M * C ≤ m + M) :
    A * C ≤ (m + M) ^ 2 / (4 * m * M) := by
  apply (le_div_iff₀ (by positivity : 0 < 4 * m * M)).mpr
  have hsum : 0 ≤ A + m * M * C := by positivity
  have hsq : (A + m * M * C) ^ 2 ≤ (m + M) ^ 2 := by nlinarith
  nlinarith [sq_nonneg (A - m * M * C)]

theorem inequality (I : Finset ι) (w x : ι → ℝ) (m M : ℝ)
    (hm : 0 < m) (hM : 0 < M) (hw : ∀ i ∈ I, 0 ≤ w i)
    (hs : ∑ i ∈ I, w i = 1) (hlo : ∀ i ∈ I, m ≤ x i) (hhi : ∀ i ∈ I, x i ≤ M) :
    (∑ i ∈ I, w i * x i) * (∑ i ∈ I, w i / x i) ≤ (m + M) ^ 2 / (4 * m * M) := by
  apply product_from_linear_bound _ _ m M hm hM
  · exact Finset.sum_nonneg (fun i hi => mul_nonneg (hw i hi) (le_trans (le_of_lt hm) (hlo i hi)))
  · exact Finset.sum_nonneg (fun i hi => div_nonneg (hw i hi) (le_trans (le_of_lt hm) (hlo i hi)))
  · exact weighted_bound I w x m M hm hw hs hlo hhi

theorem endpoint_sharp (m M : ℝ) (hm : m ≠ 0) (hM : M ≠ 0) :
    ((m + M) / 2) * ((1 / m + 1 / M) / 2) = (m + M) ^ 2 / (4 * m * M) := by
  field_simp
  ring

#print axioms scalar_bound
#print axioms weighted_bound
#print axioms product_from_linear_bound
#print axioms inequality
#print axioms endpoint_sharp
end
end PaperToLean.Kantorovich

Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Kantorovich.lean
SHA-256: a5c479a4a9e32d1d7175879d068b10ab37301c520cd34ba080676e81e600aefb
Result: passed

'PaperToLean.Kantorovich.scalar_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kantorovich.weighted_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kantorovich.product_from_linear_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kantorovich.inequality' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kantorovich.endpoint_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]

Run it

Install Lean with elan and Git. Download the project ZIP, extract it, and run these commands in that folder. The first command downloads the pinned Mathlib dependencies.

python3 prepare.py
lake env lean -DwarningAsError=true Kantorovich.lean

A successful check prints the axiom dependencies and exits without errors.