English
A further instance of the smul' rule: under suitable hypotheses, the product of two convexOn-type functions is convex on the domain.
Русский
Ещё одно приложение правила smul': произведение двух функций выпукло на области, при условиях выпуклости и монотоваривания.
LaTeX
$$$\\text{ConvexOn } 𝕜\\, S\\,(f\\cdot g)\\text{ holds under appropriate convexity and monotonicity assumptions.}$$$
Lean4
theorem smul' (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ g x)
(hfg : MonovaryOn f g s) : ConvexOn 𝕜 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) (hf₀ <| hf.1 hx hy ha hb hab) <|
add_nonneg (smul_nonneg ha <| hg₀ hx) <| smul_nonneg hb <| hg₀ hy).trans
?_
calc
_ = (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g y + f y • g x) := ?_
_ ≤ (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g x + f y • g y) := by gcongr _ + (a * b) • ?_;
exact hfg.smul_add_smul_le_smul_add_smul hx hy
_ = (a * (a + b)) • (f x • g x) + (b * (a + b)) • (f y • g y) := by
simp only [mul_add, add_smul, smul_add, mul_comm _ a]; abel
_ = _ := by simp_rw [hab, mul_one]
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, add_comm _ ((b * b) • f y • g y), add_add_add_comm,
add_comm ((a * b) • f y • g x)]
