Quadratic regularization preserves first-order smoothness

Subtract delta||x||²/2 from W. Expanding the squared distance leaves f plus a linear functional and a constant. This is convex because f is convex. The Mathlib characterization therefore proves delta-strong convexity, with the delta/2 chord convention. Differentiate the squared norm composed with x↦x-u, multiply by delta/2 and add the derivative of f. The factors two and one-half cancel. This gives the genuine Frechet derivative of W and hence its differentiability. Apply the inverse Riesz isometry to the derivative just computed. Linearity preserves addition and scalar multiplication, while the inverse of the functional v↦⟨x-u,v⟩ is x-u. Thus the claimed gradient is computed from W, not supplied as an assumption. Subtract the gradient identity at y from the one at x; the center cancels. The triangle inequality, the given beta-Lipschitz estimate for the true gradient of f, and nonnegativity of delta bound the two terms. Add the bounds to obtain beta+delta.

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 curvature_gradient_and_smoothness
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    {f : E → ℝ} (hd : Differentiable ℝ f) (hc : ConvexOn ℝ univ f)
    {β δ : ℝ≥0} (hL : LipschitzWith β (gradient f)) (u : E) :
    let W := fun x => f x + (δ : ℝ)/2*‖x-u‖^2
    Differentiable ℝ W ∧ StrongConvexOn univ (δ : ℝ) W ∧
      (∀ x, gradient W x = gradient f x + (δ : ℝ) • (x-u)) ∧
      LipschitzWith (β+δ) (gradient W) := by
  let W := fun x => f x + (δ : ℝ)/2*‖x-u‖^2
  have hq (x : E) : HasFDerivAt (fun z => (δ : ℝ)/2*‖z-u‖^2)
      ((δ : ℝ) • innerSL ℝ (x-u)) x := by
    convert (((hasFDerivAt_id x).sub_const u).norm_sq).const_mul ((δ : ℝ)/2)
      using 1 <;> first | rfl | (ext v; simp; ring)
  have hWd : Differentiable ℝ W := fun x => ((hd x).hasFDerivAt.add (hq x)).differentiableAt
  have hgrad (x : E) : gradient W x = gradient f x + (δ : ℝ) • (x-u) := by
    have hfd : fderiv ℝ W x = fderiv ℝ f x + (δ : ℝ) • innerSL ℝ (x-u) :=
      ((hd x).hasFDerivAt.add (hq x)).fderiv
    rw [gradient, hfd, map_add, map_smul]
    congr 1
    exact congrArg (fun v : E => (δ : ℝ) • v) ((toDual ℝ E).symm_apply_apply (x-u))
  have hstrong : StrongConvexOn univ (δ : ℝ) W := by
    apply strongConvexOn_iff_convex.mpr
    have ha := (hc.add (((-(δ : ℝ)) • (innerSL ℝ u).toLinearMap).convexOn convex_univ)).add_const
      ((δ : ℝ)/2*‖u‖^2)
    convert! ha using 1
    ext x
    simp [W, norm_sub_sq_real, real_inner_comm]
    ring
  refine ⟨hWd,hstrong,hgrad,?_⟩
  apply LipschitzWith.of_dist_le_mul
  intro x y
  rw [dist_eq_norm, hgrad, hgrad]
  have he : gradient f x + (δ : ℝ) • (x-u) -
      (gradient f y + (δ : ℝ) • (y-u)) =
      (gradient f x-gradient f y) + (δ : ℝ) • (x-y) := by
    simp only [smul_sub]
    abel
  rw [he]
  have hb := hL.dist_le_mul x y
  rw [dist_eq_norm, dist_eq_norm] at hb
  calc
    _ ≤ ‖gradient f x-gradient f y‖ + ‖(δ : ℝ) • (x-y)‖ := norm_add_le _ _
    _ ≤ (β : ℝ)*‖x-y‖ + (δ : ℝ)*‖x-y‖ := by
      rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg δ.coe_nonneg]
      linarith
    _ = ((β+δ : ℝ≥0) : ℝ)*dist x y := by rw [dist_eq_norm]; simp; ring
end AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationFirstOrder

Exact module and namespace context