English
Let f be concave on s and g convex on s with f(x) ≤ 0 and g(x) ≥ 0 for x ∈ s, and AntivaryOn f g s holds. Then the product h = f • g is convex on s.
Русский
Пусть f конкавна, g выпукла, f(x) ≤ 0 и g(x) ≥ 0 на s, и AntivaryOn(f,g,s) выполняется. Тогда h=f•g выпукло на s.
LaTeX
$$$\begin{aligned} &\text{ConcaveOn}(s,f) \land \text{ConvexOn}(s,g) \land \forall x\in s: f(x) \le 0, \ g(x) \ge 0 \\ &\ &\text{AntivaryOn}(f,g,s) \Rightarrow \text{ConvexOn}(s, f\cdot g). \end{aligned}$$$
Lean4
theorem mul_convexOn' (hf : ConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x⦄, x ∈ s → f x ≤ 0)
(hg₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ g x) (hfg : AntivaryOn f g s) : ConcaveOn 𝕜 s (f • g) :=
hf.smul_convexOn' hg hf₀ hg₀ hfg
