The scalar Bregman divergence of the power potential $|x|^p/p$ is strictly positive off the diagonal

Proved

HlawkaSchatten.scalarBregman_pos

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$ with $a \neq b$ . 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 < \beta_p(a,b).

This sharpens nonnegativity to strict positivity at every pair of distinct scalar arguments. It does not supply a uniform positive lower bound over all such pairs. Uniform comparison constants relating this divergence to the squared scalar Mazur distance require separate estimates for their ratio, including its limiting regimes.

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_pos {p : ℝ} (hp : 1 < p) {a b : ℝ} (hab : a ≠ b) :
    0 < scalarBregman p a b := by sorry

Source

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

View graph

The scalar Bregman divergence of the power potential ∣x∣p/p|x|^p/p∣x∣p/p is strictly positive off the diagonal

The scalar Bregman divergence of the power potential $|x|^p/p$ is strictly positive off the diagonal