English
If f is 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 concave 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{ConcaveOn}(s, f\cdot g). \end{aligned}$$$
Lean4
theorem pow (hf : ConvexOn 𝕜 s f) (hf₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ f x) : ∀ n, ConvexOn 𝕜 s (f ^ n)
| 0 => by simpa using convexOn_const 1 hf.1
| n + 1 => by
rw [pow_succ']
exact hf.mul (hf.pow hf₀ _) hf₀ (fun x hx ↦ pow_nonneg (hf₀ hx) _) <| (monovaryOn_self f s).pow_right₀ hf₀ n
