Introduction and basics of convex functions

One segment-local quadratic correction reduces the target to Mathlib scalar derivative monotonicity. Equal segment parameters are separated before positive cancellation. The final chord bound uses the exact m/2 normalization.

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 strongConvexOn_of_gradient_inner_lower_bound
    {s : Set E} {f : E → ℝ} {m : ℝ} {grad : E → E}
    (hs : Convex ℝ s)
    (hgrad : ∀ z ∈ s, HasGradientAt f (grad z) z)
    (hmono : ∀ x ∈ s, ∀ y ∈ s,
      m * ‖y - x‖ ^ 2 ≤ inner ℝ (grad y - grad x) (y - x)) :
    StrongConvexOn s m f := by
  refine ⟨hs, ?_⟩
  intro x hx y hy a b ha hb hab
  let p : ℝ → E := fun t => x + t • (y - x)
  let q : ℝ → ℝ := fun t => f (p t) - m / 2 * t ^ 2 * ‖y - x‖ ^ 2
  let q' : ℝ → ℝ := fun t => inner ℝ (grad (p t)) (y - x) - m * t * ‖y - x‖ ^ 2
  have hp : ∀ t ∈ Icc (0 : ℝ) 1, p t ∈ s := by
    intro t ht
    exact hs.add_smul_sub_mem hx hy ht
  have hq : ∀ t ∈ Icc (0 : ℝ) 1, HasDerivAt q (q' t) t := by
    intro t ht
    have hline : HasDerivAt (fun u => f (p u))
        (inner ℝ (grad (p t)) (y - x)) t := by
      have hpderiv : HasDerivAt p (y - x) t := by
        simpa [p] using ((hasDerivAt_id t).smul_const (y - x)).const_add x
      convert! (hgrad (p t) (hp t ht)).hasFDerivAt.comp_hasDerivAt t hpderiv using 1
    have hquad := (((hasDerivAt_id t).pow 2).const_mul (m / 2)).mul_const (‖y - x‖ ^ 2)
    convert! hline.sub hquad using 1
    simp only [q', id_eq]
    ring
  have hmon : MonotoneOn q' (Icc (0 : ℝ) 1) := by
    intro u hu v hv huv
    rcases eq_or_lt_of_le huv with rfl | huv
    · exact le_rfl
    have h := hmono (p u) (hp u hu) (p v) (hp v hv)
    have hdis : p v - p u = (v - u) • (y - x) := by
      simp only [p, add_sub_add_left_eq_sub, sub_smul]
    rw [hdis, inner_smul_right, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs] at h
    have hscaled : (v - u) * (m * (v - u) * ‖y - x‖ ^ 2) ≤
        (v - u) * inner ℝ (grad (p v) - grad (p u)) (y - x) := by
      nlinarith [h]
    have hbound := le_of_mul_le_mul_left hscaled (sub_pos.mpr huv)
    rw [inner_sub_left] at hbound
    dsimp [q']
    linarith
  have hconv : ConvexOn ℝ (Icc (0 : ℝ) 1) q := by
    apply MonotoneOn.convexOn_of_deriv (convex_Icc (0 : ℝ) 1)
      (fun t ht => (hq t ht).continuousAt.continuousWithinAt)
      (fun t ht => (hq t (interior_subset ht)).differentiableAt.differentiableWithinAt)
    intro u hu v hv huv
    rw [(hq u (interior_subset hu)).deriv, (hq v (interior_subset hv)).deriv]
    exact hmon (interior_subset hu) (interior_subset hv) huv
  have hchord := hconv.2 (show (0 : ℝ) ∈ Icc 0 1 by norm_num)
    (show (1 : ℝ) ∈ Icc 0 1 by norm_num) ha hb hab
  have hpoint : a • x + b • y = p b := by
    have ha' : a = 1 - b := by linarith
    simp [p, ha', sub_smul, smul_sub]
    abel
  rw [hpoint]
  simp only [smul_eq_mul, mul_zero, mul_one, zero_add] at hchord ⊢
  norm_num [q, p] at hchord
  rw [norm_sub_rev] at hchord
  have ha' : a = 1 - b := by linarith
  rw [ha'] at hchord ⊢
  dsimp [p]
  nlinarith [hchord]

end AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGradientConverse

Exact module and namespace context

The local definitions path and isSelected encode the chosen affine segment; hconvex rewrites the Mathlib chord inequality into the geodesic parent's normalization. hgrad supplies HasFDerivAt, then HasLineDerivAt; hderiv identifies the real derivative of the segment composition. simpa reconciles dist and norm conventions.

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 firstOrder_lower_bound_of_strongConvexOn
    {s : Set E} {f : E → ℝ} {m : ℝ} {grad : E → E}
    (hsc : StrongConvexOn s m f)
    (hgrad : ∀ z ∈ s, HasGradientAt f (grad z) z)
    {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
    f y ≥ f x + inner ℝ (grad x) (y - x) + m / 2 * ‖y - x‖ ^ 2 := by
  let path : ℝ → E := fun t => x + t • (y - x)
  let isSelected : (ℝ → E) → Prop := fun q => q = path
  have hpath : isSelected path := rfl
  have hconvex :
      Geometry.GeodesicConvexity.IsAlphaGeodesicallyConvex isSelected f m := by
    intro q hq t ht
    subst q
    have hnonneg_left : 0 ≤ 1 - t := sub_nonneg.mpr ht.2
    have hnonneg_right : 0 ≤ t := ht.1
    have hstrong := hsc.2 hx hy hnonneg_left hnonneg_right (by ring)
    have hpoint : path t = (1 - t) • x + t • y := by
      dsimp only [path]
      rw [smul_sub, sub_smul, one_smul]
      abel
    calc
      f (path t) = f ((1 - t) • x + t • y) := congrArg f hpoint
      _ ≤ (1 - t) * f x + t * f y -
          (1 - t) * t * (m / 2 * ‖x - y‖ ^ 2) := by
        simpa [smul_eq_mul] using hstrong
      _ = (1 - t) * f (path 0) + t * f (path 1) -
          (m * t * (1 - t) / 2) * dist (path 0) (path 1) ^ 2 := by
        simp [path, dist_eq_norm]
        ring
  have hline :
      HasLineDerivAt ℝ f (inner ℝ (grad x) (y - x)) x (y - x) := by
    have h := (hgrad x hx).hasFDerivAt.hasLineDerivAt (y - x)
    simpa [InnerProductSpace.toDual_apply_apply] using h
  have hderiv :
      HasDerivAt (fun t : ℝ => f (path t)) (inner ℝ (grad x) (y - x)) 0 := by
    simpa [HasLineDerivAt, path] using hline
  have hfirst :=
    Geometry.GeodesicConvexity.firstOrder_geodesicConvexity
      hconvex hpath hderiv
  simpa [path, dist_eq_norm, norm_sub_rev] using hfirst

/-- The gradient of a strongly convex function has the corresponding inner-product
lower bound on its domain.

Mathematical provenance: Optlib `Strong_Convex_lower`, commit
`5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3`,
`Optlib/Convex/StronglyConvex.lean` (Apache-2.0; Chenyi Li and Ziyu Wang).
This proof reuses the local first-order bound in both directions, as in Chewi,
arXiv:2605.07006v1, Proposition 1.6, (1.4) implies (1.5).
The domain-local supplied-gradient interface retains arbitrary real `m`;
Chewi's whole-space `C¹`, nonnegative-modulus statement is a specialization.
-/

Exact module and namespace context

hxy and hyx are the two calls to the same ASTIS parent. rw changes the reversed displacement to a negative, normalizes its norm, and expands inner_sub_left. linarith combines the two scalar inequalities without assuming the desired conclusion.

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_inner_lower_bound_of_strongConvexOn
    {s : Set E} {f : E → ℝ} {m : ℝ} {grad : E → E}
    (hsc : StrongConvexOn s m f)
    (hgrad : ∀ z ∈ s, HasGradientAt f (grad z) z)
    {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
    m * ‖y - x‖ ^ 2 ≤ inner ℝ (grad y - grad x) (y - x) := by
  have hxy := firstOrder_lower_bound_of_strongConvexOn hsc hgrad hx hy
  have hyx := firstOrder_lower_bound_of_strongConvexOn hsc hgrad hy hx
  rw [show x - y = -(y - x) by abel, inner_neg_right, norm_neg] at hyx
  rw [inner_sub_left]
  linarith

end

end StrongConvexFirstOrder
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

C¹ gives a genuine derivative of f at every point. The chain rule differentiates the composition with x+sv, including the two endpoints. The derivative map is continuous because f is C¹. Evaluating it on the fixed direction v and composing with the segment gives a continuous scalar integrand; compact-interval integrability follows. FTC and the values at 0 and 1 give the identity.

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 sub_eq_integral_gradient {f : E → ℝ} (hf : ContDiff ℝ 1 f) (x v : E) :
    f (x + v) - f x = ∫ s : ℝ in 0..1, inner ℝ (gradient f (x + s • v)) v := by
  have hc : Continuous (fun s : ℝ => inner ℝ (gradient f (x + s • v)) v) := by
    simpa [gradient, Function.comp_def] using
      ((hf.continuous_fderiv (by norm_num)).comp
        (continuous_const.add (continuous_id.smul continuous_const))).clm_apply continuous_const
  have hd (s : ℝ) : HasDerivAt (fun t : ℝ => f (x + t • v))
      (inner ℝ (gradient f (x + s • v)) v) s := by
    convert! (hf.differentiable_one (x + s • v)).hasGradientAt.hasFDerivAt.comp_hasDerivAt s
      (((hasDerivAt_id s).smul_const v).const_add x) using 1
    simp
  simpa using (intervalIntegral.integral_eq_sub_of_hasDerivAt
    (fun s _ => hd s) (hc.intervalIntegrable 0 1)).symm

/-- Quantitative gradient monotonicity implies the chord inequality by the
source's two affine-segment FTC identities and integration of their difference.
The modulus can be signed; no Hessian or extra integrability is assumed. -/

Exact module and namespace context

Put v=y−x and fix 0≤t≤1. Apply the segment identity to v and to tv. Scalar linearity moves t outside the second integral. The case t=1 is equality. For t<1 and 0<s<1, the difference of the two segment points is s(1−t)v. Apply gradient monotonicity and cancel s(1−t)>0. No division occurs at a zero displacement parameter. C¹ makes A and B continuous and hence interval integrable. The inequality on the open interval suffices because Lebesgue measure gives its endpoints zero mass. Integrate s from 0 to 1. Multiply the integrated lower bound by nonnegative t and substitute the two FTC identities. This gives the exact m/2 correction; it also covers t=0. The signed m is never divided by or required to be positive.

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 strongConvexOn_univ_of_gradient_mono_integral
    {f : E → ℝ} {m : ℝ} (hf : ContDiff ℝ 1 f)
    (hm : ∀ x y : E, m * ‖y - x‖ ^ 2 ≤
      inner ℝ (gradient f y - gradient f x) (y - x)) :
    StrongConvexOn (univ : Set E) m f := by
  refine ⟨convex_univ, ?_⟩
  intro x _ y _ a t ha ht hat
  have hat' : a = 1 - t := by linarith
  subst a
  have ht1 : t ≤ 1 := by linarith
  rcases eq_or_lt_of_le ht1 with ht1 | ht1
  · subst t
    simp
  let v := y - x
  let A : ℝ → ℝ := fun s => inner ℝ (gradient f (x + s • v)) v
  let B : ℝ → ℝ := fun s => inner ℝ (gradient f (x + (s * t) • v)) v
  have hA : Continuous A := by
    simpa [A, gradient, Function.comp_def] using
      ((hf.continuous_fderiv (by norm_num)).comp
        (continuous_const.add (continuous_id.smul continuous_const))).clm_apply continuous_const
  have hB : Continuous B := by
    simpa [B, gradient, Function.comp_def] using
      ((hf.continuous_fderiv (by norm_num)).comp
        (continuous_const.add ((continuous_id.mul continuous_const).smul continuous_const))).clm_apply continuous_const
  have hbound : ∫ s : ℝ in 0..1, m * s * (1 - t) * ‖v‖ ^ 2 ≤
      ∫ s : ℝ in 0..1, (A s - B s) := by
    apply intervalIntegral.integral_mono_on_of_le_Ioo (by norm_num)
      ((show Continuous (fun s : ℝ => m * s * (1 - t) * ‖v‖ ^ 2) by fun_prop).intervalIntegrable 0 1)
      ((hA.sub hB).intervalIntegrable 0 1)
    intro s hs
    have h := hm (x + (s * t) • v) (x + s • v)
    have hdis : (x + s • v) - (x + (s * t) • v) = (s * (1 - t)) • v := by module
    rw [hdis, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs, inner_smul_right] at h
    have hscaled : (s * (1 - t)) * (m * s * (1 - t) * ‖v‖ ^ 2) ≤
        (s * (1 - t)) * inner ℝ
          (gradient f (x + s • v) - gradient f (x + (s * t) • v)) v := by nlinarith [h]
    have hcancel := le_of_mul_le_mul_left hscaled (mul_pos hs.1 (sub_pos.mpr ht1))
    simpa [A, B, inner_sub_left] using hcancel
  have hpoly : (∫ s : ℝ in 0..1, m * s * (1 - t) * ‖v‖ ^ 2) =
      m / 2 * (1 - t) * ‖v‖ ^ 2 := by
    rw [intervalIntegral.integral_mul_const, intervalIntegral.integral_mul_const,
      intervalIntegral.integral_const_mul, integral_id]
    norm_num only [one_pow, zero_pow, sub_zero]
    ring
  rw [hpoly, intervalIntegral.integral_sub (hA.intervalIntegrable 0 1)
    (hB.intervalIntegrable 0 1)] at hbound
  have hy := sub_eq_integral_gradient hf x v
  have hz := sub_eq_integral_gradient hf x (t • v)
  have hpoint : (1 - t) • x + t • y = x + t • v := by dsimp [v]; module
  have hys : x + v = y := by simp [v]
  rw [hys] at hy
  change f y - f x = ∫ s : ℝ in 0..1, A s at hy
  simp only [smul_smul, inner_smul_right, intervalIntegral.integral_const_mul] at hz
  change f (x + t • v) - f x = t * ∫ s : ℝ in 0..1, B s at hz
  change f ((1 - t) • x + t • y) ≤ (1 - t) * f x + t * f y -
    (1 - t) * t * (m / 2 * ‖x - y‖ ^ 2)
  rw [hpoint, norm_sub_rev]
  change f (x + t • v) ≤ (1 - t) * f x + t * f y -
    (1 - t) * t * (m / 2 * ‖v‖ ^ 2)
  nlinarith [mul_le_mul_of_nonneg_left hbound ht]

/-- Proposition 1.6, part 1: on all of Euclidean space, the C¹ chord,
quadratic lower-model and gradient-monotonicity conditions are equivalent.
The nonnegative modulus is retained exactly as in the source. -/

Exact module and namespace context

C¹ supplies the ambient gradients everywhere. Apply the already compiled shared lower-model theorem, whose proof takes the derivative limit of the strong-convexity chord inequality. Assume only the global lower-model condition, apply it in both orders, and add. Function values cancel, the two half-quadratic terms add, and the inner products combine into a gradient difference. The newly proved integral converse takes gradient monotonicity back to the chord condition. Package the two equivalences using this three-condition cycle.

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 convexity_equivalences {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ}
    {m : ℝ} (_hm : 0 ≤ m) (hf : ContDiff ℝ 1 f) :
    (StrongConvexOn univ m f ↔ ∀ x y,
      f x + inner ℝ (gradient f x) (y - x) + m / 2 * ‖y - x‖ ^ 2 ≤ f y) ∧
    (StrongConvexOn univ m f ↔ ∀ x y,
      m * ‖y - x‖ ^ 2 ≤ inner ℝ (gradient f y - gradient f x) (y - x)) := by
  have hg : ∀ z ∈ (univ : Set (EuclideanSpace ℝ (Fin d))),
      HasGradientAt f (gradient f z) z := fun z _ => (hf.differentiable_one z).hasGradientAt
  have hforward := fun (hsc : StrongConvexOn univ m f) x y =>
    StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn hsc hg
      (mem_univ x) (mem_univ y)
  have hsum : (∀ x y, f x + inner ℝ (gradient f x) (y - x) +
      m / 2 * ‖y - x‖ ^ 2 ≤ f y) → ∀ x y,
      m * ‖y - x‖ ^ 2 ≤ inner ℝ (gradient f y - gradient f x) (y - x) := by
    intro hl x y
    have hxy := hl x y
    have hyx := hl y x
    rw [show x - y = -(y - x) by abel, inner_neg_right, norm_neg] at hyx
    rw [inner_sub_left]
    linarith
  exact ⟨⟨hforward, fun h => strongConvexOn_univ_of_gradient_mono_integral hf (hsum h)⟩,
    ⟨fun h => hsum (hforward h), strongConvexOn_univ_of_gradient_mono_integral hf⟩⟩

end AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC1

Exact module and namespace context

Set g(t)=Df(x+tv)[v]. Because f is C², Df is C¹; compose its derivative with the affine segment and evaluate the resulting linear functional at the fixed v. The second derivative is continuous. Composition with the segment and two evaluations preserve continuity, giving interval integrability. FTC gives g(1)−g(0). The gradient pairing identity identifies the endpoints.

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_sub_inner_eq_integral_fderiv2
    {f : E → ℝ} (hf : ContDiff ℝ 2 f) (x v : E) :
    inner ℝ (gradient f (x + v) - gradient f x) v =
      ∫ t : ℝ in 0..1, (fderiv ℝ (fderiv ℝ f) (x + t • v) v) v := by
  have hfd : ContDiff ℝ 1 (fderiv ℝ f) := hf.fderiv_right (by norm_num)
  have hd (t : ℝ) : HasDerivAt (fun s : ℝ => fderiv ℝ f (x + s • v) v)
      ((fderiv ℝ (fderiv ℝ f) (x + t • v) v) v) t := by
    convert ((hfd.differentiable_one _).hasFDerivAt.comp_hasDerivAt t
      (((hasDerivAt_id t).smul_const v).const_add x)).clm_apply
      (hasDerivAt_const t v) using 1 <;> first | rfl | simp
  have hc : Continuous (fun t : ℝ => (fderiv ℝ (fderiv ℝ f) (x + t • v) v) v) :=
    (((hfd.continuous_fderiv (by norm_num)).comp
      (continuous_const.add (continuous_id.smul continuous_const))).clm_apply
        continuous_const).clm_apply continuous_const
  simpa [inner_sub_left, gradient, Function.comp_def] using
    (intervalIntegral.integral_eq_sub_of_hasDerivAt
      (fun t _ => hd t) (hc.intervalIntegrable 0 1)).symm

/-- Global quantitative gradient monotonicity is equivalent to the genuine
Hessian diagonal lower bound, by a right derivative limit and the FTC. -/

Exact module and namespace context

Fix x,v and let g(t)=Df(x+tv)[v]. Apply gradient monotonicity at x and x+tv with t>0. The displacement is tv and its squared norm is t²‖v‖². Cancelling the positive t and dividing once more by t gives a bound on the difference quotient. C² gives g′(0)=D²f(x)[v,v]. The displayed inequality holds for all positive t, so passage to t↓0 preserves it. Neither m nor ‖v‖ is divided by. For v=y−x the Hessian bound holds along x+tv. C² gives a continuous integrand and interval integrability. Integrate the constant lower bound over an interval of length one, then use the preceding segment identity.

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_mono_iff_fderiv2_lower
    {f : E → ℝ} {m : ℝ} (hf : ContDiff ℝ 2 f) :
    (∀ x y : E, m * ‖y - x‖ ^ 2 ≤
      inner ℝ (gradient f y - gradient f x) (y - x)) ↔
    ∀ x v : E, m * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) x v) v := by
  have hfd : ContDiff ℝ 1 (fderiv ℝ f) := hf.fderiv_right (by norm_num)
  constructor
  · intro hm x v
    let g : ℝ → ℝ := fun t => fderiv ℝ f (x + t • v) v
    have hdAll (t : ℝ) : HasDerivAt g
        ((fderiv ℝ (fderiv ℝ f) (x + t • v) v) v) t := by
      convert ((hfd.differentiable_one _).hasFDerivAt.comp_hasDerivAt t
        (((hasDerivAt_id t).smul_const v).const_add x)).clm_apply
        (hasDerivAt_const t v) using 1 <;> first | rfl | simp
    have hd : HasDerivAt g ((fderiv ℝ (fderiv ℝ f) x v) v) 0 := by
      simpa using hdAll 0
    apply ge_of_tendsto hd.tendsto_slope_zero_right
    filter_upwards [self_mem_nhdsWithin] with t ht
    have ht : 0 < t := ht
    have h := hm x (x + t • v)
    rw [add_sub_cancel_left, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs,
      inner_smul_right, inner_sub_left] at h
    have hscaled : t * (m * ‖v‖ ^ 2) ≤ g t - g 0 := by
      apply le_of_mul_le_mul_left (a := t) _ ht
      simpa [g, gradient, Function.comp_def, pow_two, mul_assoc, mul_left_comm, mul_comm] using h
    simpa [smul_eq_mul, div_eq_inv_mul] using
      (le_div_iff₀ ht).mpr (by simpa [mul_comm] using hscaled)
  · intro hH x y
    let v := y - x
    have hc : Continuous (fun t : ℝ => (fderiv ℝ (fderiv ℝ f) (x + t • v) v) v) :=
      (((hfd.continuous_fderiv (by norm_num)).comp
        (continuous_const.add (continuous_id.smul continuous_const))).clm_apply
          continuous_const).clm_apply continuous_const
    have h := intervalIntegral.integral_mono_on (by norm_num : (0 : ℝ) ≤ 1)
      (intervalIntegrable_const : IntervalIntegrable (fun _ : ℝ => m * ‖v‖ ^ 2) volume 0 1)
      (hc.intervalIntegrable 0 1) (fun t _ => hH (x + t • v) v)
    rw [← gradient_sub_inner_eq_integral_fderiv2 hf x v] at h
    simpa [v] using h

/-- Proposition 1.6 part 2, with the source's whole Euclidean domain,
nonnegative modulus and C² regularity. Together with the C¹ theorem this
connects all four source conditions. -/

Exact module and namespace context

C² implies C¹. Apply the already proved source equivalence between the chord condition and global gradient monotonicity. Compose with the derivative-limit/integral equivalence above. On Euclidean space D²f(x)[v,v] is the source Hessian matrix quadratic form. This finishes part 2 and connects it to the lower-model equivalence already in part 1.

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 strongConvexOn_iff_fderiv2_lower
    {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} {m : ℝ}
    (hm : 0 ≤ m) (hf : ContDiff ℝ 2 f) :
    StrongConvexOn univ m f ↔
      ∀ x v, m * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) x v) v := by
  exact (ConvexityC1.convexity_equivalences hm (hf.of_le (by norm_num))).2.trans
    (gradient_mono_iff_fderiv2_lower hf)

end AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC2

Exact module and namespace context

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.

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 := 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

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.

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 := 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