Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Bench / optimisation

sogb-010 · public-dev · editorial and formal status separate

Reading a PL inequality before using an algorithm

Optimisation · natural-language: L1 (author-assigned; calibration pending)

Why this difficulty?

Read the PL inequality, objective gap and parameter normalization; do not derive an iteration bound.

Editorial review and exact formal-coverage boundary

AI editorial review accepted. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.

  • The full explanatory answer has no equivalent Lean task. In particular the ordinary differentiable-function interpretation, terminology distinctions and warnings against inferring an unprovided algorithmic rate are prose review findings, not an alignment certificate.

Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.

Assumptions and conventions

  • f is differentiable on a real finite-dimensional Euclidean space and attains its global minimum f* at z. Let \(α>0\). Use the convention \(2α(f(x)-f*)\le \|\nabla f(x)\|^{2}\) for all x.

Natural-language question

What is the objective gap, what does the PL inequality compare, and is convexity part of this definition? Identify the roles of \(α\) and the gradient. Do not infer a gradient-descent rate without a step rule and a descent estimate.

Reference mathematical proof

  1. The objective gap is \(f(x)-f*\), which is nonnegative by global minimality. The parameter \(α\) is a positive PL modulus in the stated factor-two convention.

  2. The inequality \[2\alpha(f(x)-f_*)\le\|\nabla f(x)\|^2\] compares an objective-value gap with squared gradient norm. It is not a bound on distance to z.

  3. Convexity is not one of the stated PL hypotheses. Do not insert a convexity or strong-convexity premise just because these conditions often appear in nearby optimization theorems.

  4. An algorithmic rate additionally needs an actual update, a step restriction and a suitable decrease estimate. This question is about the condition itself, not that convergence proof.

Formal support and missing Lean alignment

The local iteration theorem uses a more general algebraic PL hypothesis and a totalized gradient. This introductory differentiable-function QA is not an exact aligned Lean task.

Assessment rubric · 4 points
  1. Identifies \(f(x)-f*\) and explains its nonnegativity. (1 point)
  2. States the gap versus squared-gradient comparison with the correct factor \(2α\). (1 point)
  3. Does not include convexity or a distance conclusion in the definition. (1 point)
  4. Separates the condition from an algorithmic convergence theorem. (1 point)

Lean view: not yet aligned

The local iteration theorem uses a more general algebraic PL hypothesis and a totalized gradient. This introductory differentiable-function QA is not an exact aligned Lean task.

This support theorem does not certify the complete QA or its explanatory counterexamples.

What this does—and does not—verify

No convexity equivalence, error bound in distance, or convergence rate is asserted by this terminology question.

Existing library mathematics reused; no new mathematical leaf or paper-completion credit. The editorial panel records the exact current review scope and remaining unformalized explanation.

Sources, graph location and dependencies

Original definition-reading companion to the existing local PL iteration result.

Exact local source and full context · Locate the existing Lean declaration

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL.gradient_descent_pl_value_bound

ASTIS formal support (not an equivalent QA)

    Mathlib facts / definitions

      Binding SHA-256: 7e2364e8fcf6653f355ba88b88d71d81b69d2e3959e42df0e523a13352a1b94d