English
Let f be convex on s and g concave on s, with f(x) ≤ 0 and g(x) ≥ 0 for x ∈ s, and assume MonovaryOn f g s. Then the product h = f · g is concave on s.
Русский
Пусть f выпукла на s, g конкавна на s, f(x) ≤ 0 и g(x) ≥ 0 на s, и 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 \land g(x) \ge 0 \\ &\ \text{MonovaryOn}(f,g,s) \Rightarrow \text{ConcaveOn}(s, f\cdot g). \end{aligned}$$$
Lean4
theorem smul_concaveOn (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ f x)
(hg₀ : ∀ ⦃x⦄, x ∈ s → g x ≤ 0) (hfg : AntivaryOn f g s) : ConcaveOn 𝕜 s (f • g) :=
by
rw [← neg_convexOn_iff, ← smul_neg]
exact hf.smul' hg.neg hf₀ (fun x hx ↦ neg_nonneg.2 <| hg₀ hx) hfg.neg_right
