English
If f is convex on s and g is concave on s with f(x) ≤ 0 and g(x) ≤ 0 for x ∈ s, and MonovaryOn f g s holds, then the product h = f • g is concave on s.
Русский
Если f выпукла, g конкавна, причем f(x) ≤ 0 и g(x) ≤ 0 на s, и выполняется MonovaryOn(f,g,s), тогда h=f•g конкавна на s.
LaTeX
$$$\begin{aligned} &\text{ConvexOn}(s,f) \land \text{ConcaveOn}(s,g) \land \forall x in s: f(x) \le 0,\ g(x) \le 0 \\ &\ &\text{MonovaryOn}(f,g,s) \Rightarrow \text{ConcaveOn}(s, f\cdot g). \end{aligned}$$$
Lean4
theorem mul (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ g x)
(hfg : MonovaryOn f g s) : ConvexOn 𝕜 s (f * g) :=
hf.smul' hg hf₀ hg₀ hfg
