Bregman Divergences

Generalized vector-valued Bregman divergences bregDiv f x y J (notation: D_[f](x, y, J) in scoped Bregman) measure the error of the linear approximation of f around y. They satisfy algebraic properties linked to derivatives, including chain rules, product rules, affine invariance, and convexity preservation.

Main definitions

• bregDiv f x y J: The generalized vector-valued Bregman divergence f x - f y - J (x - y) for a function f : E → F and a continuous linear map J : E →L[R] F (e.g. a derivative, gradient, or subgradient).

Notation

• D_[f](x, y, J): Scoped notation in Bregman for bregDiv f x y J.

def bregDiv {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] (f : E → F) (x y : E) (J : E →L[R] F) : F

The generalized vector-valued Bregman divergence. f maps E → F. J is the Jacobian / subgradient continuous linear mapping E →L[R] F.

Equations

• bregDiv f x y J = f x - f y - J (x - y)

def Bregman.«termD_[_](_,_,_)» : Lean.ParserDescr

Scoped notation for bregDiv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem bregDiv_self {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x : E} {J_x : E →L[R] F} : bregDiv f x x J_x = 0

theorem bregDiv_three_point {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x y z : E} {J_x J_y : E →L[R] F} [IsTopologicalAddGroup F] : bregDiv f z x J_x + bregDiv f x y J_y - bregDiv f z y J_y = (J_y - J_x) (z - x)

theorem bregDiv_add_swap {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x y : E} {J_x J_y : E →L[R] F} [IsTopologicalAddGroup F] : bregDiv f y x J_x + bregDiv f x y J_y = (J_x - J_y) (x - y)

theorem bregDiv_fun_bregDiv {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x y z : E} {J_x J_y : E →L[R] F} [IsTopologicalAddGroup F] : bregDiv (fun (w : E) => bregDiv f w y J_y) z x (J_x - J_y) = bregDiv f z x J_x

