English
Right translation preserves convexity: if f is convex on s, then the translated preimage of s under z ↦ c+z is convex for the composed function f ∘ (z ↦ c+z).
Русский
Правое сдвиг сохраняет выпуклость: если f выпукла на s, то отображение сдвига по c сохраняет выпуклость для композиции f ∘ (z ↦ c+z).
LaTeX
$$$$ \\text{ConvexOn } 𝕜\\ s\\ f \\rightarrow\\ \\forall c,\\ \\text{ConvexOn } 𝕜\\ ((\\lambda z, c+z)^{-1} s)\\ (f \\circ (\\lambda z, c+z)). $$$$
Lean4
/-- Right translation preserves convexity. -/
theorem translate_right (hf : ConvexOn 𝕜 s f) (c : E) : ConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z) :=
⟨hf.1.translate_preimage_right _, fun x hx y hy a b ha hb hab =>
calc
f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y)) := by
rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self hab]
_ ≤ a • f (c + x) + b • f (c + y) := hf.2 hx hy ha hb hab⟩
