StrongConvexFirstOrder: mathematical reading route

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