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