English
A function f on a real normed space is uniformly convex on a set s with modulus φ if for all x,y in s and a,b ≥ 0 with a+b=1, f(a x + b y) ≤ a f(x) + b f(y) − a b φ(‖x−y‖).
Русский
Функция f на вещественном нормированном пространстве равномерно выпукла на множества s с модулем φ, если для любых x,y из s и a,b ≥ 0 с a+b=1 выполняется неравенство выпуклости с минусом модуля φ(‖x−y‖).
LaTeX
$$$UniformConvexOn(s,\phi, f) := Convex\ Real(s)\ \land\ \forall x\in s,\forall y\in s,\forall a,b\ge 0,\ a+b=1\Rightarrow f(a x + b y) \le a f(x) + b f(y) - a b \phi(\|x-y\|).$$$
Lean4
/-- A function `f` from a real normed space is uniformly convex with modulus `φ` if
`f (t • x + (1 - t) • y) ≤ t • f x + (1 - t) • f y - t * (1 - t) * φ ‖x - y‖` for all `t ∈ [0, 1]`.
`φ` is usually taken to be a monotone function such that `φ r = 0 ↔ r = 0`. -/
def UniformConvexOn (s : Set E) (φ : ℝ → ℝ) (f : E → ℝ) : Prop :=
Convex ℝ s ∧
∀ ⦃x⦄,
x ∈ s →
∀ ⦃y⦄,
y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y - a * b * φ ‖x - y‖
