ASTIS mathematical exposition

A quadratic upper model is equivalent to a Hessian upper bound

AutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalences.upper_model_iff_fderiv2_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 genuine Hessian quadratic form at each point is at most β times squared norm in every direction.

\[\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,v,\ D^2f(x)[v,v]\le\beta\|v\|^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 twice continuously Fréchet differentiable everywhere (ContDiff ℝ 2 f).
D²f(x)[v,v] means (fderiv ℝ (fderiv ℝ f) x v) v. C² supplies its existence and continuity; no separate Hessian, symmetry or integrability premise is supplied.

Mathematical proof

1. Use the C¹ equivalence

C² implies C¹, so the preceding theorem replaces the upper model by its one-sided gradient inequality.

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

Corresponding Lean step

upper_model_iff_gradient_upper with ContDiff.of_le.

2. Apply the signed Hessian equivalence to the negative function

Set g=−f and m=−β again. Genuine first and second Fréchet derivatives commute with negation. The compiled equivalence for g uses a positive-direction derivative limit in one direction and the Hessian segment FTC in the other.

\[\nabla g=-\nabla f,\qquad D^2g=-D^2f,\qquad\langle\nabla g(y)-\nabla g(x),y-x\rangle\ge m\|y-x\|^2\ \Longleftrightarrow\ D^2g(x)[v,v]\ge m\|v\|^2.\]

Corresponding Lean step

hg and hH prove both sign identities; ConvexityC2.gradient_mono_iff_fderiv2_lower applies to hf.neg at m=-β.

3. Reverse both signs

Multiplying the two lower inequalities by −1 gives the upper gradient and Hessian bounds. Neither β nor the norm of the direction is divided by, so zero and negative β and v=0 remain valid.

\[D^2f(x)[v,v]\le\beta\|v\|^2\]

Corresponding Lean step

The two directions use Iff.mp and Iff.mpr with linear real arithmetic; no source-specific matrix field replaces fderiv.

Lean statement · upper_model_iff_fderiv2_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_fderiv2_upper {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 2 f) :
    (∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2) ↔
    ∀ x v, (fderiv ℝ (fderiv ℝ f) x v) v ≤ β * ‖v‖ ^ 2

Exact module and namespace context

Lean proof · upper_model_iff_fderiv2_upper

C² implies C¹, so the preceding theorem replaces the upper model by its one-sided gradient inequality. Set g=−f and m=−β again. Genuine first and second Fréchet derivatives commute with negation. The compiled equivalence for g uses a positive-direction derivative limit in one direction and the Hessian segment FTC in the other. Multiplying the two lower inequalities by −1 gives the upper gradient and Hessian bounds. Neither β nor the norm of the direction is divided by, so zero and negative β and v=0 remain valid.

theorem upper_model_iff_fderiv2_upper {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 2 f) :
    (∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2) ↔
    ∀ x v, (fderiv ℝ (fderiv ℝ f) x v) v ≤ β * ‖v‖ ^ 2 := by
  have hg (x : E) : gradient (fun z => -f z) x = -gradient f x := by
    simp [gradient]
  have hH (x v : E) :
      (fderiv ℝ (fderiv ℝ (fun z => -f z)) x v) v =
        -(fderiv ℝ (fderiv ℝ f) x v) v := by
    rw [show fderiv ℝ (fun z => -f z) = -fderiv ℝ f by
      funext z; exact fderiv_fun_neg]
    rw [fderiv_neg]
    rfl
  rw [upper_model_iff_gradient_upper (hf.of_le (by norm_num))]
  have h := ConvexityC2.gradient_mono_iff_fderiv2_lower (m := -β) hf.neg
  simp only [hg, inner_sub_left, inner_neg_left, hH] at h
  constructor
  · intro hu x v
    have hl := h.mp (by
      intro x y
      have hxy := hu x y
      rw [inner_sub_left] at hxy
      linarith) x v
    linarith
  · intro hu x y
    have hl := h.mpr (by intro x v; have hv := hu x v; linarith) x y
    rw [inner_sub_left]
    linarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalences

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.
This closes the C² equivalence of Proposition 1.13 when specialized to the source domain. It does not close the later convexity-to-Lipschitz consequence or an entire chapter.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContDiff.neg; ContDiff.of_le
fderiv_fun_neg; fderiv_neg; gradient; map_neg; inner_sub_left; inner_neg_left

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.