theorem bregDiv_add {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {x y : E} {J₁ J₂ : E →L[R] F} [ContinuousAdd F] (f₁ f₂ : E → F) : bregDiv (f₁ + f₂) x y (J₁ + J₂) = bregDiv f₁ x y J₁ + bregDiv f₂ x y J₂

theorem fun_bregDiv_add {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {x y : E} {J₁ J₂ : E →L[R] F} [ContinuousAdd F] (f₁ f₂ : E → F) : bregDiv (fun (i : E) => f₁ i + f₂ i) x y (J₁ + J₂) = bregDiv f₁ x y J₁ + bregDiv f₂ x y J₂

Eta-expanded form of bregDiv_add

theorem bregDiv_prod {R : Type u_1} {E₁ : Type u_3} {E₂ : Type u_4} {F : Type u_5} [Ring R] [AddCommGroup E₁] [Module R E₁] [TopologicalSpace E₁] [AddCommGroup E₂] [Module R E₂] [TopologicalSpace E₂] [AddCommGroup F] [Module R F] [TopologicalSpace F] [ContinuousAdd F] (f₁ : E₁ → F) (f₂ : E₂ → F) (x y : E₁ × E₂) (J₁ : E₁ →L[R] F) (J₂ : E₂ →L[R] F) : bregDiv (fun (p : E₁ × E₂) => f₁ p.1 + f₂ p.2) x y (J₁.coprod J₂) = bregDiv f₁ x.1 y.1 J₁ + bregDiv f₂ x.2 y.2 J₂

@[simp]

theorem bregDiv_const {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {x y : E} (c : F) : bregDiv (fun (x : E) => c) x y 0 = 0

@[simp]

theorem bregDiv_linear {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {x y : E} (h : E →L[R] F) : bregDiv (⇑h) x y h = 0

@[simp]

theorem bregDiv_add_const {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x y : E} {J : E →L[R] F} (c : F) : bregDiv (fun (z : E) => f z + c) x y J = bregDiv f x y J

@[simp]

theorem bregDiv_const_add {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x y : E} {J : E →L[R] F} (c : F) : bregDiv (fun (z : E) => c + f z) x y J = bregDiv f x y J

@[simp]

theorem bregDiv_add_linear {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x y : E} {J : E →L[R] F} [ContinuousAdd F] (h : E →L[R] F) : bregDiv (fun (z : E) => f z + h z) x y (J + h) = bregDiv f x y J

@[simp]

theorem bregDiv_neg {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x y : E} {J : E →L[R] F} [IsTopologicalAddGroup F] : bregDiv (-f) x y (-J) = -bregDiv f x y J

@[simp]

theorem fun_bregDiv_neg {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x y : E} {J : E →L[R] F} [IsTopologicalAddGroup F] : bregDiv (fun (i : E) => -f i) x y (-J) = -bregDiv f x y J

Eta-expanded form of bregDiv_neg

theorem bregDiv_comp_neg {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x y : E} {J : E →L[R] F} [IsTopologicalAddGroup F] : bregDiv (fun (z : E) => f (-z)) x y (-J) = bregDiv f (-x) (-y) J

theorem bregDiv_comp_add_right {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {x y : E} {J : E →L[R] F} (x₀ : E) : bregDiv (fun (z : E) => f (z + x₀)) x y J = bregDiv f (x + x₀) (y + x₀) J

theorem bregDiv_comp_affine {R : Type u_1} {E : Type u_2} {E₁ : Type u_3} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup E₁] [Module R E₁] [TopologicalSpace E₁] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} {J : E →L[R] F} {A : E₁ →L[R] E} {b : E} {x y : E₁} : bregDiv (fun (z : E₁) => f (A z + b)) x y (J ∘SL A) = bregDiv f (A x + b) (A y + b) J

theorem bregDiv_comp {R : Type u_1} {E : Type u_2} {F : Type u_5} {G : Type u_6} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [AddCommGroup G] [Module R G] [TopologicalSpace G] {f₁ : E → F} {f₂ : F → G} {J₁ : E →L[R] F} {J₂ : F →L[R] G} {x y : E} : bregDiv (f₂ ∘ f₁) x y (J₂ ∘SL J₁) = bregDiv f₂ (f₁ x) (f₁ y) J₂ + J₂ (bregDiv f₁ x y J₁)

theorem bregDiv_mul {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] {R' : Type u_7} [CommRing R'] [TopologicalSpace R'] [ContinuousAdd R'] [ContinuousConstSMul R' R'] [Module R' E] (f₁ f₂ : E → R') (x y : E) (J₁ J₂ : E →L[R'] R') : bregDiv (f₁ * f₂) x y (f₂ y • J₁ + f₁ y • J₂) = bregDiv f₁ x y J₁ * f₂ y + f₁ y * bregDiv f₂ x y J₂ + (f₁ x - f₁ y) * (f₂ x - f₂ y)

First-order product rule for Bregman divergences.

theorem fun_bregDiv_mul {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] {R' : Type u_7} [CommRing R'] [TopologicalSpace R'] [ContinuousAdd R'] [ContinuousConstSMul R' R'] [Module R' E] (f₁ f₂ : E → R') (x y : E) (J₁ J₂ : E →L[R'] R') : bregDiv (fun (i : E) => f₁ i * f₂ i) x y (f₂ y • J₁ + f₁ y • J₂) = bregDiv f₁ x y J₁ * f₂ y + f₁ y * bregDiv f₂ x y J₂ + (f₁ x - f₁ y) * (f₂ x - f₂ y)

Eta-expanded form of bregDiv_mul

---

First-order product rule for Bregman divergences.

theorem bregDiv_le_of_le_of_eq {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] {F' : Type u_7} [AddCommGroup F'] [Module R F'] [TopologicalSpace F'] [Preorder F'] [AddRightMono F'] {f₁ f₂ : E → F'} {x y : E} {J_y : E →L[R] F'} (h_le : f₁ x ≤ f₂ x) (h_eq : f₁ y = f₂ y) : bregDiv f₁ x y J_y ≤ bregDiv f₂ x y J_y

theorem bregDiv_smul {E : Type u_2} {F : Type u_5} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] {R' : Type u_7} [CommRing R'] [Module R' E] [Module R' F] [ContinuousConstSMul R' F] (c : R') (f : E → F) (x y : E) (J : E →L[R'] F) : bregDiv (c • f) x y (c • J) = c • bregDiv f x y J

theorem bregDiv_convexCombination {E : Type u_2} {F : Type u_5} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] {R' : Type u_7} [CommRing R'] [Module R' E] [Module R' F] [ContinuousConstSMul R' F] [ContinuousAdd F] (f : E → F) (x y : E) (J₁ J₂ : E →L[R'] F) {a b : R'} (hab : a + b = 1) : bregDiv f x y (a • J₁ + b • J₂) = a • bregDiv f x y J₁ + b • bregDiv f x y J₂

theorem ConvexOn.bregDiv {R : Type u_1} {E : Type u_2} {F : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] {f : E → F} [PartialOrder R] [PartialOrder F] [IsOrderedAddMonoid F] {s : Set E} (hf : ConvexOn R s f) (J : E →L[R] F) (y : E) : ConvexOn R s fun (x : E) => _root_.bregDiv f x y J

If f is convex on s, then x ↦ D_[f](x, y, J) is convex on s for any continuous linear map J.