English
If f is convex on s, then f ∘ g is convex on the preimage of s under a linear map g.
Русский
Если f выпукла на s, то f ∘ g выпукла на прообразе s под линейным отображением g.
LaTeX
$$$\text{If } f \text{ is convex on } s, \text{ then } f\circ g \text{ is convex on } g^{-1}(s)$$$
Lean4
/-- If `f` is convex on `s`, so is `(f ∘ g)` on `g ⁻¹' s` for a linear `g`. -/
theorem comp_linearMap {f : F → β} {s : Set F} (hf : ConvexOn 𝕜 s f) (g : E →ₗ[𝕜] F) : ConvexOn 𝕜 (g ⁻¹' s) (f ∘ g) :=
⟨hf.1.linear_preimage _, fun x hx y hy a b ha hb hab =>
calc
f (g (a • x + b • y)) = f (a • g x + b • g y) := by rw [g.map_add, g.map_smul, g.map_smul]
_ ≤ a • f (g x) + b • f (g y) := hf.2 hx hy ha hb hab⟩
