English
If hg is strictly convex on f(S) for g, hf is strictly concave on S for f, hg' is strictly AntiOn on f(S), and hf' is InjOn on f, 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{StrictConcaveOn}_{\\mathsf{𝕜}}(S,f) \\land \\operatorname{StrictAntiOn}_{\\mathsf{𝕜}}(g,f(S)) \\land \\operatorname{Set.InjOn}(f,S) \\Rightarrow \\operatorname{StrictConvexOn}_{\\mathsf{𝕜}}(S, g\\circ f). $$$$
Lean4
theorem comp (hg : StrictConcaveOn 𝕜 (f '' s) g) (hf : StrictConcaveOn 𝕜 s f) (hg' : StrictMonoOn g (f '' s))
(hf' : s.InjOn f) : StrictConcaveOn 𝕜 s (g ∘ f) :=
⟨hf.1, fun _ hx _ hy hxy _ _ ha hb hab =>
(hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) (mt (hf' hx hy) hxy) ha hb hab).trans <|
hg' (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab)
(mem_image_of_mem f <| hf.1 hx hy ha.le hb.le hab) <|
hf.2 hx hy hxy ha hb hab⟩
