strongConvexOn_iff_convex — Mathlib

English

In an inner product space, StrongConvexOn s m f is equivalent to ConvexOn s of f minus (m/2)‖x‖^2.

Русский

В пространстве с внутренним произведением StrongConvexOn s m f эквивалентно тому, что f − (m/2)‖x‖^2 выпукла на s.

LaTeX

$$$$ \text{StrongConvexOn}(s,m,f) \iff \text{ConvexOn}(\mathbb{R},s\; (f(x) - \tfrac{m}{2} \|x\|^2)). $$$$

Lean4

theorem strongConvexOn_iff_convex : StrongConvexOn s m f ↔ ConvexOn ℝ s fun x ↦ f x - m / (2 : ℝ) * ‖x‖ ^ 2 :=
  by
  refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_
  simp_rw [sub_le_iff_le_add, smul_eq_mul, aux_sub ha hb hab, mul_assoc, mul_left_comm]

Похожие утверждения