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

A strongly convex gradient step contracts distances

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContraction.gradient_step_contraction · theorem · Teaching coverage

Statement

For every pair x,y, the actual step T satisfies the displayed contraction estimate under the stated global curvature and step conditions.

\[\begin{gathered}T(x)=x-h\nabla f(x),\\r=\sqrt{1-\alpha h},\\f(y)\le f(x)+\langle\nabla f(x),y-x\rangle\\{}+\frac\beta2\|y-x\|^2,\\\|T(y)-T(x)\|\le r\|y-x\|.\end{gathered}\]

All objects and hypotheses

  • E is a complete real inner-product space, f:E→ℝ is C¹, and all point quantifiers range over E. The gradient is the genuine Riesz representative of its Fréchet derivative.
  • The real parameters α, β and h are nonnegative and βh≤1.
  • f is α-strongly convex on all E: the convex chord inequality has the subtraction (α/2)t(1−t)‖y−x‖² for t∈[0,1]. The displayed β quadratic upper model holds for all x,y.
  • Write T(x)=x−h∇f(x) and r=√(1−αh), with the nonnegative real square root (zero on negative arguments).

Mathematical proof

1. Use the two compiled curvature inequalities

For arbitrary x,y define v=y−x, d=∇f(y)−∇f(x) and p=⟨d,v⟩. Strong convexity with α≥0 supplies convexity and the lower pairing bound. Cocoercivity supplies the upper gradient-square bound.

\[\begin{gathered}\alpha\|v\|^2\le p,\quad p\ge0,\\\|d\|^2\le\beta p.\end{gathered}\]
Corresponding Lean step

StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn; UniformConvexOn.convexOn; ConvexSmoothGradient.gradient_cocoercive.

2. Expand one actual step

Since h≥0 and βh≤1, multiplying the cocoercivity bound by h² gives h²‖d‖²≤h²βp≤hp. Insert this into the exact squared-norm expansion, then use hp≥αh‖v‖².

\[\begin{gathered}\|v-hd\|^2=\|v\|^2-2hp+h^2\|d\|^2,\\\|v-hd\|^2\le\|v\|^2-hp\\\le(1-\alpha h)\|v\|^2.\end{gathered}\]
Corresponding Lean step

norm_sub_sq_real, inner_smul_right, norm_smul; three mul_le_mul_of_nonneg_left applications and nlinarith.

3. Take a square root without adding compatibility

The squared norm is nonnegative. Taking square roots and factoring the nonnegative factor ‖v‖² yields the asserted distance bound. If 1−αh is negative and v≠0, the squared estimate is impossible; hence no nontrivial negative-coefficient case is hidden.

\[\sqrt{(1-\alpha h)\|v\|^2}=r\|v\|.\]
Corresponding Lean step

Real.le_sqrt_of_sq_le; Real.sqrt_mul' with sq_nonneg; Real.sqrt_sq with norm_nonneg.

Lean statement · gradient_step_contraction

For every pair x,y, the actual step T satisfies the displayed contraction estimate under the stated global curvature and step conditions.

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_step_contraction {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 ≤ β) (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ≤
      Real.sqrt (1 - α * h) * ‖y - x‖

Exact module and namespace context

Lean proof · gradient_step_contraction

For arbitrary x,y define v=y−x, d=∇f(y)−∇f(x) and p=⟨d,v⟩. Strong convexity with α≥0 supplies convexity and the lower pairing bound. Cocoercivity supplies the upper gradient-square bound. Since h≥0 and βh≤1, multiplying the cocoercivity bound by h² gives h²‖d‖²≤h²βp≤hp. Insert this into the exact squared-norm expansion, then use hp≥αh‖v‖². The squared norm is nonnegative. Taking square roots and factoring the nonnegative factor ‖v‖² yields the asserted distance bound. If 1−αh is negative and v≠0, the squared estimate is impossible; hence no nontrivial negative-coefficient case is hidden.

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_step_contraction {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 ≤ β) (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ≤
      Real.sqrt (1 - α * h) * ‖y - x‖ := by
  have hc : ConvexOn ℝ univ f := hsc.convexOn (by intro r; positivity)
  have hm := StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn
    hsc (fun z _ => (hf.differentiable_one z).hasGradientAt) (mem_univ x) (mem_univ y)
  have hg := ConvexSmoothGradient.gradient_cocoercive hf hc hβ hu x y
  have hp : 0 ≤ inner ℝ (gradient f y - gradient f x) (y - x) :=
    le_trans (mul_nonneg hα (sq_nonneg _)) hm
  have hg' := mul_le_mul_of_nonneg_left hg (sq_nonneg h)
  have hs := mul_le_mul_of_nonneg_left hstep (mul_nonneg hh hp)
  have hm' := mul_le_mul_of_nonneg_left hm hh
  have hv : (y - h • gradient f y) - (x - h • gradient f x) =
      (y - x) - h • (gradient f y - gradient f x) := by rw [smul_sub]; abel
  have hb : ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ^ 2 ≤
      (1 - α * h) * ‖y - x‖ ^ 2 := by
    rw [hv, norm_sub_sq_real, inner_smul_right,
      real_inner_comm (gradient f y - gradient f x), norm_smul,
      Real.norm_eq_abs, mul_pow, sq_abs]
    nlinarith
  simpa only [Real.sqrt_mul' _ (sq_nonneg _), Real.sqrt_sq (norm_nonneg _)] using
    Real.le_sqrt_of_sq_le hb

/-- The actual Nth gradient-descent iterate has geometric, then exponential,
distance control about a supplied global minimizer. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • C¹ on a complete real inner-product space is an explicit extension of the section’s C² Euclidean setting. The source reciprocal restriction is recovered for β>0; the division-free statement also includes β=0 and h=0. If 1−αh<0, the squared bound forces every pairwise distance to vanish, so the norm result remains valid on a singleton space without an unjustified α≤β assumption. No constrained-domain, Riemannian or stochastic method is covered; this is shared optimization background, not companion-paper progress.
  • The source prints h≤1/β without stating h≥0. Nonnegative step is essential: f(t)=t²/2, α=β=1 and h=−1 gives T(t)=2t, contradicting the claimed factor √2 for distinct points. The reciprocal formula additionally needs β>0. The stray gradient before y−x in the middle proof display is a transcription typo, resolved by the preceding expansion and Proposition1.6.
  • The source specializes to h=1/β and κ=β/α. For 0<α≤β, r^N=(1−1/κ)^(N/2) and the exponential factor is exp(−N/(2κ)). This unit does not formalize the subsequent logarithmic iteration-complexity statement or the improved step of Exercise3.2.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • UniformConvexOn.convexOn; ContDiff.differentiable_one; DifferentiableAt.hasGradientAt
  • norm_sub_sq_real; inner_smul_right; norm_smul; mul_le_mul_of_nonneg_left; Real.le_sqrt_of_sq_le; Real.sqrt_mul'; Real.sqrt_sq

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.