AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization

- A nonnegative quadratic regularization shifts the strong-convexity and actual gradient-Lipschitz constants by its precision, including zero precision. All derivatives are genuine because the input potential is everywhere C².

theorem strongConvexOn_and_lipschitzWith_gradient_add_quadratic
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    {U : E → ℝ} {m L r : ℝ≥0}
    (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E,
      (m : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ U) x v) v ∧
      (fderiv ℝ (fderiv ℝ U) x v) v ≤ (L : ℝ) * ‖v‖ ^ 2)
    (u : E) :
    let W := fun x => U x + (r : ℝ) / 2 * ‖x - u‖ ^ 2
    StrongConvexOn Set.univ ((m + r : ℝ≥0) : ℝ) W ∧
      LipschitzWith (L + r) (gradient W) := by
  let W := fun x => U x + (r : ℝ) / 2 * ‖x - u‖ ^ 2
  have hUd : Differentiable ℝ U := hU.differentiable (by norm_num)
  have hUdd : Differentiable ℝ (fderiv ℝ U) :=
    (hU.fderiv_right (m := 1) (by norm_num)).differentiable_one
  have hn : ContDiff ℝ 2 (fun x : E => ‖x - u‖ ^ 2) :=
    (contDiff_id.sub contDiff_const).norm_sq (𝕜 := ℝ)
  have hW : ContDiff ℝ 2 W := hU.add (contDiff_const.mul hn)
  have hq (x : E) : HasFDerivAt (fun z => (r : ℝ) / 2 * ‖z - u‖ ^ 2)
      ((r : ℝ) • innerSL ℝ (x - u)) x := by
    convert (((hasFDerivAt_id x).sub_const u).norm_sq).const_mul ((r : ℝ) / 2)
      using 1 <;> first | rfl | (ext v; simp; ring)
  have hWfd (x : E) : fderiv ℝ W x =
      fderiv ℝ U x + (r : ℝ) • innerSL ℝ (x - u) :=
    ((hUd x).hasFDerivAt.add (hq x)).fderiv
  let J : E →L[ℝ] (E →L[ℝ] ℝ) :=
    { toFun := fun v => innerSL ℝ v
      map_add' := by intros; ext; simp
      map_smul' := by intros; ext; simp
      cont := (innerSL ℝ (E := E)).continuous }
  have hWdd (x : E) : HasFDerivAt (fderiv ℝ W)
      (fderiv ℝ (fderiv ℝ U) x + (r : ℝ) • J) x := by
    rw [show fderiv ℝ W = (fun z => fderiv ℝ U z +
      (r : ℝ) • innerSL ℝ (z - u)) from funext hWfd]
    convert (hUdd x).hasFDerivAt.add
      ((J.hasFDerivAt.comp x ((hasFDerivAt_id x).sub_const u)).const_smul
        (r : ℝ)) using 1 <;> rfl
  have hbounds (x v : E) :
      ((m + r : ℝ≥0) : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ W) x v) v ∧
      (fderiv ℝ (fderiv ℝ W) x v) v ≤ ((L + r : ℝ≥0) : ℝ) * ‖v‖ ^ 2 := by
    rw [(hWdd x).fderiv]
    change ((m : ℝ) + r) * ‖v‖ ^ 2 ≤
        (fderiv ℝ (fderiv ℝ U) x v) v + (r : ℝ) * inner ℝ v v ∧
      (fderiv ℝ (fderiv ℝ U) x v) v + (r : ℝ) * inner ℝ v v ≤
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticRegularization.lean:29published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.