English
Right translation preserves strict convexity.
Русский
Правое перенос сохраняет строгую выпуклость.
LaTeX
$$$StrictConvexOn\ 𝕜\ s\ f \Rightarrow \forall c\, StrictConvexOn\ 𝕜\ (Set.preimage(\lambda z. c + z)\ s)\ (f \circ (\lambda z. c + z))$$$
Lean4
/-- Right translation preserves strict convexity. -/
theorem translate_right (hf : StrictConvexOn 𝕜 s f) (c : E) :
StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z) :=
⟨hf.1.translate_preimage_right _, fun x hx y hy hxy 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 ((add_right_injective c).ne hxy) ha hb hab⟩
