Samplinglib mathematical lesson

A finite run contains a subgradient iterate with the convergence bound

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

Read this first

Mathematical statement

Under the same Lipschitz, support and exact-update assumptions, suppose every step is strictly positive and N>0. For any comparator z, some index i<N satisfies the displayed normalized best-iterate objective-gap bound.

\[\exists i<N:\quad f(x_i)-f(z)\le\frac{\|x_0-z\|^2+G^2\sum_{k=0}^{N-1}a_k^2}{2\sum_{k=0}^{N-1}a_k}.\]

Lean statement · exists_gap_le

A positive finite subgradient run has a best index with the normalized objective-gap guarantee.

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 exists_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 : ℕ} (hN : 0 < N) :
    ∃ i < N, f (x i) - f z ≤
      (‖x 0 - z‖ ^ 2 + (G : ℝ) ^ 2 * (∑ k ∈ Finset.range N, (a k) ^ 2)) /
        (2 * ∑ k ∈ Finset.range N, a k)

Exact module and namespace context

Proof roadmap

1Take a genuine finite minimum
Choose i minimizing f(x_k) among k<N. This finite choice exists because N>0; it is not a default value of a totalized infimum.
2Compare the best gap to the weighted gaps
Multiply each minimum inequality by a_k≥0 and sum. Apply the preceding actual-update telescope, then discard only the nonnegative terminal squared distance.
3Divide only on the positive domain
The sum of positive steps over a nonempty finite range is positive. Dividing by twice that sum preserves the inequality and produces the claimed witness.

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; a:ℕ→ℝ with a_k>0; each v_k supports f at x_k; x_(k+1)=x_k−a_k v_k for every k.
N>0, so the finite index set is nonempty and the sum of its positive step sizes is strictly positive.
z is arbitrary. Neither attainment of the global infimum nor differentiability is supplied.

Mathematical proof

1. Take a genuine finite minimum

Choose i minimizing f(x_k) among k<N. This finite choice exists because N>0; it is not a default value of a totalized infimum.

\[i<N,\qquad f(x_i)\le f(x_k)\quad(k<N).\]

Corresponding Lean step

Finset.exists_min_image; range nonempty from 0<N.

2. Compare the best gap to the weighted gaps

Multiply each minimum inequality by a_k≥0 and sum. Apply the preceding actual-update telescope, then discard only the nonnegative terminal squared distance.

\[\begin{aligned}\left(\sum_{k<N}a_k\right)(f(x_i)-f(z))&\le\sum_{k<N}a_k(f(x_k)-f(z)),\\2\left(\sum_{k<N}a_k\right)(f(x_i)-f(z))&\le\|x_0-z\|^2+G^2\sum_{k<N}a_k^2.\end{aligned}\]

Corresponding Lean step

Finset.sum_le_sum; Finset.sum_mul; sum_weighted_gap_le; sq_nonneg.

3. Divide only on the positive domain

The sum of positive steps over a nonempty finite range is positive. Dividing by twice that sum preserves the inequality and produces the claimed witness.

\[2\sum_{k<N}a_k>0.\]

Corresponding Lean step

Finset.sum_pos; le_div_iff₀. No zero-step quotient is asserted.

Lean verification

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

Lean proof · exists_gap_le

Choose a minimizing finite index, bound its gap by the weighted gaps, use the actual-update telescope, and divide by the proved positive total step.

Download module (.lean)

theorem exists_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 : ℕ} (hN : 0 < N) :
    ∃ i < N, f (x i) - f z ≤
      (‖x 0 - z‖ ^ 2 + (G : ℝ) ^ 2 * (∑ k ∈ Finset.range N, (a k) ^ 2)) /
        (2 * ∑ k ∈ Finset.range N, a k) := by
  have hne : (Finset.range N).Nonempty := ⟨0, Finset.mem_range.mpr hN⟩
  obtain ⟨i, hi, hmin⟩ := Finset.exists_min_image (Finset.range N) (fun k => f (x k)) hne
  refine ⟨i, Finset.mem_range.mp hi, ?_⟩
  have hsumpos : 0 < ∑ k ∈ Finset.range N, a k :=
    Finset.sum_pos (fun k _ => ha k) hne
  have hlower : (∑ k ∈ Finset.range N, a k) * (f (x i) - f z) ≤
      ∑ k ∈ Finset.range N, a k * (f (x k) - f z) := by
    rw [Finset.sum_mul]
    exact Finset.sum_le_sum fun k hk =>
      mul_le_mul_of_nonneg_left (sub_le_sub_right (hmin k hk) _) (ha k).le
  have he := sum_weighted_gap_le hf (fun k => (ha k).le) hs hx z N
  apply (le_div_iff₀ (mul_pos (by norm_num : (0 : ℝ) < 2) hsumpos)).mpr
  nlinarith [sq_nonneg ‖x N - z‖]

end AutoSamplingTheory.TechnicalLemmas.Analysis.SubgradientMethod

Exact module and namespace context

Scope and omitted-condition boundaries

The upstream theorem writes the best finite value as a real sInf over k+1 iterates. An actual minimizing index is equivalent on this nonempty finite set; N>0 corresponds to its k+1 horizon.
No claim is made about the last iterate, existence of subgradient selectors, asymptotic iterate convergence, stochastic selection, PBPS/SPHMC or sampling complexity.
These are reusable Optlib-source components placed beside Optimisation Chapter6; the complete Chewi chapter statement/route is not silently declared finished.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.SubgradientMethod.sum_weighted_gap_le

Mathlib API called (external library)

Finset.exists_min_image
Finset.sum_pos
Finset.sum_le_sum
Finset.sum_mul
le_div_iff₀

Mathematical sources

Optlib subgradient_method_converge — Equivalent finite-index normalized formulation of the source best-value bound.
Actual |x| recurrence — Concrete nonsmooth, nonconstant iterates with no smoothness 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.