Samplinglib mathematical lesson

The actual subgradient steps telescope weighted objective gaps

AutoSamplingTheory.TechnicalLemmas.Analysis.SubgradientMethod.sum_weighted_gap_le · theorem · Teaching coverage

Read this first

Mathematical statement

Let f be globally G-Lipschitz. For sequences x_k,v_k and nonnegative real steps a_k, suppose v_k supports f at x_k and x_(k+1)=x_k−a_k v_k for every k. For every comparator z and every N≥0, the weighted objective gaps obey the displayed bound, including the terminal squared distance.

\[2\sum_{k=0}^{N-1}a_k\bigl(f(x_k)-f(z)\bigr)\le\|x_0-z\|^2+G^2\sum_{k=0}^{N-1}a_k^2-\|x_N-z\|^2.\]

Lean statement · sum_weighted_gap_le

Finite weighted-gap telescope for actual Lipschitz subgradient updates with nonnegative steps.

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.

Download module (.lean)

theorem sum_weighted_gap_le {f : E → ℝ} {G : ℝ≥0} {x g : ℕ → E} {a : ℕ → ℝ}
    (hf : LipschitzWith G f) (ha : ∀ k, 0 ≤ a k)
    (hs : ∀ k, SupportsAt f (x k) (g k))
    (hx : ∀ k, x (k + 1) = x k - a k • g k) (z : E) (N : ℕ) :
    2 * (∑ k ∈ Finset.range N, a k * (f (x k) - f z)) ≤
      ‖x 0 - z‖ ^ 2 + (G : ℝ) ^ 2 * (∑ k ∈ Finset.range N, (a k) ^ 2) - ‖x N - z‖ ^ 2

Exact module and namespace context

Proof roadmap

1Turn support into a gap estimate
Use the supporting inequality at the comparator z and reverse the displacement. The norm bound is proved by the preceding theorem inside this proof; it is not a new hypothesis.
2Expand the actual update
The squared-distance identity is exact for the supplied recurrence. Multiplying the gap estimate by 2a_k is legitimate because the step is nonnegative; the squared subgradient term is at most a_k²G².
3Sum and cancel adjacent distances
Sum the one-step inequality for k=0,…,N−1. Interior squared distances cancel, leaving the initial and terminal terms. The Lean induction performs exactly this finite telescope; the empty sum is the N=0 base case.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space with its associated norm. No completeness or finite-dimensionality assumption is imposed.
G is a nonnegative real Lipschitz constant and f:E→ℝ is globally G-Lipschitz.
SupportsAt f x v means f(x)+⟨v,z−x⟩≤f(z) for every z∈E. It supplies a genuine global supporting vector; no differentiability or totalized gradient is used.
x,v:ℕ→E and a:ℕ→ℝ. Each a_k≥0; each v_k supports f at x_k; the update x_(k+1)=x_k−a_k v_k is an exact equality.
z is any comparator in E, not a supplied minimizer. N is any natural number, including zero. There is no division by a step or horizon.

Mathematical proof

1. Turn support into a gap estimate

Use the supporting inequality at the comparator z and reverse the displacement. The norm bound is proved by the preceding theorem inside this proof; it is not a new hypothesis.

\[f(x_k)-f(z)\le\langle v_k,x_k-z\rangle,\qquad\|v_k\|\le G.\]

Corresponding Lean step

SupportsAt evaluated at z; inner_sub_right; norm_le_of_supportsAt.

2. Expand the actual update

The squared-distance identity is exact for the supplied recurrence. Multiplying the gap estimate by 2a_k is legitimate because the step is nonnegative; the squared subgradient term is at most a_k²G².

\[\begin{aligned}\|x_{k+1}-z\|^2&=\|x_k-z\|^2-2a_k\langle v_k,x_k-z\rangle+a_k^2\|v_k\|^2\\&\le\|x_k-z\|^2-2a_k(f(x_k)-f(z))+a_k^2G^2.\end{aligned}\]

