mul_const for StrictConcaveOn?

Stream: new members

[Adomas Baliuka]

I couldn't find this in Mathlib. It should be there, right? (My proof is ugly, of course. Happy for suggestions how to improve)

import Mathlib

lemma StrictConcaveOn.mul_const {c : ℝ} (cpos : 0 < c) (f : ℝ → ℝ) :
    StrictConcaveOn ℝ S f → StrictConcaveOn ℝ S (fun x ↦ c * f x) := by
    rintro ⟨hconv, h⟩
    refine' ⟨hconv, fun x hx y hy hxy a b ha hb hab => _⟩
    simp
    have := h hx hy hxy ha hb hab
    simp at this
    convert (mul_lt_mul_left cpos).mpr this using 1
    ring

Loogle for StrictConcaveOn _ _ _, "mul" gives nothing relevant.

[Eric Rodriguez]

I'd PR this and similar things for other sides :)

[Adomas Baliuka]

What do you mean by "sides"?

[Ruben Van de Velde]

Shorter:

import Mathlib

lemma StrictConcaveOn.mul_const {c : ℝ} (cpos : 0 < c) (f : ℝ → ℝ) (h : StrictConcaveOn ℝ S f) :
    StrictConcaveOn ℝ S (fun x ↦ c * f x) := by
  refine' ⟨h.1, fun x hx y hy hxy a b ha hb hab => _⟩
  simp_rw [← mul_smul_comm, ← mul_add, mul_lt_mul_left cpos]
  exact h.2 hx hy hxy ha hb hab

[Eric Wieser]

Is this true more generally for smul?

[Yaël Dillies]

Yep. I have a better proof. PR incoming.

[Adomas Baliuka]

Maybe also add strictConvexOn_id and strictConcaveOn_id (for Real -> Real functions)?

[Yaël Dillies]

id is certainly not strictly convex!

[Adomas Baliuka]

Right, sorry... it's not strict of course, and the "non-strict" versions seem to be in Mathlib already...