The Bregman gap controls the gradient difference

Fix x,y and write d=∇f(y)−∇f(x), z=y−d/β. Convexity and the actual gradient give the supporting-plane lower bound at x. This says f minus its tangent plane at x is minimized at x. The positive β makes the trial step meaningful. Apply the original upper model from y to z. Insert z−y=−d/β and z−x=(y−x)−d/β in the two models. Combining the inequalities eliminates f(z). The difference of the two linear terms is ⟨d,d⟩/β. Multiplication by 2β gives the shared division-free statement. The Lean proof carries out the same field arithmetic with β≠0 and positive reciprocal. The source reciprocal form is only recovered for β>0.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem gradient_gap_sq_le_bregman {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 1 f) (hc : ConvexOn ℝ univ f) (hβ : 0 < β)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖gradient f y - gradient f x‖ ^ 2 ≤
      2 * β * (f y - f x - inner ℝ (gradient f x) (y - x)) := by
  let d := gradient f y - gradient f x
  let z := y - β⁻¹ • d
  have hl := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
    (strongConvexOn_zero.mpr hc)
    (fun w _ => (hf.differentiable_one w).hasGradientAt) (mem_univ x) (mem_univ z)
  simp only [zero_div, zero_mul, add_zero] at hl
  have hh := hu y z
  have hzx : z - x = (y - x) - β⁻¹ • d := by dsimp [z]; abel
  rw [hzx, inner_sub_right, inner_smul_right] at hl
  have hzy : z - y = -(β⁻¹ • d) := by dsimp [z]; abel
  rw [hzy, inner_neg_right, inner_smul_right, norm_neg, norm_smul,
    Real.norm_eq_abs, mul_pow, sq_abs] at hh
  have hd : inner ℝ (gradient f y) d - inner ℝ (gradient f x) d = ‖d‖ ^ 2 := by
    rw [← inner_sub_left]
    exact real_inner_self_eq_norm_sq d
  have h := le_trans hl hh
  have hb : β ≠ 0 := ne_of_gt hβ
  apply (mul_le_mul_iff_right₀ (inv_pos.mpr hβ)).mp
  field_simp [hb] at h ⊢
  nlinarith

/-- Convex gradients are cocoercive in the division-free normalization.
The zero-modulus case follows by relaxing the upper model to `β + ε` and
letting positive `ε` tend to zero, without assigning meaning to a zero denominator. -/

Exact module and namespace context