Corresponding Lean step

norm_sub_sq_real; norm_smul; sq_abs; pow_le_pow_left₀; mul_le_mul_of_nonneg_left.

3. Sum and cancel adjacent distances

Sum the one-step inequality for k=0,…,N−1. Interior squared distances cancel, leaving the initial and terminal terms. The Lean induction performs exactly this finite telescope; the empty sum is the N=0 base case.

\[\sum_{k=0}^{N-1}\bigl(\|x_k-z\|^2-\|x_{k+1}-z\|^2\bigr)=\|x_0-z\|^2-\|x_N-z\|^2.\]

Corresponding Lean step

Finset.sum_range_succ; induction on N; nlinarith.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · sum_weighted_gap_le

Prove the support gap and subgradient norm bounds, expand the actual squared-distance update, then telescope by induction.

Download module (.lean)

theorem sum_weighted_gap_le {f : E → ℝ} {G : ℝ≥0} {x g : ℕ → E} {a : ℕ → ℝ}
    (hf : LipschitzWith G f) (ha : ∀ k, 0 ≤ a k)
    (hs : ∀ k, SupportsAt f (x k) (g k))
    (hx : ∀ k, x (k + 1) = x k - a k • g k) (z : E) (N : ℕ) :
    2 * (∑ k ∈ Finset.range N, a k * (f (x k) - f z)) ≤
      ‖x 0 - z‖ ^ 2 + (G : ℝ) ^ 2 * (∑ k ∈ Finset.range N, (a k) ^ 2) - ‖x N - z‖ ^ 2 := by
  have hstep (k : ℕ) :
      2 * a k * (f (x k) - f z) ≤
        ‖x k - z‖ ^ 2 - ‖x (k + 1) - z‖ ^ 2 + (G : ℝ) ^ 2 * (a k) ^ 2 := by
    have hs' := hs k z
    change f (x k) + inner ℝ (g k) (z - x k) ≤ f z at hs'
    have hpair : f (x k) - f z ≤ inner ℝ (g k) (x k - z) := by
      rw [inner_sub_right] at hs' ⊢
      linarith
    have hg := norm_le_of_supportsAt hf (hs k)
    have hgsq : ‖g k‖ ^ 2 ≤ (G : ℝ) ^ 2 :=
      pow_le_pow_left₀ (norm_nonneg _) hg 2
    have hnorm : ‖x (k + 1) - z‖ ^ 2 =
        ‖x k - z‖ ^ 2 - 2 * a k * inner ℝ (g k) (x k - z) + (a k) ^ 2 * ‖g k‖ ^ 2 := by
      rw [hx k, sub_right_comm, norm_sub_sq_real, inner_smul_right,
        norm_smul, Real.norm_eq_abs, mul_pow, sq_abs, real_inner_comm (x k - z)]
      ring
    have hp := mul_le_mul_of_nonneg_left hpair (mul_nonneg (by norm_num : (0 : ℝ) ≤ 2) (ha k))
    have hn := mul_le_mul_of_nonneg_left hgsq (sq_nonneg (a k))
    nlinarith
  induction N with
  | zero => simp
  | succ N ih =>
      rw [Finset.sum_range_succ, Finset.sum_range_succ]
      nlinarith [hstep N]

Exact module and namespace context

Scope and omitted-condition boundaries

This exposes the stronger weighted intermediate estimate used by the upstream convergence proof. It does not assert monotonicity of function values or a last-iterate rate.
The source uses positive steps; allowing zero steps and N=0 here is an explicit division-free generalization, not a repair. No stochastic oracle, kernel or expected sampling cost is constructed.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

norm_sub_sq_real
norm_smul
sq_abs
Finset.sum_range_succ
mul_le_mul_of_nonneg_left

Mathematical sources

Optlib subgradient_method_converge: algorithm and one-step/telescope proof — Native extraction of the source energy estimate; exact recurrence and no optimizer assumption.

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