The scalar Bregman divergence of the power potential $|x|^p/p$ is nonnegative

Proved

HlawkaSchatten.scalarBregman_nonneg

by savarin · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

bregman-divergenceconvexityhlawka-schattenscalar-comparison

Let $p \in \mathbb R$ with $p>1$ , and let $a,b \in \mathbb R$ . Write $F_p(x)=|x|^p/p$ (powerPotential), $G_p(x)=|x|^{p-2}x$ (powerGradient), and

\beta_p(a,b) = F_p(a) - F_p(b) - G_p(b)(a-b)

(scalarBregman) for the Bregman divergence of $F_p$ between $a$ and $b$ . Then

0 \le \beta_p(a,b).

This supplies the scalar nonnegativity used in the spectral Bregman argument. There, the operator quantity is written as a sum of scalar Bregman terms with nonnegative weights, so this result gives nonnegativity of the whole sum.

Preamble

import Definitions.Def_HlawkaSchatten_ScalarBregman
import Mathlib.Analysis.Convex.Deriv
import Mathlib.Analysis.Convex.SpecificFunctions.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.NormPow
import Mathlib.Data.Sign.Basic
import Mathlib.Topology.Instances.Sign

/-
Copyright (c) 2026 Ezzeri Esa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ezzeri Esa
-/

/-!
# Scalar power Bregman data

These are the scalar objects used in the first layer of the audited
Bregman--Mazur proof. The normalization of `powerPotential` is important:
its derivative is the signed `(p - 1)`-power with no extra factor of `p`.
-/


open Filter
open scoped Topology

open HlawkaSchatten

Formal statement

theorem HlawkaSchatten.scalarBregman_nonneg {p : ℝ} (hp : 1 < p) (a b : ℝ) :
    0 ≤ scalarBregman p a b := by sorry

Source

https://github.com/savarin/hlawka-schatten/blob/79aa498bfcf7b22bd91d771fb32ec278e2d4704b/HlawkaSchatten/ScalarBregman.lean#L263-L287

View graph

The scalar Bregman divergence of the power potential ∣x∣p/p|x|^p/p∣x∣p/p is nonnegative

The scalar Bregman divergence of the power potential $|x|^p/p$ is nonnegative