Cauchy–Schwarz for real powers
In 2025 four mathematicians conjectured that a strengthened Cauchy–Schwarz inequality holds for every real power from 2 upwards. This page explains why it is true, with pictures you can play with. The full proof is in the paper, and every step of it is checked by the Lean proof assistant.
Pragyaan Gaur
A 7 minute narrated video covers the same ground. The paper has the full proofs.
1. The gap in Cauchy–Schwarz
The Cauchy–Schwarz inequality is one of the most used facts in mathematics. For two vectors $v$ and $w$ it says
where $\langle v,w\rangle=v_1w_1+\dots+v_nw_n$ is the inner product and $\|v\|=\sqrt{\langle v,v\rangle}$ is the length. In the plane this is the statement that $\cos\theta\le1$ for the angle $\theta$ between the vectors. The difference between the two sides is a gap, $\|v\|\,\|w\|-\langle v,w\rangle$. It is zero exactly when the vectors point the same way, and it grows as they turn apart. Drag the tips of the arrows below.
2. Raising the entries to a power
Now take vectors with nonnegative entries and raise every entry to a power $p$. Write $v^p=(v_1^p,\dots,v_n^p)$. Large entries grow faster than small ones, so the powered vectors turn towards the coordinate axes and away from each other, and their gap grows. Nathaniel Johnston found in 2018 that for $p=2$ the gap of the squared vectors never exceeds the square of something natural:
The right side is the squared area of the parallelogram spanned by $v$ and $w$. Johnston, Plosker, Torrance and Varona asked which other powers work. The question is whether
holds for all nonnegative vectors. Try it. The sliders set three entries of each vector and the exponent. The curve shows, for every $p$ at once, whether the inequality holds for your vectors. It is above the axis where the inequality holds and below it where it fails.
With $v=(2,1)$ and $w=(1,2)$ the two sides are equal at $p=1$ and at $p=2$, the inequality fails for every $p$ strictly between them, and it holds for every $p$ above 2. At $p=1.5$ the left side is $3.343$ and the right side is $3.180$.
3. A short history
4. Why whole numbers were easier
For $p=2$, write all the products $v_iv_j$ in a grid. This grid is the tensor square $v\otimes v$. Its diagonal is exactly $v^2$.
The full grids satisfy $\langle v\otimes v,w\otimes w\rangle=\langle v,w\rangle^2$ and $\|v\otimes v\|=\|v\|^2$, so the right side of the inequality is the gap of the full grids. Johnston, Plosker, Torrance and Varona showed that throwing away coordinates never increases this kind of gap. Keeping only the diagonal gives the left side, so the inequality follows. With $p$ factors the same argument works for every whole number $p$.
For $p=2.5$ there is no grid with two and a half factors. This is the reason the real case stayed open, and it needs a different idea.
5. The new idea: one small matrix per coordinate
For each coordinate $i$ put three numbers into a symmetric $2\times2$ matrix,
Adding these matrices gives the matrix of lengths and inner products of $v$ and $w$, called their Gram matrix. Now raise every entry to the power $p$, which is written $A^{\circ p}$. There are two ways to combine this with the sum.
Powering first and then adding gives the matrix behind the left side. Adding first and then powering gives the matrix behind the right side. The key fact is that for $p\ge2$ the second matrix is always the bigger one:
Here $M\succeq N$ means that $M-N$ is positive semidefinite. For a $2\times2$ symmetric matrix this is a simple condition: the diagonal entries $a,b$ are nonnegative and the corner entry $c$ satisfies $c^2\le ab$. This fact is a special case of a 2015 theorem of Guillot, Khare and Rajaratnam, who found exactly which powers behave this way for matrices of every size. For $2\times2$ matrices the answer is $p=1$ and every $p\ge2$. So the number 2 in the conjecture is the same number 2 that appears in their theorem. The paper gives a short self-contained proof using the formula
and the Cauchy–Schwarz inequality for integrals, which works because $p-2\ge0$.
6. The picture: a disk that the difference must stay in
A symmetric matrix $\left(\begin{smallmatrix}a&c\\c&b\end{smallmatrix}\right)$ with $a+b>0$ is positive semidefinite exactly when the point
lies in the unit disk, because $(a-b)^2+4c^2\le(a+b)^2$ is the same as $c^2\le ab$. The disk is a slice of the cone of positive semidefinite matrices. The plot below shows this point for the difference between the two matrices of Section 5, using the vectors you chose above. For $v=(2,1)$ and $w=(1,2)$, move the exponent and watch the point leave the disk between 1 and 2 and return to it at 2. The preset $v=(3,1,0)$, $w=(1,4,0)$ in Section 2 gives a path that is not straight.
From the matrices back to numbers
One last ingredient turns a matrix into a number. Define
Applied to the two matrices of Section 5 it gives exactly the two sides of the inequality. It can be written as the smallest value of $\tfrac12(sa+b/s)-c$ over $s>0$, and each of these expressions increases when the matrix increases in the sense of $\succeq$. So $\Phi$ of the bigger matrix is bigger, and the inequality is proved.
7. Beyond the conjecture
When are the two sides equal?
For $p>2$ the two sides are equal only in the obvious cases: when $v$ and $w$ are parallel, or when each of them has only one nonzero entry. For $p=2$ there is one more family, in which both vectors live on the same two coordinates and $v_iw_i=v_jw_j$. For example $v=(1,2)$ and $w=(4,2)$ give equality at $p=2$ and a strict inequality for every $p>2$. Try it with the "equality at p = 2" button in Section 2.
Weights
Put a positive weight $\omega_i$ on each coordinate, so that $\langle x,y\rangle_\omega=\sum_i\omega_ix_iy_i$. The weighted inequality holds for all nonnegative vectors and every $p\ge2$ exactly when $\omega_i\omega_j\ge1$ for every pair of different coordinates. At most one weight can be below 1, and only if the others make up for it.
More than two vectors
The matrix argument works for $k$ vectors with $k\times k$ Gram matrices, for $p$ a whole number or $p\ge k$, and this range cannot be enlarged.
8. What it is good for: cooling and sharpening
Raise every probability of a distribution $P$ to the power $p$ and divide by the total. The result $P^{(p)}$ is called the escort or tempered distribution. If $P$ is the Boltzmann distribution of a physical system, $P^{(p)}$ is the same system at a temperature $p$ times lower. In machine learning the same map is called sharpening. MixMatch uses $p=2$, and Unsupervised Data Augmentation uses temperature $0.4$, which is $p=2.5$.
Apply the theorem to $v=\sqrt P$ and $w=\sqrt Q$. The inner product $\langle v,w\rangle$ is the Bhattacharyya coefficient $\mathrm{BC}(P,Q)=\sum_i\sqrt{P_iQ_i}$, which measures how much the two distributions overlap. The theorem becomes
a limit on how fast cooling or sharpening can pull two distributions apart. It holds for every $p\ge2$ and fails for some pairs when $1<p<2$.
The applications report goes through this and other consequences in detail, including partition functions, densities of states, kernel methods and the quantum origin of the problem, and marks clearly which statements are proved and which are proposals.
9. Checked by a computer
Every step of the main theorem, the equality cases and the weighted characterisation is checked by Lean 4 with the Mathlib library. This is the conjecture as it is stated in Lean, followed by its proof.
def Conjecture_5_1 : Prop :=
∀ n : ℕ, 1 ≤ n → ∀ p : ℝ, 2 ≤ p → ∀ v w : EuclideanSpace ℝ (Fin n),
(∀ i, 0 < v i) → (∀ i, 0 < w i) →
‖epow p v‖ * ‖epow p w‖ - inner ℝ (epow p v) (epow p w)
≤ ‖v‖ ^ p * ‖w‖ ^ p - (inner ℝ v w) ^ p
theorem conjecture_5_1_true : Conjecture_5_1
The repository's check script builds the project, fails if any proof is missing, and prints the axioms that the main theorems use. They are only the three standard axioms of Lean's logic.