4th-power quartic Jensen convexity gap strict positivity theorem on continuous annuli
Provedquartic_annulus_gap_identity_pos2combinatorics
The quartic Jensen convexity gap strict positivity theorem on continuous annuli.
Formal statement
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_pos2 (x z : ℝ) : ((x + z) / 2)^4 + quartic_gap x z = (1 / 2 : ℝ) * x^4 + (1 / 2 : ℝ) * z^4 := by sorry