ASTIS mathematical exposition

A quadratic upper model is equivalent to a one-sided gradient bound

AutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalences.upper_model_iff_gradient_upper · theorem · Teaching coverage

Statement

For every C¹ real-valued function f on a complete real inner-product space and every real β, the global quadratic upper model with coefficient β/2 holds if and only if the gradient difference has inner product with the displacement at most β times squared displacement.

\[\bigl[\forall x,y,\ f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac\beta2\|y-x\|^2\bigr]\quad\Longleftrightarrow\quad\bigl[\forall x,y,\ \langle\nabla f(y)-\nabla f(x),y-x\rangle\le\beta\|y-x\|^2\bigr].\]

All objects and hypotheses

E is a complete real inner-product space; all points and directions range over E. The domain is the whole space.
β is any real number, including zero and negative values. This explicitly generalizes the source parameter range β≥0 and Euclidean domain.
The gradient is the actual Mathlib Riesz gradient of the Fréchet derivative. No convexity assumption is imposed.
f is continuously Fréchet differentiable everywhere (ContDiff ℝ 1 f).

Mathematical proof

1. Add the two endpoint models

Write the upper model from x to y and from y to x. The values cancel on addition; the linear terms combine with opposite displacements. Each quadratic correction is β‖y−x‖²/2.

\[0\le-\langle\nabla f(y)-\nabla f(x),y-x\rangle+\beta\|y-x\|^2.\]

Corresponding Lean step

hxy and hyx, inner_neg_right and norm_neg; linarith derives the bound.

2. Turn the upper bound into a signed lower bound

For the converse set g=−f and m=−β. Linearity of the derivative and Riesz map gives ∇g=−∇f. The assumed one-sided upper bound becomes quantitative gradient monotonicity of g with signed modulus m.

\[\langle\nabla g(y)-\nabla g(x),y-x\rangle\ge(-\beta)\|y-x\|^2.\]

Corresponding Lean step

hg proves actual gradient negation; ConvexityC1.strongConvexOn_univ_of_gradient_mono_integral applies with m=-β.

3. Recover the endpoint model through the existing integral route

The signed gradient-to-chord theorem integrates along affine segments; C¹ supplies derivative continuity and interval integrability. Its chord conclusion and the genuine gradient yield the existing first-order lower model for g. Negating this inequality gives exactly the upper model for f, with coefficient β/2.

\[-f(y)\ge-f(x)-\langle\nabla f(x),y-x\rangle-\frac\beta2\|y-x\|^2.\]

Corresponding Lean step

StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn uses hf.neg.differentiable_one.hasGradientAt; hg and linarith finish.

Lean statement · upper_model_iff_gradient_upper

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 upper_model_iff_gradient_upper {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 1 f) :
    (∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2) ↔
    ∀ x y, inner ℝ (gradient f y - gradient f x) (y - x) ≤ β * ‖y - x‖ ^ 2

Exact module and namespace context

Lean proof · upper_model_iff_gradient_upper

Write the upper model from x to y and from y to x. The values cancel on addition; the linear terms combine with opposite displacements. Each quadratic correction is β‖y−x‖²/2. For the converse set g=−f and m=−β. Linearity of the derivative and Riesz map gives ∇g=−∇f. The assumed one-sided upper bound becomes quantitative gradient monotonicity of g with signed modulus m. The signed gradient-to-chord theorem integrates along affine segments; C¹ supplies derivative continuity and interval integrability. Its chord conclusion and the genuine gradient yield the existing first-order lower model for g. Negating this inequality gives exactly the upper model for f, with coefficient β/2.

theorem upper_model_iff_gradient_upper {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 1 f) :
    (∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2) ↔
    ∀ x y, inner ℝ (gradient f y - gradient f x) (y - x) ≤ β * ‖y - x‖ ^ 2 := by
  have hg (x : E) : gradient (fun z => -f z) x = -gradient f x := by
    simp [gradient]
  constructor
  · intro h x y
    have hxy := h x y
    have hyx := h y x
    rw [show x - y = -(y - x) by abel, inner_neg_right, norm_neg] at hyx
    rw [inner_sub_left]
    linarith
  · intro h
    have hn : StrongConvexOn (univ : Set E) (-β) (fun z => -f z) :=
      ConvexityC1.strongConvexOn_univ_of_gradient_mono_integral hf.neg (by
        intro x y
        rw [hg, hg, inner_sub_left, inner_neg_left, inner_neg_left]
        have hxy := h x y
        rw [inner_sub_left] at hxy
        linarith)
    intro x y
    have hl := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn hn
      (fun z _ => (hf.neg.differentiable_one z).hasGradientAt) (mem_univ x) (mem_univ y)
    rw [hg, inner_neg_left] at hl
    linarith

/-- With genuine C² regularity the same upper model is equivalent to the
Hessian diagonal upper bound, without assuming convexity. -/

Exact module and namespace context

Scope and omitted-condition boundaries

These are one-sided upper bounds. They do not imply a β-Lipschitz gradient without an additional condition such as convexity; no such implication is asserted here. The source instance is E=ℝᵈ and β≥0.
The source omits the proof by reference to Proposition 1.6. The explicit sign reversal reuses its already compiled signed integral and derivative-limit ingredients.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContDiff.neg; ContDiff.differentiable_one; DifferentiableAt.hasGradientAt
gradient; fderiv_fun_neg; map_neg; inner_sub_left; inner_neg_left; inner_neg_right; norm_neg

Mathematical sources

Sinho Chewi, Definition 1.12 and Proposition 1.13 — ASTIS-authored explanation, expanding the omitted proof using Proposition 1.6.
Sharp quadratics, nonconvex boundary and descent consumer — Tests actual declarations; no theorem status inferred from examples.

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