AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGradientConverse

- Quantitative monotonicity of genuine ambient gradients on a convex domain implies strong convexity, with the same (possibly signed) modulus.

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

AutoSamplingTheory/TechnicalLemmas/Analysis/StrongConvexGradientConverse.lean:31published source at 0e31a3cda412Open detailed card

Excerpt truncated; the exact source link is authoritative.