English
If hg is concave on f(S) for g, hf is concave on S for f, and hg' is antitone on f(S), then concavity of g∘f on S holds.
Русский
Если hg конкавна на f(S) для g, hf конкавна на S для f, и hg' антимонотонна на f(S), то конкавность g∘f на S выполнена.
LaTeX
$$$$ \\operatorname{ConcaveOn}_{\\mathsf{𝕜}}(f(S),g) \\land \\operatorname{ConcaveOn}_{\\mathsf{𝕜}}(S,f) \\land \\operatorname{AntitoneOn}_{\\mathsf{𝕜}}(g,f(S)) \\Rightarrow \\operatorname{ConcaveOn}_{\\mathsf{𝕜}}(S, g\\circ f). $$$$
Lean4
theorem comp_concaveOn (hg : ConvexOn 𝕜 (f '' s) g) (hf : ConcaveOn 𝕜 s f) (hg' : AntitoneOn g (f '' s)) :
ConvexOn 𝕜 s (g ∘ f) :=
hg.dual.comp hf hg'