Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

Convex smooth gradients are cocoercive

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSmoothGradient.gradient_cocoercive · theorem · Teaching coverage

Statement

For a nonnegative real β and a C¹ convex real-valued function on a complete real inner-product space satisfying the global β quadratic upper model, every ordered pair x,y satisfies the division-free cocoercivity inequality.

\[\begin{gathered}f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac\beta2\|y-x\|^2\\[4pt]B_f(y,x):=f(y)-f(x)-\langle\nabla f(x),y-x\rangle\\[4pt]\|\nabla f(y)-\nabla f(x)\|^2\le\beta\langle\nabla f(y)-\nabla f(x),y-x\rangle\end{gathered}\]

All objects and hypotheses

  • E is a complete real inner-product space, f:E→ℝ, and all points range over the entire space E.
  • f is C¹ (ContDiff ℝ 1 f) and convex on E (ConvexOn ℝ Set.univ f). No second derivative is assumed.
  • The genuine gradient is the Riesz representative of the Fréchet derivative. The displayed quadratic upper model holds for every x,y.
  • β is a nonnegative real number, including zero.

Mathematical proof

1. Use a strictly positive relaxed modulus

Fix x,y and set d=∇f(y)−∇f(x). For ε>0, the β upper model implies the (β+ε) model because squared norm is nonnegative. Thus the positive-modulus Bregman bound applies even when β=0.

\[\|d\|^2\le2(\beta+\varepsilon)B_f(y,x),\qquad\|d\|^2\le2(\beta+\varepsilon)B_f(x,y).\]
Corresponding Lean step

hu' follows by real arithmetic from hu and sq_nonneg; two calls of gradient_gap_sq_le_bregman.

2. Exchange endpoints and add

The values f(x),f(y) cancel. The two Bregman gaps sum to the gradient-displacement pairing, while reversing the gradient difference preserves its squared norm.

\[B_f(y,x)+B_f(x,y)=\langle d,y-x\rangle,\qquad\|d\|^2\le(\beta+\varepsilon)\langle d,y-x\rangle.\]
Corresponding Lean step

hxy and hyx; norm_sub_rev, inner_neg_right, inner_sub_left and nlinarith.

3. Include the zero boundary by a real limit

Let ε decrease to zero. The right side is affine and continuous in ε, and order is closed in ℝ. This proves the scaled bound for all β≥0. At β=0 the norm square must be zero, so the gradient is constant; no inverse at zero is used.

\[\|\nabla f(y)-\nabla f(x)\|^2\le\beta\langle\nabla f(y)-\nabla f(x),y-x\rangle\]
Corresponding Lean step

Tendsto.add/mul and tendsto_id.mono_left nhdsWithin_le_nhds; ge_of_tendsto with self_mem_nhdsWithin.

Lean statement · gradient_cocoercive

For a nonnegative real β and a C¹ convex real-valued function on a complete real inner-product space satisfying the global β quadratic upper model, every ordered pair x,y satisfies the division-free cocoercivity inequality.

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_cocoercive {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 ≤
      β * inner ℝ (gradient f y - gradient f x) (y - x)

Exact module and namespace context

Lean proof · gradient_cocoercive

Fix x,y and set d=∇f(y)−∇f(x). For ε>0, the β upper model implies the (β+ε) model because squared norm is nonnegative. Thus the positive-modulus Bregman bound applies even when β=0. The values f(x),f(y) cancel. The two Bregman gaps sum to the gradient-displacement pairing, while reversing the gradient difference preserves its squared norm. Let ε decrease to zero. The right side is affine and continuous in ε, and order is closed in ℝ. This proves the scaled bound for all β≥0. At β=0 the norm square must be zero, so the gradient is constant; no inverse at zero is used.

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_cocoercive {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 ≤
      β * inner ℝ (gradient f y - gradient f x) (y - x) := by
  have he (ε : ℝ) (hε : 0 < ε) :
      ‖gradient f y - gradient f x‖ ^ 2 ≤
        (β + ε) * inner ℝ (gradient f y - gradient f x) (y - x) := by
    have hu' (a b : E) : f b ≤ f a + inner ℝ (gradient f a) (b - a) +
        (β + ε) / 2 * ‖b - a‖ ^ 2 := by
      have := hu a b
      nlinarith [sq_nonneg ‖b - a‖]
    have hxy := gradient_gap_sq_le_bregman hf hc (add_pos_of_nonneg_of_pos hβ hε) hu' x y
    have hyx := gradient_gap_sq_le_bregman hf hc (add_pos_of_nonneg_of_pos hβ hε) hu' y x
    rw [norm_sub_rev (gradient f x), show x - y = -(y - x) by abel, inner_neg_right] at hyx
    rw [inner_sub_left]
    nlinarith
  have ht : Tendsto (fun ε : ℝ => (β + ε) *
      inner ℝ (gradient f y - gradient f x) (y - x)) (𝓝[>] 0)
      (𝓝 (β * inner ℝ (gradient f y - gradient f x) (y - x))) := by
    simpa using (tendsto_const_nhds.add (tendsto_id.mono_left nhdsWithin_le_nhds :
      Tendsto (fun ε : ℝ => ε) (𝓝[>] 0) (𝓝 0))).mul tendsto_const_nhds
  apply ge_of_tendsto ht
  filter_upwards [self_mem_nhdsWithin] with ε hε
  exact he ε hε

/-- A C¹ convex function with the global quadratic upper model has a
`β`-Lipschitz gradient, including `β = 0`. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • The complete real inner-product space explicitly generalizes the source Euclidean space. A constrained set is not covered: the trial gradient step must remain in the domain. No Riemannian, stochastic, or companion-paper theorem is claimed.
  • Definition1.12 permits β≥0, but the reciprocal in (3.4) and the suggested step 1/β require β>0; the source does not state that restriction explicitly. The first declaration covers this positive domain. The scaled (3.5) and Lipschitz conclusions are separately established at β=0.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • norm_sub_rev; inner_neg_right; inner_sub_left
  • Tendsto.add; Tendsto.mul; tendsto_id; nhdsWithin_le_nhds; ge_of_tendsto; self_mem_nhdsWithin

Mathematical sources

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.