English
Let s be a subset of G and f: G → E, g: G → F be concave on s, with f(x) ≥ 0 and g(x) ≥ 0 for all x ∈ s, and assume f and g antivary on s. Then the pointwise product h(x) = f(x) · g(x) is concave on s.
Русский
Пусть s ⊆ G и f: G → E, g: G → F — конкавны на s, при этом ∀x ∈ s имеет место f(x) ≥ 0 и g(x) ≥ 0, и 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) \ge 0, \ g(x) \ge 0 \text{ для } x \in s, \\ &\text{и } f,g \ антивариют на } s. \\ &\text{Пусть } h = f \cdot g. \\ &\text{Тогда } h \text{ конкавна на } s. \end{aligned}$$$
Lean4
theorem smul' [IsOrderedModule 𝕜 E] (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ f x)
(hg₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ g x) (hfg : AntivaryOn f g s) : ConcaveOn 𝕜 s (f • g) :=
by
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
dsimp
refine
(smul_le_smul (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
(add_nonneg (smul_nonneg ha <| hf₀ hx) <| smul_nonneg hb <| hf₀ hy) (hg₀ <| hf.1 hx hy ha hb hab)).trans'
?_
calc
a • f x • g x + b • f y • g y = (a * (a + b)) • (f x • g x) + (b * (a + b)) • (f y • g y) := by
simp_rw [hab, mul_one]
_ = (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g x + f y • g y) := by
simp only [mul_add, add_smul, smul_add, mul_comm _ a]; abel
_ ≤ (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g y + f y • g x) := by gcongr _ + (a * b) • ?_;
exact hfg.smul_add_smul_le_smul_add_smul hx hy
_ = _ := ?_
simp only [add_smul, smul_add]
rw [← smul_smul_smul_comm a, ← smul_smul_smul_comm b, ← smul_smul_smul_comm a b, ← smul_smul_smul_comm b b,
smul_eq_mul, smul_eq_mul, smul_eq_mul, smul_eq_mul, mul_comm b a, add_comm ((a * b) • f x • g y),
add_comm ((a * b) • f x • g y), add_add_add_comm]
