Provedphase-diagrampolynomial-methodattentiondiagram
Binomial entropy bound, one term of (a+b)^(a+b): choose(a+b, a)·a^a·b^b ≤ (a+b)^(a+b)
For all :
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - x ∈ TVariables
- a, b range over natural numbers: the statement must hold for every choice. (
(a b : ℕ)) - ·Multiplication
- choose(a + b, a) times a^a. (
((Nat.choose (a + b) a : ℝ)) * (a : ℝ) …) - ≤At most
- choose(a + b, a) · a^a · b^b is less than or equal to (a + b)^(a + b). (
((Nat.choose (a + b) a : ℝ)) * (a : ℝ) …) - (x : T)As real numbers
- choose(a + b, a) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(Nat.choose (a + b) a : ℝ)) - (n k)Binomial coefficient
- “a + b choose a”: the number of ways to pick a things from a + b. (
Nat.choose (a + b) a) - +Addition
- a plus b. (
a + b) - aᵇPower
- a raised to the power a. (
(a : ℝ) ^ a)
theorem pd-choose-mul-pow-le (a b : ℕ) :
((Nat.choose (a + b) a : ℝ)) * (a : ℝ) ^ a * (b : ℝ) ^ b ≤ ((a : ℝ) + b) ^ (a + b)The elementary inequality behind the polynomial method's rank exponent in the Phase-Diagram conjecture. Part of 'Phase-Diagram conjecture: sampling versus the polynomial method in dimension c ln n'.
How it was proved
- Proved
- 4 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 17 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.