Quartic Algebraic Jensen Convexity Gap Midpoint Identity

Proved

quartic_algebraic_annulus_gap

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscombinatoricserdos-problems

For any real numbers $x, z \in \mathbb{R}$ , the fourth power midpoint identity satisfies $((x+z)/2)^4 + \frac{1}{16}(x-z)^2(7x^2+10xz+7z^2) = \frac{1}{2}x^4 + \frac{1}{2}z^4$ , guaranteeing non-negative quartic convexity defect on spherical annuli.

Formal statement

import Mathlib

theorem quartic_algebraic_annulus_gap (x z : ℝ) :
  ((x + z) / 2)^4 + (x - z)^2 * (7 * x^2 + 10 * x * z + 7 * z^2) / 16 = (1 / 2 : ℝ) * x^4 + (1 / 2 : ℝ) * z^4 := by sorry

View graph