English
If f and g are concave on s with f(x) ≤ 0 and g(x) ≤ 0 for x ∈ s, and f and g antivary on s, then the product h(x) = f(x) · g(x) is convex on s.
Русский
Если f и g конкавны на s и удовлетворяют f(x) ≤ 0, g(x) ≤ 0 на s, и f,g антивариют на s, то h(x) = f(x)·g(x) выпуклона на s.
LaTeX
$$$\begin{aligned} &\text{Пусть } f,g: G \to \mathbb{R}, \text{ конкавны на } s, \ f(x) \le 0, \ g(x) \le 0 \text{ для } x\in s, \\ &\ \text{MonovaryOn}(f,g,s) \Rightarrow \text{ConvexOn}(s, f\cdot g). \end{aligned}$$$
Lean4
theorem smul'' (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x⦄, x ∈ s → f x ≤ 0)
(hg₀ : ∀ ⦃x⦄, x ∈ s → g x ≤ 0) (hfg : MonovaryOn f g s) : ConvexOn 𝕜 s (f • g) :=
by
rw [← neg_smul_neg]
exact hf.neg.smul' hg.neg (fun x hx ↦ neg_nonneg.2 <| hf₀ hx) (fun x hx ↦ neg_nonneg.2 <| hg₀ hx) hfg.neg
