comp_convexOn — Mathlib

English

If hg is concave on f(S) for g, hf is convex 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{ConvexOn}_{\\mathsf{𝕜}}(S,f) \\land \\operatorname{AntitoneOn}_{\\mathsf{𝕜}}(g,f(S)) \\Rightarrow \\operatorname{ConcaveOn}_{\\mathsf{𝕜}}(S, g\\circ f). $$$$

Lean4

theorem comp_convexOn (hg : ConcaveOn 𝕜 (f '' s) g) (hf : ConvexOn 𝕜 s f) (hg' : AntitoneOn g (f '' s)) :
    ConcaveOn 𝕜 s (g ∘ f) :=
  hg.dual.comp hf hg'

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