SubgradientMethod: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Lipschitz growth bounds every supplied subgradient
The actual subgradient steps telescope weighted objective gaps
A finite run contains a subgradient iterate with the convergence bound

Samplinglib mathematical lesson

Lipschitz growth bounds every supplied subgradient

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

Read this first

Mathematical statement

For any globally G-Lipschitz real-valued function on a real inner-product space, every global supporting vector v at x satisfies ‖v‖≤G.

\[f(x)+\langle v,z-x\rangle\le f(z)\ (\forall z)\quad\Longrightarrow\quad\|v\|\le G.\]

Lean statement · norm_le_of_supportsAt

A supplied global supporting vector of a globally G-Lipschitz objective has norm at most G.

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 norm_le_of_supportsAt {f : E → ℝ} {G : ℝ≥0} {x g : E}
    (hf : LipschitzWith G f) (hs : SupportsAt f x g) : ‖g‖ ≤ (G : ℝ)

Exact module and namespace context

Proof roadmap

1Probe in the supporting direction
Evaluate the global supporting inequality at z=x+v. The pairing is exactly ‖v‖², with no derivative or inverse norm needed.
2Use the actual Lipschitz bound
The function increment is at most its absolute value, and global Lipschitz continuity bounds that absolute value by G‖v‖.
3Keep the zero vector separate
If v=0 the result is nonnegativity of G. Otherwise ‖v‖>0, so the quadratic inequality implies ‖v‖≤G. This is the same bound as the upstream normalized-direction argument, with a division-free proof.

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.

Mathematical proof

1. Probe in the supporting direction

Evaluate the global supporting inequality at z=x+v. The pairing is exactly ‖v‖², with no derivative or inverse norm needed.

\[\|v\|^2\le f(x+v)-f(x).\]

Corresponding Lean step

SupportsAt evaluated at x+g; real_inner_self_eq_norm_sq.

2. Use the actual Lipschitz bound

The function increment is at most its absolute value, and global Lipschitz continuity bounds that absolute value by G‖v‖.

\[f(x+v)-f(x)\le |f(x+v)-f(x)|\le G\|v\|.\]

Corresponding Lean step

LipschitzWith.dist_le_mul; Real.dist_eq; le_abs_self.

3. Keep the zero vector separate

If v=0 the result is nonnegativity of G. Otherwise ‖v‖>0, so the quadratic inequality implies ‖v‖≤G. This is the same bound as the upstream normalized-direction argument, with a division-free proof.

\[\|v\|^2\le G\|v\|\quad\Longrightarrow\quad\|v\|\le G.\]

Corresponding Lean step

norm_nonneg; zero/nonzero split; nlinarith.

Lean verification

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

Lean proof · norm_le_of_supportsAt

Probe at x+v, compare the quadratic lower growth with Lipschitz upper growth, and separate the zero-norm case.

Download module (.lean)

theorem norm_le_of_supportsAt {f : E → ℝ} {G : ℝ≥0} {x g : E}
    (hf : LipschitzWith G f) (hs : SupportsAt f x g) : ‖g‖ ≤ (G : ℝ) := by
  have hs' := hs (x + g)
  change f x + inner ℝ g (x + g - x) ≤ f (x + g) at hs'
  rw [add_sub_cancel_left, real_inner_self_eq_norm_sq] at hs'
  have hl : f (x + g) - f x ≤ (G : ℝ) * ‖g‖ := by
    calc
      f (x + g) - f x ≤ |f (x + g) - f x| := le_abs_self _
      _ ≤ (G : ℝ) * ‖g‖ := by
        simpa [Real.dist_eq, dist_eq_norm] using hf.dist_le_mul (x + g) x
  by_cases hg : ‖g‖ = 0
  · simp [hg]
  · have hp : 0 < ‖g‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hg)
    nlinarith

Exact module and namespace context

Scope and omitted-condition boundaries

No existence or measurable selection of supporting vectors is claimed. The theorem does not require convexity once a global supporting vector is supplied, just as the corresponding upstream direction.
This is a native local port of the norm bound, not a bulk import of Optlib or a sampling convergence result.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient.SupportsAt

Mathlib API called (external library)

LipschitzWith.dist_le_mul
real_inner_self_eq_norm_sq
Real.dist_eq
norm_nonneg

Mathematical sources

Optlib Lipschitz_to_bounded_subgradient — Apache-2.0 source norm bound; native proof rewritten over Samplinglib SupportsAt.
Nonsmooth absolute-value iteration and endpoint tests — Focused consumers of the actual new theorems.

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

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.

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.

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.

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.