English
If hg is strictly concave on f(S) for g, hf is strictly convex on S for f, hg' is strictly AntiOn on f(S), and hf' is InjOn on S, then g∘f is strictly concave on S.
Русский
Если hg строго конкавна на f(S) для g, hf строго выпукла на S для f, hg' строго анти-монтона на f(S), hf' инъективна на S, тогда g∘f строго конкавна на S.
LaTeX
$$$$ \\operatorname{StrictConcaveOn}_{\\mathsf{𝕜}}(f(S),g) \\land \\operatorname{StrictConvexOn}_{\\mathsf{𝕜}}(S,f) \\land \\operatorname{StrictAntiOn}_{\\mathsf{𝕜}}(g,f(S)) \\land \\operatorname{Set.InjOn}(f,S) \\Rightarrow \\operatorname{StrictConcaveOn}_{\\mathsf{𝕜}}(S, g\\circ f). $$$$
Lean4
theorem comp_strictConvexOn (hg : StrictConcaveOn 𝕜 (f '' s) g) (hf : StrictConvexOn 𝕜 s f)
(hg' : StrictAntiOn g (f '' s)) (hf' : s.InjOn f) : StrictConcaveOn 𝕜 s (g ∘ f) :=
hg.dual.comp hf hg' hf'
