AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder

- A strongly convex function lies above its first-order model by the quadratic term `m / 2 * ‖y - x‖²`. This is the ASTIS-owned shared port of Optlib's pinned `Strong_Convex_second_lower`. The statement is deliberately domain-local and uses a supplied Mathlib gradient. Chewi's whole-space `C¹` formulation is a downstream specialization, not a silent relabeling of this more general shared interface. The proof factors through `Geometry.GeodesicConvexity.firstOrder_geodesicConvexity`: strong convexity supplies the chord inequality on the affine segment and the supplied gradient supplies the derivative of that segment at its initial point.

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.
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Analysis/StrongConvexFirstOrder.lean:45published source at 0e31a3cda412Open detailed card

Excerpt truncated; the exact source link is authoritative.

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

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

AutoSamplingTheory/TechnicalLemmas/Analysis/StrongConvexFirstOrder.lean:97published source at 0e31a3cda412Open detailed card