English
If f is convex on s, it remains convex when precomposed by an affine map.
Русский
Если f выпукла на s, то f ∘ g выпукла на предобразе аффинного отображения g.
LaTeX
$$$ConvexOn\ 𝕜\ s\ f \Rightarrow ConvexOn 𝕜 (g^{-1}(s)) (f \circ g) \text{ for affine } g$$$
Lean4
/-- If a function is convex on `s`, it remains convex when precomposed by an affine map. -/
theorem comp_affineMap {f : F → β} (g : E →ᵃ[𝕜] F) {s : Set F} (hf : ConvexOn 𝕜 s f) : ConvexOn 𝕜 (g ⁻¹' s) (f ∘ g) :=
⟨hf.1.affine_preimage _, fun x hx y hy a b ha hb hab =>
calc
(f ∘ g) (a • x + b • y) = f (g (a • x + b • y)) := rfl
_ = f (a • g x + b • g y) := by rw [Convex.combo_affine_apply hab]
_ ≤ a • f (g x) + b • f (g y) := hf.2 hx hy ha hb hab⟩
