theorem strictConvexOn_cube_Ioi : StrictConvexOn ℝ (Set.Ioi 0) fun (x : ℝ) => x ^ 3

The cubic generator x ↦ x³ is strictly convex on the positive real line.

theorem cube_bregman_triangle_counterexample : B[fun (x : ℝ) => x ^ 3] 3 1 > B[fun (x : ℝ) => x ^ 3] 3 2 + B[fun (x : ℝ) => x ^ 3] 2 1

For the cubic generator ω(x) = x³, the Bregman distance fails the triangle inequality at x = 3, y = 2, and z = 1.

theorem exists_strictly_convex_bregman_triangle_counterexample : ∃ (ω : ℝ → ℝ), StrictConvexOn ℝ (Set.Ioi 0) ω ∧ ∃ (x : ℝ) (y : ℝ) (z : ℝ), 0 < x ∧ 0 < y ∧ 0 < z ∧ B[ω] x z > B[ω] x y + B[ω] y z

Text 9.3: the Bregman distance need not satisfy the triangle inequality; a strictly convex generator on the positive reals already gives a counterexample.