English
If f and g are concave on s with f(x) ≥ 0 and g(x) ≥ 0 for x ∈ s and f,g antivary on s, then the product h = f • g is concave on s.
Русский
Если f и g конкавны на s, f(x) ≥ 0 и g(x) ≥ 0 на s, и f,g антивариют на s, то h=f•g конкавна.
LaTeX
$$$\begin{aligned} &\text{ConcaveOn}(s,f) \land \text{ConcaveOn}(s,g) \land \forall x\in s: f(x) \ge 0, \ g(x) \ge 0 \\ &\ &\text{AntivaryOn}(f,g,s) \Rightarrow \text{ConcaveOn}(s, f\cdot g). \end{aligned}$$$
Lean4
/-- `x^n`, `n : ℕ` is convex on the whole real line whenever `n` is even. -/
protected theorem convexOn_pow {n : ℕ} (hn : Even n) : ConvexOn 𝕜 univ fun x : 𝕜 ↦ x ^ n :=
by
obtain ⟨n, rfl⟩ := hn
simp_rw [← two_mul, pow_mul]
refine ConvexOn.pow ⟨convex_univ, fun x _ y _ a b ha hb hab ↦ sub_nonneg.1 ?_⟩ (fun _ _ ↦ by positivity) _
calc
(0 : 𝕜) ≤ (a * b) * (x - y) ^ 2 := by positivity
_ = _ := by obtain rfl := eq_sub_of_add_eq hab; simp only [smul_eq_mul]; ring
