English
Right translating the domain preserves convexity: preimage under a translation of the domain yields a convexOn for the composed function.
Русский
Правое перемещение домена сохраняет выпуклость: предобраз под переносом преобразования сохраняет ConvexOn для композицией.
LaTeX
$$$hf : ConvexOn\ 𝕜\ s\ f \rightarrow ConvexOn\ 𝕜\ ((fun z => c + z)^{-1} s)\ (f \circ (fun z => c + z))$$$
Lean4
theorem convex_le (hf : ConvexOn 𝕜 s f) (r : β) : Convex 𝕜 ({x ∈ s | f x ≤ r}) := fun x hx y hy a b ha hb hab =>
⟨hf.1 hx.1 hy.1 ha hb hab,
calc
f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha hb hab
_ ≤ a • r + b • r := by
gcongr
· exact hx.2
· exact hy.2
_ = r := Convex.combo_self hab r⟩
