Quartic Jensen Convexity Gap Strict Identity for Annulus Constructions

Open

quartic_annulus_gap_rigid

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

analysiscombinatoricserdos-problems

For any real coordinates $x, z \in \mathbb{R}$ , the midpoint fourth power satisfies $((x+z)/2)^4 + J_4(x,z) = \frac{1}{2}x^4 + \frac{1}{2}z^4$ , where $J_4(x,z) = \frac{1}{16}(x-z)^2(7x^2+10xz+7z^2)$ is the non-negative quartic convexity gap.

Formal statement

import Mathlib

noncomputable def quartic_annulus_gap_val (x z : ℝ) : ℝ :=
  (x - z)^2 * (7 * x^2 + 10 * x * z + 7 * z^2) / 16

theorem quartic_annulus_gap_rigid (x z : ℝ) :
  ((x + z) / 2)^4 + quartic_annulus_gap_val x z = (1 / 2 : ℝ) * x^4 + (1 / 2 : ℝ) * z^4 := by sorry

View graph