comp_concaveOn — Mathlib

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'

Похожие утверждения