smul — Mathlib

English

Scaling a convex function by a nonnegative scalar preserves convexity.

Русский

Умножение выпуклой функции на неотрицательное число сохраняет выпуклость.

LaTeX

$$$\text{ConvexOn } 𝕜\ s\ f \land c\ge 0 \Rightarrow ConvexOn 𝕜 s (\lambda x. c \cdot f x)$$$

Lean4

theorem smul {c : 𝕜} (hc : 0 ≤ c) (hf : ConvexOn 𝕜 s f) : ConvexOn 𝕜 s fun x => c • f x :=
  ⟨hf.1, fun x hx y hy a b ha hb hab =>
    calc
      c • f (a • x + b • y) ≤ c • (a • f x + b • f y) := smul_le_smul_of_nonneg_left (hf.2 hx hy ha hb hab) hc
      _ = a • c • f x + b • c • f y := by rw [smul_add, smul_comm c, smul_comm c]⟩

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