English
If f and g are convex on s with f(x) ≥ 0 and g(x) ≥ 0 on s and MonovaryOn f g s, then the product h = f · g is convex on s.
Русский
Если f и g выпуклы на s, на s неотрицательны, и MonovaryOn(f,g,s), то произведение h=f g выпукло на s.
LaTeX
$$$\begin{aligned} &\text{ConvexOn}(s,f) \land \text{ConvexOn}(s,g) \land \forall x\in s: f(x) \ge 0,\ g(x) \ge 0 \\ &\ &\text{MonovaryOn}(f,g,s) \Rightarrow \text{ConvexOn}(s, f\cdot g). \end{aligned}$$$
Lean4
theorem smul_concaveOn' [IsOrderedModule 𝕜 E] (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g)
(hf₀ : ∀ ⦃x⦄, x ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ g x) (hfg : MonovaryOn f g s) : ConvexOn 𝕜 s (f • g) :=
by
rw [← neg_concaveOn_iff, ← smul_neg]
exact hf.smul'' hg.neg hf₀ (fun x hx ↦ neg_nonpos.2 <| hg₀ hx) hfg.neg_right
