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