4th-power quartic Jensen convexity gap strict positivity theorem on continuous annuli

import Mathlib

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

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