SmoothnessEquivalences: 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.

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

Samplinglib mathematical lesson

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

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

Read this first

Mathematical 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].\]

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.

Download module (.lean)

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

Proof roadmap

1Add 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.
2Turn 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.
3Recover 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.

Full assumptions and notation

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 verification

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

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.

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib 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.

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 quadratic upper model is equivalent to a Hessian upper bound

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

Read this first

Mathematical 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].\]

Lean statement · upper_model_iff_fderiv2_upper

Download module (.lean)

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

Proof roadmap

1Use the C¹ equivalence
C² implies C¹, so the preceding theorem replaces the upper model by its one-sided gradient inequality.
2Apply 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.
3Reverse 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.

Full assumptions and notation

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 verification

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

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.

Download module (.lean)

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib 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.

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