English
If hg is convex on f(S) for g, hf is concave on S for f, and hg' is antitone on f(S), then g∘f is convex on S.
Русский
Если hg выпукла на f(S) для g, hf конкавна на S для f, и hg' антимонотонна на f(S), то g∘f выпукла на S.
LaTeX
$$$$ \\operatorname{ConvexOn}_{\\mathsf{𝕜}}(f(S),g) \\land \\operatorname{ConcaveOn}_{\\mathsf{𝕜}}(S,f) \\land \\operatorname{AntitoneOn}_{\\mathsf{𝕜}}(g,f(S)) \\Rightarrow \\operatorname{ConvexOn}_{\\mathsf{𝕜}}(S, g\\circ f). $$$$
Lean4
theorem comp (hg : ConcaveOn 𝕜 (f '' s) g) (hf : ConcaveOn 𝕜 s f) (hg' : MonotoneOn g (f '' s)) :
ConcaveOn 𝕜 s (g ∘ f) :=
⟨hf.1, fun _ hx _ hy _ _ ha hb hab =>
(hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab).trans <|
hg' (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab)
(mem_image_of_mem f <| hf.1 hx hy ha hb hab) <|
hf.2 hx hy ha hb hab⟩
