English
Let s be a subset of G and f,g: G → E, G → F be convex on s with f(x) ≤ 0 and g(x) ≤ 0 for all x ∈ s, and assume AntivaryOn f g s. Then the pointwise product h(x) = f(x) · g(x) is concave on s.
Русский
Пусть s ⊆ G и f: G → E, g: G → F — выпуклы на s с условиями f(x) ≤ 0, g(x) ≤ 0 для всех x в s, и f,g антивариют на s. Тогда h(x) = f(x) · g(x) — в точности конкавна на s.
LaTeX
$$$\begin{aligned} &\text{Пусть } s \subseteq G, \ f: G \to E, \ g: G \to F, \\ &\text{и } f,g \text{ выпуклы на } s, \ f(x) \le 0, \ g(x) \le 0 \text{ на } s, \\ &\text{и } \text{MonovaryOn}(f,g,s). \\ & h = f \cdot g. \\ & \text{Тогда } h \text{ конкавна на } s. \end{aligned}$$$
Lean4
theorem smul'' [IsOrderedModule 𝕜 E] (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x⦄, x ∈ s → f x ≤ 0)
(hg₀ : ∀ ⦃x⦄, x ∈ s → g x ≤ 0) (hfg : AntivaryOn f g s) : ConcaveOn 𝕜 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
